Keynote: Bringing Verified Cryptographic Protocols to Practice
summary
A toolchain produces provably secure, interoperable protocol implementations: a type-based verifier Owl yields computationally sound proofs, an SMT-backed verifier Varys checks Rust refinements against interaction-tree specs, and a verified crypto library EverCrypt plus a parser generator (Vest) supply fast, side‑channel–aware primitives. Case studies: verified TLS/WASM parsers, 2× faster Bitcoin parsing, certificate validation over 10M certs that matches browsers while being 2–3 orders faster and using 3 orders less memory, and WireGuard whose verified Rust implementation meets unverified baselines.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:03Cryptographic protocol complexity
- 3:08Goals for verified replacements
- 4:11Verified parsers with Vest
- 7:25EverCrypt provider overview
- 10:34Verifying cryptographic certificates
- 14:25Challenges in verification
- 17:52Owl protocol verification tool
- 21:42Encoding security goals in Owl
- 24:51Cryptographic reductions and types
- 28:41Compiling Owl to Rust
- 34:15Preventing side-channel leaks
- 38:07Verifying WireGuard with Owl
- 41:16Performance of verified code
- 42:20Future directions
- 43:22Summary
- 43:52Q&A
related talks
01h 04mSoftware Verification meets Real-World Cryptography
39mKeynote: Towards High-Assurance Cryptographic Software
41mFormally Verifying Everybody's Cryptography
13mOwlC: Compiling Security Protocols to Verified, Secure...
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
20mFoundational Integration Verification of a Cryptographic Server
48mThe Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)
29mVale: Verifying High-Performance Cryptographic Assembly Code