Foundational Integration Verification of Diverse Software and Hardware Components

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.

Name thesis:degree_name

Doctoral

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2023

Author dc:creator

• Erbsen, Andres

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright MIT

Licence dc:rights.uri

• http://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/150216

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/150216