Formalization of Differential Privacy in Isabelle/HOL
summary
Provides a reusable Isabelle/HOL library that formalizes differential privacy over continuous probability distributions, including the standard ε,δ definition, postprocessing and composition lemmas, and a mechanized Laplace mechanism proof that uses sensitivity to get ε-differential privacy. It also formalizes report noisy max and proves the stronger claim that its privacy bound is ε-only regardless of m, with the formal proof about 1,500 lines (discrete proofs exceed ~1,000 lines). Development builds on Isabelle/HOL’s probability library and the GD monad.
AI-written summary · about
chapters (16)
- 0:00Differential privacy intro
- 3:37Differential privacy definition
- 7:01Laplace mechanism formalized
- 9:59Report Noisy Max proof
- 12:04Isabelle/HOL continuous setting
- 15:39Probability library usage
- 16:42Differential privacy formalized
- 18:05Basic DP properties
- 20:17Laplace distribution formalized
- 21:44Laplace proof implementation
- 23:13Datasets and adjacency metrics
- 23:56Report Noisy Max formalized
- 24:41Conclusion and future work
- 26:05Q&A: Report Noisy Max complexity
- 27:29Q&A: Program logic for DP
- 28:38Q&A: Coq or Lean formalization
related talks
20mSuperDP: Differential Privacy Refutation via Supermartingales
22mFormalising Oblivious Transfer in CryptHOL
28mDeciding Accuracy of Differential Privacy Schemes
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
16mTesting Differential Privacy with Dual Interpreters
13mChecking $\delta$-Satisfiability of Reals with Integrals
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
05mOn Iteration in Discrete Probabilistic Programming