CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun,, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel, Genkin, Markus Wagner, Yuval Yarom

TL;DR
CryptOpt is a novel verified compilation pipeline that uses randomized search and formal proof to generate highly optimized assembly code for cryptographic primitives, outperforming traditional compilers.
Contribution
It introduces a new approach combining randomized search with formal verification to produce faster cryptographic assembly code from high-level functional programs.
Findings
Produced the fastest known implementations of Curve25519 and secp256k1.
Achieved performance improvements over GCC and Clang.
Provided mechanized proof of correctness in Coq.
Abstract
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have the patience to write directly in assembly language. However, cryptography has been an exception, where many performance-critical routines have been written directly in assembly (sometimes through metaprogramming layers). Some past work has shown how to do formal verification of that assembly, and other work has shown how to generate C code automatically along with formal proof, but with consequent performance penalties vs. the best-known assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized proof (in Coq) whose final theorem statement mentions little…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Advanced Malware Detection Techniques · Formal Methods in Verification
