Fast Cryptographic Code via Partial Evaluation

on YouTube ↗58m

" summary

Generates mechanically verified, high-performance cryptographic C from Coq: a verified compiler using partial evaluation, abstract interpretation and normalization-by-evaluation specializes generic modular-arithmetic code to a prime and digit layout and produces C that is 5–10× faster than a generic multiprecision baseline on 64-bit x86. Tooling includes Rupicola for C-like extraction, Bedrock2 for low-level proofs, and a verified x86 validator that checks assembly found by a genetic search; on recent Intel CPUs the search yields new world‑champion implementations.

AI-written summary · about

" chapters (27)

1. 0:00Intro
2. 2:35Outline
3. 3:05Web Browsing with SSL Web Server
4. 8:05We introduced Fiat Cryptography. Parameters
5. 8:57Wide Adoption
6. 9:33Correct-by-Construction Cryptography
7. 11:57Generated Code
8. 12:48Surprising (?) Fact About Modular Arithmetic
9. 16:43The Basic Idea
10. 17:49Example: Multiplication (for modulus 2127 - 1)
11. 22:04Compiling to Low-Level Code
12. 23:42Implementation and Experiments
13. 24:57Many-Primes Experiment
14. 27:32P-256 Mixed Addition
15. 28:53Adoption?
16. 31:44Did Formal Methods Make a Big Difference?
17. 37:42Not all sunshine & roses....
18. 38:53Proof by Reflection
19. 40:27What is the generic reducer doing?
20. 42:27Parametric Higher-Order Abstract Syntax (PHOAS)
21. 42:46Normalization by Evaluation (more detail)
22. 43:26Not quite outputting plain expressions....
23. 45:54Hoare Logic Reordered
24. 46:52Rupicola Architecture
25. 47:57Rupicola Compilation Example
26. 51:02CryptOpt Architecture
27. 52:53A Minimal Equivalence Checker

" related talks

• 19mCryptOpt: Verified Compilation with Randomized Program Search for Cryptographic PrimitivesAdam Chlipala, David Wu, Daniel Genkin, Owen Conoly, Andres Erbsen, Joel Kuepper, Jason Gross, Chuyue Sun, Samuel Tian, Chitchanok Chuengsatiansup, Markus Wagner, Yuval Yarom · PLDI 2023
• 29mVale: Verifying High-Performance Cryptographic Assembly CodeSrinath Setty, Bryan Parno, Chris Hawblitzel, Barry Bond, Manos Kapritsos, Ashay Rane, K. Rustan M. Leino, Jacob R. Lorch, Laure Thompson · 26th USENIX Security Symposium (USENIX Security '17)
• 59mCoq to C Translation with Partial Evaluation + Counterexample GenerationJohn Toman, Takeshi Tsukada, Naoki Kobayashi, Akira Tanaka, Hideto Ueno · PEPM 2021
• 01h 04mSoftware Verification meets Real-World CryptographyKarthikeyan Bhargavan · Dafny 2026
• 24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...Aurèle Barrière, Sandrine Blazy, David Pichardie · POPL 2023
• 20mFoundational Integration Verification of a Cryptographic ServerAdam Chlipala, Dustin Jamner, Clément Pit-Claudel, Andres Erbsen, Samuel Gruetter, Jade Philipoom, Ashley Lin · PLDI 2024
• 24mA CompCert Compiler that Preserves Cryptographic Constant-timeRemi Hutin · PriSC 2020
• 01h 25mIntroduction to Verifiable ComputingAhto Truu · ACCU 2022