This grant supported work investigating a particular approach to programming with strong mathematical guarantees of correctness.  The unusual features relate to use of proof assistant software, which checks mathematical proofs, which may be about complex computer systems.  Work explored how to do programming inside a proof assistant (in particular, the Coq system), so that one integrated environment supports coding, writing down specifications capturing what is correct behavior, writing proofs establishing correctness, and compiling code into executable form.

The initial project plan centered on the Bedrock framework, for producing low-level software through the use of multiple high-level languages.  Key demonstrations with Bedrock included verification of a multithreaded web server.  There were also crucial technological contributions in proof automation and in structuring of large proofs so that they are broken into manageable pieces, for instance mirroring the decomposition of a program across libraries or languages.

Partly through collaborations with faculty in other research areas, the Bedrock approach was also extended fruitfully to other domains, not envisioned when the original project plan was written.  In the Kami project, we support development, proof, and compilation of digital hardware components like processors and memory systems.  In the FSCQ project, we support a similar model for creating proved file systems that integrate with real OS kernels.  In the Fiat Cryptography project, we support generation of low-level code for fast cryptographic primitives.  And two other projects demonstrated how this approach applies to distributed systems, specifically key-value stores and scientific stencil computations.

Broader impacts have included development of a new graduate course with an associated textbook, Formal Reasoning About Programs.  There has also been a significant amount of technology transfer to industry.  Most notably, Fiat Cryptography has been adopted by Google to generate elliptic-curve arithmetic code for Chrome, Android, and servers (e.g., for the main search engine); so now a majority of secure web connections opened by browsers use code generated and proved with our methods and tools.  Two startup companies are also applying our results, in consultation with the PI.  BedRock Systems is applying the latest Bedrock library to verification of operating systems for safety-critical applications like in the automotive industry.  SiFive, Inc. is piloting use of the Kami framework to prove correctness of key hardware components that factor into their business model of helping customers put together custom hardware solutions via component reuse.

Last Modified: 10/01/2018
Modified by: Adam J Chlipala