Leakage-Free Probabilistic Jasmin Programs
summary
Presents a new semantic characterization of leakage-freeness for probabilistic Jasmin programs and proves it equivalent to a probabilistic relational Hoare logic formulation; shows both generalize deterministic cryptographic constant-time and are compositional. Compiles Jasmin to EasyCrypt with leakage annotations and gives an EasyCrypt proof that a Jasmin rejection-sampling implementation is leakage-free despite not being constant-time. Demonstrates automatic proof via simulation tactics for terminating programs, notes tricky cases for unbounded (no priori-termination) or non-terminating algorithms.
AI-written summary · about
chapters (15)
- 0:00Leakage-free probabilistic programs
- 2:13Jasmin workbench and side-channel attacks
- 3:40Leakage analysis in Jasmin
- 6:28Cryptographic constant time
- 9:13Semantics of leakage-free programs
- 11:41Relational Hoare logic definition
- 13:51Equivalence and compositionality
- 14:35Case study: Rejection sampling
- 16:45Non-terminating programs challenges
- 17:30Conclusions and open questions
- 17:59Q&A: Definition three and proofs
- 20:05Q&A: XTRI and variants
- 20:34Q&A: Definition two and initial state
- 21:40Q&A: Distinguishability and wiggle room
- 22:45Q&A: Non-determinism and randomness
related talks
18mPreservation of Speculative Constant-time by Compilation
18mPreservation of speculative constant-time by compilation
23mThe Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
12mLeakage models are a leaky abstraction (...)
18mHopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…)
20mPantomime: Constructive Leakage Proofs via Simulation
17mModular Verification of Probabilistic Constant-Time
26mType-directed Program Transformation for Constant-Time Enforcement