Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract)
By Michael Carl Tschantz, Dilsun Kirli Kaynar, Anupam Datta. 2011
24 citations recorded by the source corpus.
Differential privacy is a promising approach to privacy preserving data analysis with a well-developed theory for functions. Despite recent work on implementing systems that aim to provide differential privacy, the problem of formally verifying that these systems have differential privacy has not been adequately addressed. We develop a formal probabilistic automaton model of differential privacy for systems by adapting prior work on differential privacy for functions. We present the first sound verification technique for proving differential privacy of interactive systems. The technique is based on a form of probabilistic bisimulation relation. The novelty lies in the way we track quantitative privacy leakage bounds using a relation family instead of a single relation. We illustrate the proof technique on a representative automaton motivated by PINQ, an implemented system that is intended to provide differential privacy. Surprisingly, our analysis yields a privacy leakage bound of ([email protected][email protected]) rather than ([email protected][email protected]) when @e-differentially private functions are called t times. The extra leakage arises from accounting for bounded memory constraints of real computers.
Subfields: Artificial Intelligence, Sociology and Political Science
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Gilles Barthe
- Federico Olmedo
- Boris Köpf
- Santiago Zanella-B'eguelin
- David Sands
- Gerardo Schneider
- Hamid Ebadi
- Daniel Kifer
In Sociology and Political Science
- Santiago Zanella-B'eguelin
- David Sands
- Gilles Barthe
- Gerardo Schneider
- Hamid Ebadi
- Federico Olmedo
- Boris Köpf
Citations in the corpus
- Probabilistic Relational Reasoning for Differential Privacy (2013, background): “…privacy on the basis of different languages and models of computation, e.g. SQL-like languages [McSherry 2009], higher-order functional languages [Reed and Pierce 2010], imperative languages [Chaudhuri et al. 2011], the MapReduce model [Roy et al. 2010], and I/O automata [Tschantz et al. 2011].”
- Differential Privacy (2015, background): “Tschantz, Kaynar, and Datta [25] build a model and proof techniques for reasoning about interactive differential privacy with records that are input over time.”