This presentation is an overview of and update on our project Fiat Cryptography, which uses the Coq proof assistant to generate fast cryptographic code, with proof of correctness. Code produced with this tool is now included by all major web browsers for TLS (secure browsing), and PEPM techniques are at front and center.

The heart of the project is our original verified compiler, which specializes functional programs into C-like code. It is proved in Coq and extracted to a command-line tool. Inside, it is a combination of a partial-evaluation engine, abstract interpreter, and other fairly innocuous compiler phases. A canonical use specializes a general modular-arithmetic algorithm to parameters like the large prime modulus. The resulting code has generally been the fastest pure C code for different algorithms.

We’ve been up to some improvements lately, aiming toward a complete cryptographic library generated from nice functional code but ending up as performance-competitive C code with a Coq proof of correctness. To expand the scope of functional programs that we can specialize, we developed Rupicola, an alternative to Coq extraction that targets C-like code, generates proofs, and supports extension with proved user hints. To push formal guarantees to lower levels, we have also been developing tooling to bottom out in x86 assembly code, relying on a new verified translation validator, so that we can bring arbitrary compilers into the picture. For instance, a random-search tool created by our collaborators is able to find new world-champion implementations for the second-most-recent generation of Intel processors – with Coq proofs connecting the assembly code back to whiteboard-level functional programs.

Started hacking on compilers & web-development tools in the late 1990s. Finished CS undergrad at Carnegie Mellon in 2003 and CS PhD at Berkeley in 2007, picking up mechanized proof of executable, decently practical systems with Coq as a main focus in between. Postdoc at Harvard through 2011, then faculty at MIT since. Author of Certified Programming with Dependent Types, a popular online & in-print introduction to using Coq at scale. Lately into building practical but clean-slate hardware-software stacks with end-to-end Coq proofs of everything digital, at the same time as developing a startup-company idea to trick ordinary people into using dependent types (with Ur/Web) to generate their business applications.