Testing Differential Privacy with Dual Interpreters
summary
An automated tester called DPCheck converts a common DP proof pattern into a hybrid test that combines instrumented concrete traces and symbolic execution, encoding constraints to the SMT solver Z3. It flags distinctions between correct and buggy variants across a comprehensive benchmark suite and successfully analyzes a previously unchecked complex algorithm PrivTree. A case study rewrites and extracts the core mechanism of the Disclosure Avoidance System DAS to Python3 and integrates it; the tool works but SMT solving becomes a bottleneck as sample counts grow.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:11Differential Privacy Deployments
- 1:25Landscape of Checking Differential Privacy Proofs
- 4:09DPCheck: Automated Testing of Differential Privacy
- 4:48Review of Differential Privacy
- 6:01What is Differential Privacy?
- 6:58An Example Algorithm
- 7:48A Proof Technique for DP
- 10:19Use the same technique for testing!
- 12:47Evaluation on Benchmark Algorithms
- 13:29Evaluation on Disclosure Avoidance System (DAS) United States
related talks
17mPrivacy in Theory, Bugs in Practice: Grey-Box Testing for Differential Privacy Libraries
24mRelational Symbolic Execution for Differential Privacy
20mSuperDP: Differential Privacy Refutation via Supermartingales
13mEvaluating the Usability of Differential Privacy Tools with Data Practitioners
01h 01mFrom Theory to Practice: Crafting Differential Privacy Systems with Haskell
01h 02mFormal Methods and Proofs of Privacy Properties, Part III
45mProving Differential Privacy via Relational Types
47mDeploying DP: Experiences from the Front Lines and Open Challenges