Vale: Verifying High-Performance Cryptographic Assembly Code
summary
Vale converts annotated, hand-tuned assembly into an abstract syntax tree and emits machine-checked proofs verified by an SMT-based verifier, letting the AST serve as a first-class proof term that gets extracted back to assembly. The project ships a verified leakage analyzer (taint-style, explicit and implicit flow) that proves freedom from digital side channels, and verified implementations of SHA-256 (x86, ARM), Poly1305 (x64) and AES-CBC (hardware x86) that match or beat OpenSSL performance.
AI-written summary · about
chapters (22)
- 0:00Start
- 0:40Cryptography for Information Security
- 0:57Cryptographic Implementation Requirements
- 3:22OpenSSL Performance Tricks
- 4:30Our Contribution: Vale
- 5:36Key Language Constructs in Vale
- 6:40Optimization Using inline if Statements
- 7:19Example Vale Code
- 8:46Vale Architecture
- 12:21Secret Infomation Leakage
- 13:33Information Leakage Specification
- 14:39Solutions Verified Analysis
- 15:57Leakage Analysis Using Taint Tracking
- 18:13Reusing Etort from Proof of Correctness
- 18:46Lightweight Annotations for Memory Taint
- 19:36Case Studies Using Vale
- 21:03Vale versus OpenSSL: SHA-256
- 21:28Vale versus OpenSSL Poly-1305
- 22:35Verification Effort
- 23:54Conclusion
- 24:38Future Work
- 25:10Vale versus OpenSSL: AES-CBC-128
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
23mProject Everest: Perspectives from Developing Industrial-Grade High-Assurance(…)
08mEverparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers
20mFoundational Integration Verification of a Cryptographic Server
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation