Watch a 23-minute conference presentation from POPL 2018 exploring an automated technique for verifying ε-differential privacy in randomized algorithms. Learn about coupling strategies, a novel proof technique that frames differential privacy verification as a resource-limited game. Discover how researchers developed a constraint-based approach using Horn modulo couplings (HMC) to solve these verification challenges. Follow along as the speakers demonstrate their implementation in the FairSquare verifier and showcase successful automated privacy proofs for complex algorithms like Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism. Gain insights into how this push-button verification method combines first-order Horn clauses with probabilistic constraints to advance differential privacy verification.
Overview
Syllabus
[POPL'18] Synthesizing Coupling Proofs of Differential Privacy
Taught by
ACM SIGPLAN
Related Courses
-
Randomized Approach for Tight Privacy Accounting in Differential Privacy
-
A Short Tutorial on Differential Privacy
-
Private Convex Optimization via Exponential Mechanism - Differential Privacy for Machine Learning
-
Efficient Mean Estimation with Pure Differential Privacy via a Sum-of-Squares Exponential Mechanism
-
A Blackbox Reduction for Adaptive Adversaries Using Differential Privacy
-
Less is More: Revisiting the Gaussian Mechanism for Differential Privacy
