Fiat Cryptography: A Formally Verified Compiler for Finite-Field Arithmetic

Abstract: Fiat Cryptography is a formally verified compiler for cryptographic arithmetic code, bridging the gap between whiteboard-level math and performant C code.  It started as an MIT project developed mostly by undergrads and has since been adopted by very popular open-source projects, including Chrome and Firefox.  I will give background on the problem and solution, the latter being a split between coding and proving generic algorithms as functional programs, using partial evaluation to specialize those programs to parameters, and then applying relatively traditional compilation to turn the resulting programs into C code, with Coq proofs associated with all the steps.  I will say a bit about the adoption story of Fiat Cryptography and what more general lessons we derive from that experience.  Finally, I will sketch ongoing work and tell a larger story of correct-by-construction derivation of cryptographic libraries, beyond the straightline code that the original project targeted.

Adam Chlipala has been on the faculty in computer science at MIT since 2011.  He did his undergrad at Carnegie Mellon and his PhD at Berkeley, and his research focuses on clean-slate redesign of computer-systems infrastructure, typically taking advantage of machine-checked proofs of functional correctness.  Much of his work uses the Coq proof assistant, about which he has written a popular book, "Certified Programming with Dependent Types."  He most enjoys finding opportunities for drastic simplification over incumbent abstractions in computer systems, and some favorite tools toward that end are object-capability systems, transactions, proof-carrying code, and high-level languages with whole-program optimizing compilers.  Some projects particularly far along the real-world-adoption curve are Fiat Cryptography, for proof-producing generation of low-level cryptographic code, today run by Chrome for most HTTPS connections; and Ur/Web, a production-quality domain-specific language for Web applications.