Keynote: Towards High-Assurance Cryptographic Software
summary
Formal verification and security-oriented languages are used end-to-end: mechanized proofs (ProVerif, Tamarin, F, EasyCrypt) validate protocol designs like HPKE and the tree-based key management in MLS draft 20; verified implementations (F, Low, Jasmine) feed into a combined Rust-facing library called lip Crux that bundles HACL and others. Hack-spec, a small subset of Rust, acts as an executable spec that compiles to F*/EasyCrypt, preserves preconditions (secret vs public), and yields code that matches specs and often matches or beats OpenSSL performance.
AI-written summary · about
chapters (8)
- 0:00High-assurance crypto software intro
- 3:52Formal verification in crypto design
- 7:21HPKE standard
- 8:45TreeKEM and MLS key management
- 15:21Verified crypto libraries
- 23:00HACSpec for crypto specs
- 31:02Integrating verified crypto
- 37:02Conclusion and future
related talks
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
01h 04mSoftware Verification meets Real-World Cryptography
41mFormally Verifying Everybody's Cryptography
01h 34mIntro to Cryptol and High Assurance Crypto Engineering
26mBuilding Private And Secure Applications Easily Using The Sunscreen FHE Compiler&Rust
47mHigh-Assurance Go Cryptography
23mProject Everest: Perspectives from Developing Industrial-Grade High-Assurance(…)
18mHopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…)