Software Verification meets Real-World Cryptography
summary
Verified cryptography is now practical: about a dozen verified libraries exist and verified code runs in Firefox and on major cloud services, produced from roughly 250,000 lines of F that generate about 30,000 lines of C/assembly. The toolchain combines hacks (Rust→F), HACL/EverCrypt-style cores, and protocol analyzers like ProVerif* and CryptoVerif plus SSProve/EverParse; it finds real bugs (including a Kyber-related leak), ships as CI checks in Signal, and scales to a post‑quantum TLS prototype, while side‑channels and compiler/microarchitectural models remain open problems.
AI-written summary · about
chapters (25)
- 0:00Introduction
- 1:31Verification perspective on crypto
- 2:55TLS vulnerabilities despite scrutiny
- 4:59High-assurance crypto
- 6:24Verified crypto libraries adoption
- 8:50Verification workflow standards to proofs
- 11:39Modular multiplication pitfalls
- 16:32Verifying multiplication Low* and Veil
- 19:45Lessons verified crypto libraries
- 21:53Industry requirements verified crypto
- 24:19Verifying Rust code HACs F*
- 26:47Panic freedom Rust crypto
- 30:16LipCrypt verified implementations
- 31:40Side-channel analysis challenges
- 33:03Formal verification TLS 1.3 flaws
- 35:29Lessons METLS verification
- 37:13Modular verification Bertie TLS
- 38:56Post-quantum Signal protocol
- 43:07Protocol verification ProVerif CryptoVerif
- 47:20Cross-protocol attacks vulnerabilities
- 48:25Verification Signal development
- 51:11Making verification accessible
- 54:10Model vs code verification
- 1:00:40Post-quantum verification opportunity
- 1:02:25AI cryptographic verification
related talks
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
41mFormally Verifying Everybody's Cryptography
39mKeynote: Towards High-Assurance Cryptographic Software
58mFast Cryptographic Code via Partial Evaluation
20mFoundational Integration Verification of a Cryptographic Server
29mVale: Verifying High-Performance Cryptographic Assembly Code
48mThe Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)
23mProject Everest: Perspectives from Developing Industrial-Grade High-Assurance(…)