Verified Differential Privacy for Finite Computers
summary
Coq formalization implements the Geometric Truncated Mechanism using Coq with finprob and rat and proves both an approximate bound (Alpha Prime) and when implementations match the ideal exactly. It shows a minimum uniform size T ≥ 1 + (alpha/(1-alpha))^n for any privacy at all, and for alpha = 1/B gives exact T = (B+1)·B^n which preserves exact Alpha differential privacy. A Python prototype builds the rational CDF and runs a query in ≈0.35s for n=10,000, alpha=1/3.
AI-written summary · about
chapters (10)
- 0:00Verified differential privacy
- 1:04DP bug in real world
- 3:33Finite-precision sampling challenges
- 9:16Geometric truncated mechanism
- 12:26Uniform distribution size for privacy
- 14:35Approximate privacy loss
- 17:05Exact differential privacy
- 19:56Efficiency trade-offs in DP
- 20:59Future work in DP
- 23:47Q&A
related talks
01h 00mDifferential Privacy: Fundamentals to Forefront I
16mHow to Break, Then Fix, Differential Privacy on Finite Computers
43mDifferential Privacy Meets Robust Statistics
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
47mA Blackbox Reduction for Adaptive Adversaries using Differential Privacy
26mA Framework for Adversarial Streaming via Differential Privacy and Difference Estimators
45mAutomated Verification meets Differential Privacy
26mGeneralized Private Selection and Testing with High Confidence