The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
summary
Coq is used to connect Hacspec, Jasmin and SSProve into an automated pipeline that produces: a functional Hacspec spec, an imperative SSProve spec, and mechanized proofs of their Hacspec ↔ SSProve translation validation. Jasmin code is translated to SSProve with a proved Jasmin→SSProve semantics preservation (so compiled assembly inherits properties). The system delivers an end-to-end Coq proof of AES with hardware acceleration, plus NC-CPA security reasoning; the translations and proofs are fully mechanized and applied to a real AES implementation.
AI-written summary · about
chapters (11)
- 0:00End-to-end cryptography verification
- 1:35Verification framework
- 3:01Haxe in the framework
- 4:06SSProve for proofs
- 6:35Jasmin cryptography language
- 9:05One-time pad example
- 11:11Security properties and game hopping
- 13:24Framework summary
- 14:05Evaluating on AES
- 17:16Conclusion
- 18:19Q&A
related talks
58mFast Cryptographic Code via Partial Evaluation
41mFormally Verifying Everybody's Cryptography
31mMachine-checking post-quantum cryptography
18mPreservation of Speculative Constant-time by Compilation
29mVale: Verifying High-Performance Cryptographic Assembly Code
01h 04mSoftware Verification meets Real-World Cryptography
01h 08mProviding evidence for the security properties of hardware/software codesigns
39mKeynote: Towards High-Assurance Cryptographic Software