Modular Verification of Probabilistic Constant-Time
summary
Proposes a call-by-contract modular proof rule for probabilistic constant-time that replaces each call with three steps: leak public input, invoke an ideal function with no leakage, then leak public output. Gives a soundness theorem: if every callee satisfies the modular constant-time contract and the replaced caller is modular constant-time then the original caller is too. Frames the result as an analogue of Canetti 2000 sequential modular composition and notes practical gaps (conditional probability reasoning missing in EasyCrypt).
AI-written summary · about
chapters (8)
- 0:00Introduction
- 0:46Constant time in crypto
- 1:51Modularity in proofs
- 3:19Function contracts
- 5:07Idealized function calls
- 8:17Connection to multi-party computation
- 10:49Future work
- 11:34Q&A
related talks
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
32mVerifying Constant-Time Implementations
15mA Modular Cost Analysis for Probabilistic Programs
27mProofs of proofs: incremental verifiability from recursion and accumulation
44mModular Approach to Cloud Security
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
15mTaming Callbacks for Smart Contract Modularity
22mCounterexample-Guided Inference of Modular Specifications