Formal Verification of Differential Privacy for Interactive Systems

By Michael Carl Tschantz, Dilsun Kirli Kaynar, Anupam Datta. 2011

46 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. This paper presents the first results towards automated verification of source code for differentially private interactive systems. We develop a formal probabilistic automaton model of differential privacy for systems by adapting prior work on differential privacy for functions. The main technical result of the paper is a sound proof technique based on a form of probabilistic bisimulation relation for proving that a system modeled as a probabilistic automaton satisfies differential privacy. 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. To make our proof technique easier to apply to realistic systems, we prove a form of refinement theorem and apply it to show that a refinement of the abstract PINQ automaton also satisfies our differential privacy definition. Finally, we begin the process of automating our proof technique by providing an algorithm for mechanically checking a restricted class of relations from the proof technique.

Subfields: Artificial Intelligence, Information Systems, 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

In Information Systems

In Sociology and Political Science

Citations in the corpus

Detecting Violations of Differential Privacy (2018, background): “Several dynamic tools [21, 29, 37, 39, 40] exist for enforcing differential privacy.”
Proving Differential Privacy in Hoare Logic (2014, background): “Differentially private algorithms are typically built from two constructions:private mechanisms, which add probabilistic noise to their input, andcomposition, which combines differentially private operations into a single one.”
Proving differential privacy with shadow execution (2019, background): “However, along with other work such as computing bisimulations families for probabilistic automata [39, 41], they fail to provide a tight bound on the privacy cost of sophisticated algorithms.”
Differential Privacy by Typing in Security Protocols (2013, background): “[32] showed how to verify differential privacy properties based on I/Oautomata.”
LightDP: towards automating differential privacy proofs (2016, methodology): “There are also methods based on computing bisimulations families for probabilistic automata (Tschantz et al. 2011; Xu et al. 2014).”
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].”
Property Testing For Differential Privacy (2018, methodology): “Several algorithms and tools have been proposed for formal verification of the DP guarantee of an algorithm (6, 27, 26, 20, 29, 6, 27, 26, 20, 29, 7, 5, 23).”