Formal Methods and Proofs of Privacy Properties, Part II
summary
Language called PINQ implements privacy by creating chained agents that track budget and apply Laplace noise to counts after checking budget and throwing an exception if insufficient. A filtering where transformation has sensitivity = 1, so noise scale is epsilon inverse times that sensitivity. An alternative line builds a static type checker using metric-space nonexpansive typing to infer sensitivities before running, enabling budget planning and compositional proofs but sacrificing some expressivity (no exponential mechanism) and leaving runtime side channels and formalization of PINQ tricky.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:37Pink implementation
- 8:51Noise implementation
- 11:33Pink
- 16:13Runtime Systems
- 17:55Pink and Rabbit
- 18:37Why
- 19:57Issues
- 23:28Approach
- 25:39Semantic Model
- 35:05Static Check
- 44:01Data Analysis
- 46:59Usability
- 50:53Programming Language Design
related talks
39mPufferfish Privacy Mechanisms for Correlated Data
29mVerifying Pufferfish Privacy in Hidden Markov Models
45mMaking Privacy Technology Accessible: Benchmarks and Platforms
24mRelational Symbolic Execution for Differential Privacy
29mPrivacy-preserving methods: Building secure projects
16mBalancing Privacy: Leveraging Privacy Budgets for Privacy-Enhancing Technologies
43mPufferfish Privacy Mechanisms for Correlated Data
01h 00mDifferential Privacy: Fundamentals to Forefront I