Proving Differential Privacy via Relational Types
Talkat Data Privacy: From Foundations to Applications (Simons Institute workshop, 2019) · 2019-03-04..03-08·
summary
A relational dependent type system (implemented as LightDP and extended as ShadowDP) converts probabilistic programs into non‑deterministic targets that track a special budget variable V_epsilon and replace sampling with havoc plus cost updates; verified examples include sparse vector and report‑noisy‑max (tight epsilon bound) using off‑the‑shelf model checkers. The prototype is open source, needs only light annotations on sampling, typechecks and model‑checks quickly, and has a soundness theorem guaranteeing epsilon‑DP when the target proves V_epsilon ≤ ε.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:41Programming Tools for DP
- 3:03But, sophisticated algorithms require more advanced proofs
- 7:04Approach Overview
- 10:15(Pure) Differential Privacy
- 11:49Randomness Alignment Key idea: construct an injective relation between points on two distributions
- 14:58Relational Types in LightDP
- 15:58Dependent Types in LightDP Can be a program expression
- 17:38Randomness Alignment in Language-Based Proof Memory: mapping from variables to values Initial memory
- 20:22Type System
- 22:33Target Language
- 24:27Putting Together The Sparse Vector Technique
- 24:47Required Annotations
- 26:28Completing the Proof
- 29:24Report Noisy Max
- 30:30Randomness Alignment of Noisy Max
- 35:10Randomness Alignment with Shadow Execution
- 38:28Usefulness of ShadowDP
- 39:32Goals Revisited Proving Differential Privacy via Shadow Execution ACM conference on Programming Language Design and implementation, 2019
- 40:16Verification Using ShadowDP
- 40:54Summary
related talks
19mPractical Considerations for Differential Privacy
01h 01mFrom Theory to Practice: Crafting Differential Privacy Systems with Haskell
01h 02mFormal Methods and Proofs of Privacy Properties, Part III
33mHeterogeneity and Privacy in Modern Learning
01h 00mPANEL: Statistical Theory, Privacy and Data Analysis
50mPrivacy Amplification by Sampling and Renyi Differential Privacy
26mAaron Roth, Associate Professor, University of Pennsylvania, NYC 2017
17mPrivacy in Theory, Bugs in Practice: Grey-Box Testing for Differential Privacy Libraries