Foundational Integration Verification of a Cryptographic Server
summary
A verified bare-metal garage-door server implements authenticated open/close commands and prevents replays by rotating seeds, and a single machine-checked end-to-end theorem from curve math to RISC-V proves total correctness, liveness, and static memory bounds. The stack stitches Fiat Crypto, Coq proofs, Bedrock2, Rupicola, and four compilers into a canceling-semantics pipeline, and performance measurements show the verified Bedrock2 path is slowest — about 47s vs 2s per interaction when replaced by GCC.
AI-written summary · about
chapters (10)
- 0:00Cryptographic server verification intro
- 2:12End-to-end theorem benefits
- 4:41Simple specs guiding principle
- 6:30System demo with garage door
- 7:32Top-level theorem IO trace
- 9:39Proof techniques tour
- 13:37Component compilation integration
- 15:46Performance bottlenecks
- 16:50Conclusion results summary
- 17:35Q&A
related talks
58mFast Cryptographic Code via Partial Evaluation
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
41mFormally Verifying Everybody's Cryptography
29mVale: Verifying High-Performance Cryptographic Assembly Code
01h 08mProviding evidence for the security properties of hardware/software codesigns
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
01h 25mIntroduction to Verifiable Computing