Relational Symbolic Execution for Differential Privacy

on YouTube ↗24m

" summary

Proposes relational symbolic execution that runs paired symbolic traces and encodes Laplace sampling with an axiom that consumes an epsilon budget, turning differential-privacy checks into first-order constraints solvable by an SMT solver. Builds a tool that searches for counterexamples when verification fails, finds real bugs in Sparse Vector variants (including an infinite privacy loss when queries are not noised), reports possible false positives and requires fixed loop unroll bounds for termination.

AI-written summary · about

" chapters (6)

1. 0:00Start
2. 1:39About formal proofs of correctness
3. 2:21When the proof fails
4. 3:06What is a counterexample to e-d.p of c?
5. 4:36Symbolic Execution (a crash course)
6. 9:14Relational Symbolic Execution

" related talks

• 01h 02mFormal Methods and Proofs of Privacy Properties, Part IIIMarco Gaboardi · Data Privacy: Foundations and Applications Boot Camp
• 27mPrivacy-preserving statistical analysesElisabet Lobo-Vesga · foss-north 2020
• 16mTesting Differential Privacy with Dual InterpretersAaron Roth, Benjamin C. Pierce, Hengchu Zhang, Edo Roth, Andreas Haeberlen · OOPSLA 2020
• 30mAccuracy First: Selecting a Differential Privacy Level for Accuracy-Constrained...Katrina Ligett · Optimization, Statistics and Uncertainty
• 01h 01mFrom Theory to Practice: Crafting Differential Privacy Systems with HaskellAlejandro Russo · PEPM 2024
• 01h 16mLaw and CSKobbi Nissim · Blockchain in Society: Applications, Economics, Law, and Ethics 2019
• 42mDifferential PrivacyKunal Talwar · Uncertainty in Computation 2016
• 58mFormal Methods and Proofs of Privacy Properties, Part IMarco Gaboardi · Data Privacy: Foundations and Applications Boot Camp