Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala. Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises. Proceedings of the IEEE Symposium on Security & Privacy 2019 (S&P'19). May 2019.

Coming soon!

In the domain of cryptographic-primitive implementation, where coding is usually done manually at a low level and with minimal abstraction, we introduce a new approach that supports high-level library-based coding, without giving up acceptable performance. Specifically, we present a general framework for elliptic-curve arithmetic, with automatic generation of performance-competitive code for new curves and hardware targets, also generating machine-checked proofs of correctness using the Coq proof assistant. Where previous work has required hand-coding an implementation for each combination of curve and hardware target, we demonstrate automatic generation of the now fastest-known C code for dozens of curves, also coming close enough to the best-known assembly code that it is plausible that orthogonal C-compiler improvements can close the gap. For instance, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve; but our main result is design of a framework to reuse development (and proof) effort across many curves, without sacrificing performance. Our framework has been adopted in a few prominent places, including in the Chrome Web browser, for the curve arithmetic behind the public-key-crypto part of TLS connection initiation.

Source code