Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
summary
Claims a program logic that encodes privacy budget as resource inside a probabilistic higher-order separation logic, proves an adequacy theorem linking the internal predicate to external differential privacy, and isolates probabilistic reasoning so deterministic steps use standard rules. Implements a verified library (including an online Sparse Vector Technique and a privacy filter inspired by OpenDP), reasons about Laplace-like discrete sampling with pre-sampling tapes, and formalizes everything in the Rocq Prover; artifacts are reusable.
AI-written summary · about
chapters (12)
- 0:00Differential privacy goals
- 1:46Noise mechanisms for privacy
- 4:15Verifying randomized programs
- 7:49Clutch DP separation logic
- 9:59Hoare quadruples and credits
- 12:07Differential privacy notion
- 13:52Logic to semantics theorem
- 14:55Compositional privacy reasoning
- 16:20Laplacian sampling rules
- 17:46Above threshold verification
- 18:30Summary and references
- 19:13Q&A
related talks
45mAutomated Verification meets Differential Privacy
20mAsynchronous Probabilistic Couplings in Higher-Order Separation Logic
48mFormal Modelling of Information-flow Control Systems: Some Lessons Learned
28mProving Obliviousness of Probabilistic Algorithms with Formal Verification
54mVerification Dilemmas, Law, and the Promise of Zero-Knowledge Proofs
27mVerified Differential Privacy for Finite Computers
17mModular Verification of Probabilistic Constant-Time
15mNecessary Conditions in Multi-Server Differential Privacy