Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
summary
Formal definition of cryptographic constant‑time for languages with compiler‑resolved nondeterminism using omnisemantics and single‑copy assertions, mechanized in Coq. Proof shows a Bedrock2 C subset compiled to RISC‑V preserves constant‑time, gives two equivalent treatments of compiler‑resolved nondeterminism (e.g., stack allocation) and explains subtle contract differences. Results compose: source proofs + compiler theorem yield machine‑code constant‑time, and artifacts (proofs, compiler, examples) are available and evaluated.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:23Cryptographic constant time
- 1:48Project goals and theorem
- 2:52Nondeterminism in programs
- 3:37Bedrock 2 overview
- 4:39Omnismantics for languages
- 6:01Omnismantics simplifies proofs
- 8:07Constant time for deterministic
- 9:32Single-copy constant time
- 11:17Constant time for nondeterministic
- 13:49Compiler-resolved nondeterminism
- 15:55Approaches to constant time
- 16:42Leakage and declassification
- 17:46Equivalence to hyperproperties
- 18:50Bad idea vs option two
- 19:33Generalizing to hyperproperties
- 20:37Relation to non-interference
- 21:22Q&A
related talks
32mVerifying Constant-Time Implementations
23mRobust Constant-Time Cryptography
18mPreservation of Speculative Constant-time by Compilation
24mA CompCert Compiler that Preserves Cryptographic Constant-time
18mPreservation of speculative constant-time by compilation
21mWhen Obfuscations Preserve Cryptographic Constant-Time
17mModular Verification of Probabilistic Constant-Time
23mCorrect Compilation of Concurrent C Code