CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
summary
CryptOpt turns Fiat Cryptography IR into x86-64 assembly by running a random local search over instruction selection and scheduling, auto-benchmarking candidates on target CPUs, then proving equivalence with a formally verified checker implemented in Coq. Results show per-function speedups (example 60% vs Clang in a microexample; curve25519 multiply ~19% faster on average) and new fastest-known field-arithmetic for Curve25519 and secp256k1 on Intel 12th/13th gens, with end-to-end machine-checked correctness.
AI-written summary · about
chapters (9)
- 0:00CryptOpt introduction and goals
- 1:45Handwritten vs compiler assembly
- 2:51Random search for assembly
- 6:04Performance vs baseline
- 7:08Field study results
- 8:11Scalar multiplication results
- 9:14Proving assembly correctness
- 10:39CryptOpt achievements summary
- 11:42Q&A
related talks
58mFast Cryptographic Code via Partial Evaluation
24mA CompCert Compiler that Preserves Cryptographic Constant-time
29mVale: Verifying High-Performance Cryptographic Assembly Code
16mReconciling Optimization With Secure Compilation
19mFormally Verifying Optimizations with Block Simulations
40mImplementation
20mFoundational Integration Verification of a Cryptographic Server
22mInteractive Source-to-Source Optimizations Validated using Static Resource Analysis