A Proof-Oriented Approach to Low-Level, High-Assurance Programming
thesisposted on 2022-02-23, 22:04 authored by Aymeric FromherzAymeric Fromherz
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 concerns
about 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 describe
next. 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 compose
and verify C and assembly cryptographic implementations against shared specifications. We then demonstrate how abstraction and zero-cost generic programming can simplify
verification without sacrificing performance, leading to verified cryptographic code whose performance matches or exceeds the best unverified implementations. EverCrypt
has 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 verification
framework based on a higher-order, impredicative concurrent separation logic shallowly embedded in the F? proof assistant. We show how designing Steel with proofs in
mind enables us to automatically separate verification conditions between separationlogic predicates and first-order logic encodeable predicates, allowing us to provide
practical automation through a mixture of efficient reflective tactics that focus on the former, and SMT solving for the latter. We finally demonstrate the expressiveness and
programmability of Steel on a variety of examples, including sequential, self-balancing trees; standard, concurrent data structures such as the Owicki-Gries monotonic counter
and 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.
DepartmentElectrical and Computer Engineering
- Doctor of Philosophy (PhD)