{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/150216"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/150216","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Foundational Integration Verification of Diverse Software and Hardware Components","abstract":"The engineering of computer systems is distinguished by a long-standing tradition of building on quicksand. Even the most venerable and critical systems have a history of serious bugs and security vulnerabilities. Human fallibility continues to prevail. Computer-checked mathematical proofs of software correctness have emerged as a promising method to rule out large classes of bugs. However, the appropriate notion of correctness for a computer-systems component is exceedingly difficult to specify correctly in isolation, and unrelated verification of adjacent components does not rule out bugs due to their interactions. Therefore, I argue for (1) centering systems-verification efforts around interface specifications within a proof assistant, (2) proving both clients and implementations of an interface, and (3) using these results to prove an integrated-correctness theorem stated without referencing the internal interfaces. I present a serious (several-year, several-person) exploration of what formally proven computer-systems development would look like if this practice were standard, culminating in precedent-setting case studies involving embedded implementations of networked software and elliptic-curve cryptography. Whole-system correctness theorems spanning from application behavior to hardware designs are proven by instantiating correctness proofs of compilers, translation validators, processor implementations, and mathematical theories. For example, RISC-V machine code for a public-key-authenticated Ethernet server is proven to always eventually satisfy a trace predicate. Specifications of imperative languages within the system are modeled using an underappreciated technique that we call omnisemantics. Choosing an inductively defined weakest-precondition predicate transformer as the semantics of a language allows unspecified behavior to be encoded using rules with universally quantified premises, greatly simplifying compiler-correctness proofs and program-logic construction.","abstract_html":"The engineering of computer systems is distinguished by a long-standing tradition of building on quicksand. Even the most venerable and critical systems have a history of serious bugs and security vulnerabilities. Human fallibility continues to prevail. Computer-checked mathematical proofs of software correctness have emerged as a promising method to rule out large classes of bugs. However, the appropriate notion of correctness for a computer-systems component is exceedingly difficult to specify correctly in isolation, and unrelated verification of adjacent components does not rule out bugs due to their interactions. Therefore, I argue for (1) centering systems-verification efforts around interface specifications within a proof assistant, (2) proving both clients and implementations of an interface, and (3) using these results to prove an integrated-correctness theorem stated without referencing the internal interfaces. I present a serious (several-year, several-person) exploration of what formally proven computer-systems development would look like if this practice were standard, culminating in precedent-setting case studies involving embedded implementations of networked software and elliptic-curve cryptography. Whole-system correctness theorems spanning from application behavior to hardware designs are proven by instantiating correctness proofs of compilers, translation validators, processor implementations, and mathematical theories. For example, RISC-V machine code for a public-key-authenticated Ethernet server is proven to always eventually satisfy a trace predicate. Specifications of imperative languages within the system are modeled using an underappreciated technique that we call omnisemantics. Choosing an inductively defined weakest-precondition predicate transformer as the semantics of a language allows unspecified behavior to be encoded using rules with universally quantified premises, greatly simplifying compiler-correctness proofs and program-logic construction.","abstract_has_math":false,"creators":["Erbsen, Andres"],"institution":"Massachusetts Institute of Technology","degree_name":"Doctoral","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Chlipala, Adam"],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-02","date_published":"2023-02","updated_at":"2026-07-22T22:22:27Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"rights_urls":["http://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/150216","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Chlipala, Adam"]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"]},{"key":"dc:creator","label":"Author","values":["Erbsen, Andres"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2023-03-31T14:40:14Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2023-03-31T14:40:14Z"]},{"key":"dc:date.issued","label":"Date","values":["2023-02"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctoral","Doctor of Philosophy"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright MIT"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/150216"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["The engineering of computer systems is distinguished by a long-standing tradition of building on quicksand. Even the most venerable and critical systems have a history of serious bugs and security vulnerabilities. Human fallibility continues to prevail. Computer-checked mathematical proofs of software correctness have emerged as a promising method to rule out large classes of bugs. However, the appropriate notion of correctness for a computer-systems component is exceedingly difficult to specify correctly in isolation, and unrelated verification of adjacent components does not rule out bugs due to their interactions. Therefore, I argue for (1) centering systems-verification efforts around interface specifications within a proof assistant, (2) proving both clients and implementations of an interface, and (3) using these results to prove an integrated-correctness theorem stated without referencing the internal interfaces. I present a serious (several-year, several-person) exploration of what formally proven computer-systems development would look like if this practice were standard, culminating in precedent-setting case studies involving embedded implementations of networked software and elliptic-curve cryptography. Whole-system correctness theorems spanning from application behavior to hardware designs are proven by instantiating correctness proofs of compilers, translation validators, processor implementations, and mathematical theories. For example, RISC-V machine code for a public-key-authenticated Ethernet server is proven to always eventually satisfy a trace predicate. Specifications of imperative languages within the system are modeled using an underappreciated technique that we call omnisemantics. Choosing an inductively defined weakest-precondition predicate transformer as the semantics of a language allows unspecified behavior to be encoded using rules with universally quantified premises, greatly simplifying compiler-correctness proofs and program-logic construction."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Ph.D."]},{"key":"dc:title","label":"Title","values":["Foundational Integration Verification of Diverse Software and Hardware Components"]}]}],"canonical_facts":{"dc:contributor.advisor":["Chlipala, Adam"],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"],"dc:creator":["Erbsen, Andres"],"dc:date.accessioned":["2023-03-31T14:40:14Z"],"dc:date.available":["2023-03-31T14:40:14Z"],"dc:date.issued":["2023-02"],"dc:description.abstract":["The engineering of computer systems is distinguished by a long-standing tradition of building on quicksand. Even the most venerable and critical systems have a history of serious bugs and security vulnerabilities. Human fallibility continues to prevail. Computer-checked mathematical proofs of software correctness have emerged as a promising method to rule out large classes of bugs. However, the appropriate notion of correctness for a computer-systems component is exceedingly difficult to specify correctly in isolation, and unrelated verification of adjacent components does not rule out bugs due to their interactions. Therefore, I argue for (1) centering systems-verification efforts around interface specifications within a proof assistant, (2) proving both clients and implementations of an interface, and (3) using these results to prove an integrated-correctness theorem stated without referencing the internal interfaces. I present a serious (several-year, several-person) exploration of what formally proven computer-systems development would look like if this practice were standard, culminating in precedent-setting case studies involving embedded implementations of networked software and elliptic-curve cryptography. Whole-system correctness theorems spanning from application behavior to hardware designs are proven by instantiating correctness proofs of compilers, translation validators, processor implementations, and mathematical theories. For example, RISC-V machine code for a public-key-authenticated Ethernet server is proven to always eventually satisfy a trace predicate. Specifications of imperative languages within the system are modeled using an underappreciated technique that we call omnisemantics. Choosing an inductively defined weakest-precondition predicate transformer as the semantics of a language allows unspecified behavior to be encoded using rules with universally quantified premises, greatly simplifying compiler-correctness proofs and program-logic construction."],"dc:description.degree":["Ph.D."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/150216"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"dc:rights.uri":["http://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["Foundational Integration Verification of Diverse Software and Hardware Components"],"dc:type":["Thesis"],"thesis:degree_name":["Doctoral","Doctor of Philosophy"]},"updated_at":"2026-07-22T22:22:27Z"}