Verified Foundations for Differential Privacy
summary
SampCert is a mechanized foundation for differential privacy written in Lean that proves correctness of sampling and DP composition and ships verified samplers into production. It features SampCert with 12,000 lines of Lean proofs, formally verified discrete Laplace and Gaussian samplers that avoid floating‑point pitfalls, an abstract DP interface supporting pure and zero‑concentrated DP, heavy re‑use of Mathlib, extraction via about 50 lines of trusted C++, and competitive deployed performance at AWS.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:22SAMERT and verified DP
- 2:29Floating-point pitfalls
- 3:31AWS Clean Rooms goals
- 4:15SAMERT architecture and Lean
- 4:58Probabilistic programming semantics
- 6:20Mass functions and verification
- 6:41Discrete Gaussian sampling
- 8:49Privacy guarantees with abstract DP
- 10:12Abstract DP interface
- 11:58Histogram privatization
- 12:39Verified programs to C++
- 14:01Performance and deployment
related talks
01h 14mTutorial: Privacy, Part II
43mPrivacy Amplification by Sampling in Practice
35mDifferential Privacy Made Practical
26mAaron Roth, Associate Professor, University of Pennsylvania, NYC 2017
09mExpanding Differentially Private Solutions: A Python Case Study
37mUser-level and federated local differential privacy
21m"SECRETS ARE LIES, SHARING IS CARING, PRIVACY IS THEFT." - A Dive into Privacy Preserving
38mDemystifying Privacy Preserving Computing