{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/88993"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/88993","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Automated deductive verification of systems software","abstract":"Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage.","abstract_html":"Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage.","abstract_has_math":false,"creators":["Pek, Edgar"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Parthasarathy, Madhusudan","King, Samuel T","Ball, Thomas","Rosu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-03-02T19:33:42Z","date_published":"2016-03-02T19:33:42Z","updated_at":"2026-07-22T22:26:32Z","subjects":["software verification","software security","automated deductive reasoning"],"languages":["en"],"rights":["Copyright 2015 Edgar Pek"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/88993","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan","King, Samuel T","Ball, Thomas","Rosu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Pek, Edgar"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016-03-02T19:33:42Z","2015-11-25","2015-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["software verification","software security","automated deductive reasoning"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2015 Edgar Pek"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/88993"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-03-02 without embargo terms","The student, Edgar Pek, accepted the attached license on 2015-11-17 at 12:27.","The student, Edgar Pek, submitted this Dissertation for approval on 2015-11-17 at 12:30.","This Dissertation was approved for publication on 2015-11-25 at 11:27.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8795 on 2016-03-02 at 12:50:08","Made available in DSpace on 2016-03-02T19:33:42Z (GMT). No. of bitstreams: 2 PEK-DISSERTATION-2015.pdf: 1317729 bytes, checksum: bc08e8664dd69717fd08082b4c832215 (MD5) LICENSE.txt: 4206 bytes, checksum: a202742244abfa787271da00d4d48638 (MD5) Previous issue date: 2015-11-25"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Automated deductive verification of systems software"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan","King, Samuel T","Ball, Thomas","Rosu, Grigore"],"dc:creator":["Pek, Edgar"],"dc:date":["2016-03-02T19:33:42Z","2015-11-25","2015-12"],"dc:description":["Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-03-02 without embargo terms","The student, Edgar Pek, accepted the attached license on 2015-11-17 at 12:27.","The student, Edgar Pek, submitted this Dissertation for approval on 2015-11-17 at 12:30.","This Dissertation was approved for publication on 2015-11-25 at 11:27.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8795 on 2016-03-02 at 12:50:08","Made available in DSpace on 2016-03-02T19:33:42Z (GMT). No. of bitstreams: 2 PEK-DISSERTATION-2015.pdf: 1317729 bytes, checksum: bc08e8664dd69717fd08082b4c832215 (MD5) LICENSE.txt: 4206 bytes, checksum: a202742244abfa787271da00d4d48638 (MD5) Previous issue date: 2015-11-25"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/88993"],"dc:language":["en"],"dc:rights":["Copyright 2015 Edgar Pek"],"dc:subject":["software verification","software security","automated deductive reasoning"],"dc:title":["Automated deductive verification of systems software"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:32Z"}