A Proof-Oriented Approach to Low-Level, High-Assurance Programming

From autonomous cars to online banking, software nowadays is widely used in safety and security-critical settings. As the complexity and size of software grows, ensuring that it behaves as a programmer intended becomes increasingly difficult, raising concernsabout software���s reliability. To tackle this problem, we wish to provide strong, formal guarantees about the security and correctness of real-world critical software. In this thesis, we therefore advocate for the adoption of a proof-oriented programming paradigm in high-assurance software development. We argue that co-developing programs and proofs yields several benefits: the program structure can simplify the proofs, while proofs can simplify programming and improve the software quality too by, for instance, eliminating unneeded checks and cases. To validate this thesis, we rely on two case studies, which we describenext. Our first case study targets high-performance cryptography, the cornerstone of Internet security. Relying on proof-oriented programming, we develop EverCrypt, a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. We first propose a methodology to composeand verify C and assembly cryptographic implementations against shared specifications. We then demonstrate how abstraction and zero-cost generic programming can simplifyverification without sacrificing performance, leading to verified cryptographic code whose performance matches or exceeds the best unverified implementations. EverCrypthas been deployed in several high-profile open-source projects such as Mozilla Firefox and the Linux Kernel.Our second case study investigates the use of proof-oriented programming to develop concurrent, low-level systems. To this end, we present Steel, a novel verificationframework based on a higher-order, impredicative concurrent separation logic shallowly embedded in the F? proof assistant. We show how designing Steel with proofs inmind enables us to automatically separate verification conditions between separationlogic predicates and first-order logic encodeable predicates, allowing us to providepractical automation through a mixture of efficient reflective tactics that focus on the former, and SMT solving for the latter. We finally demonstrate the expressiveness andprogrammability of Steel on a variety of examples, including sequential, self-balancing trees; standard, concurrent data structures such as the Owicki-Gries monotonic counterand Michael and Scott���s 2-lock queue; various synchronization primitives such as libraries for spin locks and fork/join parallelism; and a library for message-passing concurrency on dependently typed channels.