Formally Verifying Everybody's Cryptography
summary
Production TLS and crypto libraries get formal, with real code verified against machine-readable Cryptol specifications using symbolic execution at the LLVM level and off‑the‑shelf SMT solvers. Results include equivalence proofs and guarantees of absence of crashes for HMAC, SHA, AES‑GCM, ECDSA and library builds like s2n AWS‑lc and blst. The workflow shows which optimizations need lemmas, where uninterpreted functions and rewriting rescue a stuck solver, and when full proofs are practical.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:28Aim: formal verification of code
- 1:16This talk: cryptographic primitives
- 3:46Who did the proofs, anyway?
- 4:27We do difficult proofs
- 5:48Threat model for cryptographic primitives
- 8:23So, verification is just fancy testing
- 14:53Result-high confidence of this
- 16:04Verifying cryptography is easy! (in some ways)
- 18:18Conservation of difficulty rule
- 18:59Why is it difficult to verify cryptography?
- 20:58Verifying cryptography is difficult, as well
- 23:12Changing the code is very powerful during formal verification!
- 26:10Rewrites in practice (from SHA 384)
- 29:10Composition has a cost
- 32:13Cumulative Correctness planning
related talks
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
39mKeynote: Towards High-Assurance Cryptographic Software
29mVale: Verifying High-Performance Cryptographic Assembly Code
39mFormal specification of attestation mechanisms in Confidential Computing
32mVerifying Constant-Time Implementations
20mFoundational Integration Verification of a Cryptographic Server
32mBlack box side-channel leakage verification using statistical approach