The cryptographic code that runs the Internet is subject to intense manual optimization by elite programmers. Most of the complexity of the optimized code comes from manipulation of integers too large to fit in hardware registers. Perhaps surprisingly, for a change as innocuous as changing an algorithmic parameter to a different prime number, significant pieces of code are rewritten from scratch. Only a handful of experts on the planet are seen as competent enough to do it well, and new implementations (which often include significant amounts of handwritten assembly) tend to take months to code and debug.
In this paper, we demonstrate that the work of those experts can be automated while si multaneously increasing our confidence in code correctness. We implemented a framework in the Coq proof assistant for generating efficient code for elliptic curve cryptography (ECC), with proofs of conformance to a whiteboard-level specification in number theory. While some past projects have verified this kind of code, ours is the first to synthesize it from security parameters.
We also have a smaller trusted code base than in past work, as all of our formal reasoning is done within Coq. Still, our generated code is faster than past work that verified clean-slate implementations. We come within a factor of 6 of the running time of the handcrafted world-champion implementations.