Formal Modelling of Information-flow Control Systems: Some Lessons Learned
Talkat Data Privacy: From Foundations to Applications (Simons Institute workshop, 2019) · 2019-03-04..03-08·
summary
Proposes replacing a global privacy budget with per-user privacy budgets and implements a dynamic enforcement system that tracks provenance-tracking for every record to charge individual epsilons; builds a PINQ-style runtime that deducts budget and silently drops records whose budget is exhausted. Formal models and proofs reveal the system is initially broken but fixable: general joins make the deletion step have joins cause unbounded sensitivity, so the implementation must restrict operators (similar limits to PINQ) and prove privacy for every finite output-prefix.
AI-written summary · about
chapters (15)
- 0:00Start
- 5:08An Example
- 7:31PINQ [McSherry]
- 9:28Problem 1: Wasteful Global Budget
- 11:15Problem 2: Continuous Data
- 12:38Personalised Differential Privacy (PDP) 1. Generalise DP: each individual has their
- 16:02ProPer in Action
- 18:08The Catch
- 18:49Solution
- 20:15Dropping records
- 26:01Some Cautionary Tales from Secure Information Flow
- 29:31Information Erasure
- 34:20Lesson: Generalise as needed but avoid "tweaking"
- 37:17Featherweight PINQ
- 38:05Conclusions
related talks
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
29mVerifying Pufferfish Privacy in Hidden Markov Models
29mPrivacy-preserving methods: Building secure projects
01h 08mTutorial: Security
32mSubstructural Information Flow via Polymorphism
22mEnhancing Privacy through an Interactive On-demand Incremental Information
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
51mPrivacy Engineering : The State of The Art