Formal Methods and Proofs of Privacy Properties, Part III
summary
Claims a practical verification path for differential privacy by encoding relational proofs into SMT solvers and using approximate probabilistic coupling rules that charge epsilon for Laplace-like steps. Demonstrates the verifier rejecting a buggy addition then accepting a fixed version, verifies a CDF+Laplace pipeline by coupling outputs, and proves a tighter guarantee for report-noisy-max using one-sided noise rather than naïve composition. Tooling from Microsoft Research automates much inference but invariants still require user guidance.
AI-written summary · about
chapters (15)
- 0:00Intro
- 2:46Example
- 12:13Wire Order
- 14:40Verification
- 19:58Differential Privacy
- 22:27Old Verification Infrastructure
- 27:28Reasoning with approximate probabilistic coupling
- 29:28Preconditions
- 33:40Noisy Max
- 34:27Onesided noisy Max
- 40:15Postconditions
- 45:28Approximate Coupling
- 48:50Sliding Property
- 50:43Noise
- 54:15Conclusion
related talks
24mRelational Symbolic Execution for Differential Privacy
45mProving Differential Privacy via Relational Types
01h 16mLaw and CS
29mPrivacy-preserving methods: Building secure projects
22mPrivacy-preserving Computation in Plain Sight
01h 00mPANEL: Statistical Theory, Privacy and Data Analysis
45mMaking Privacy Technology Accessible: Benchmarks and Platforms
30mAccuracy First: Selecting a Differential Privacy Level for Accuracy-Constrained...