[PEPM'23] Fast Cryptographic Code via Partial Evaluation

[PEPM'23] Fast Cryptographic Code via Partial Evaluation

Adam Chlipala

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.