Separation Logics for Probability, Concurrency, and Security
summary
Presents concrete logics that extend Iris + Rocq to reason about randomized, higher‑order, concurrent code: unary Errors with an error credit resource that upper‑bounds collision probabilities, a binary Approxis for approximate relational equivalence, and concurrent variants Canerys/Foxtrot. Implements Merkle trees, an unreliable storage system, a concurrent Bloom filter with provable false‑positive bounds, and a libsodium sampler proven contextually equivalent to an ideal sampler. Works for many real examples but current concurrency schedulers are too powerful for some security proofs, so restricted schedulers are next.
AI-written summary · about
chapters (15)
- 0:00Verifying security infrastructure
- 1:05Password storage challenges
- 3:10Verifying security programs
- 6:01Probabilistic program verification
- 7:48Probabilistic extensions of Iris
- 8:31Hash function specifications
- 9:37Error credits in separation logic
- 11:26Error bounds for hash functions
- 12:33Relational properties and refinement
- 14:22Concurrent probabilistic programs
- 15:45Concurrent probabilistic reasoning
- 16:31Verifying concurrent data structures
- 17:36Password storage system verification
- 18:40Scheduler model limitations
- 20:04Conclusion and future work
related talks
26mCryptis: Cryptographic Reasoning in Separation Logic
20mAsynchronous Probabilistic Couplings in Higher-Order Separation Logic
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
16mCerisier: A Program Logic for Attestation in a Capability Machine
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
19mA quantitative probabilistic relational Hoare logic
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
43mConcurrency Abstractions for Application Security