Verifying Constant-Time Implementations
summary
Claims an automated verifier, ct-verif, that proves constant-time for optimized LLVM code by reducing the two-execution security property to safety of a product program via selective self-composition (cross-product plus limited self-composition where declassification occurs). Implementation uses SMACK and Boogie, is cross‑platform, and verifies real-world APIs from NaCl, OpenSSL and FourQ. Formal reduction is machine‑checked in Coq. Prototype runs successfully on a wide set of cryptographic and arithmetic components, handling benign local constant‑time violations.
AI-written summary · about
chapters (24)
- 0:00Intro
- 0:22OVERVIEW
- 0:54PROGRAM LEAKAGE
- 1:22LEAKING SECRETS
- 2:53FLOW SECURITY
- 3:14TIMING ATTACKS
- 6:19CONSTANT PATH
- 7:43MEMORY CACHE
- 8:48OPERAND SIZE
- 9:50CODING RULES
- 11:05PROGRAMMABILITY?
- 11:53VERIFICATION
- 13:30CONSTANT TIME
- 15:27APPROACH
- 16:13SELF COMPOSITION
- 18:02HARD FOR VERIFIERS
- 19:02CROSS PRODUCT
- 22:42EXPERIMENTS
- 23:06RELATED TOOLS
- 23:29LLVM ASSEMBLY
- 24:26CONCLUSION
- 25:10IMPLEMENTATION
- 28:01INSTRUCTION CACHE
- 28:44HYBRID PRODUCT
related talks
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
24mA CompCert Compiler that Preserves Cryptographic Constant-time
21mWhen Obfuscations Preserve Cryptographic Constant-Time
18mPreservation of Speculative Constant-time by Compilation
23mRobust Constant-Time Cryptography
18mPreservation of speculative constant-time by compilation
32mFaCT: A New Language for Constant-Time Programming
17mRobust Constant-Time Cryptography