Proving Differential Privacy via Probabilistic Couplings

By Gilles Barthe, Marco Gaboardi, Benjamin Gr'egoire, Justin Hsu, Pierre-Yves Strub. 2016

110 citations recorded by the source corpus.

Over the last decade, differential privacy has achieved widespread adoption within the privacy community. Moreover, it has attracted significant attention from the verification community, resulting in several successful tools for formally proving differential privacy. Although their technical approaches vary greatly, all existing tools rely on reasoning principles derived from the composition theorem of differential privacy. While this suffices to verify most common private algorithms, there are several important algorithms whose privacy analysis does not rely solely on the composition theorem. Their proofs are significantly more complex, and are currently beyond the reach of verification tools.In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on deep connections between differential privacy and probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by a coupling argument.We demonstrate our methods on two algorithms: the Exponential mechanism and the Above Threshold algorithm, the critical component of the famous Sparse Vector algorithm. We verify these examples in a relational program logic apRHL+, which can construct approximate couplings. This logic extends the existing apRHL logic with more general rules for the Laplace mechanism and the one-sided Laplace mechanism, and new structural rules enabling pointwise reasoning about privacy; all the rules are inspired by the connection with coupling. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community.

Subfields: Artificial Intelligence, Sociology and Political Science, Privacy & Security, Information Theory

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 Sociology and Political Science

In Privacy & Security

In Information Theory

Citations in the corpus

The Privacy Blanket of the Shuffle Model (2019, methodology): “We address this challenge by leveraging a characterization of differential privacy in terms of hockey-stick divergences that originated in the formal methods community to address the verification for differentially private programs [5, 4, 3] and has also been used to prove tight results on privacy a”
Detecting Violations of Differential Privacy (2018, methodology): “, variants of the noisy max algorithm [5, 19] and the histogram algorithm [14]).”
Privacy Loss in Apple's Implementation of Differential Privacy on MacOS 10.12 (2017, background): “It has been observed that properly implementing algorithms claiming to preserve differential privacy is non-trivial in practice [4, 5, 13].”
Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “Barthe et al. [10] work with the relational program logic apRHL [6], extended with a new composition principle called pointwise privacy .”
Proving differential privacy with shadow execution (2019, methodology): “, [8, 42]), we assume a subdistribution instead of a distribution, since sub-distribution gives rise to an elegant program semantics in face of non-terminating programs [28].”
A Program Logic for Union Bounds (2016, unknown): “The diﬀerential privacy property of Sparse Vector was recently formally veriﬁed [8]; here, we consider the accuracy property.”
LightDP: towards automating differential privacy proofs (2016, methodology): “With the exception of (Barthe et al. 2016c,b), most existing formal methods rely on the composition theorem (McSherry 2009).”
AutoPriv: Automating Differential Privacy Proofs (2016, methodology): “Except the very recent work by Barthe et al. (2016), all existing formal methods (e.g., (Reed and Pierce 2010; Gaboardi et al. 2013; Barthe et al. 2012, 2014)) solely rely on the composition theorem, hence fail to prove that the Sparse Vector method satisfies ǫ ′ privacy for any ǫ ′ .”
Differentially Private Testing of Identity and Closeness of Discrete Distributions (2017, background): “[9, 8] characterize differential privacy through a coupling argument.”
Coupling proofs are probabilistic product programs (2016, background): “[15] extend the connection to approximate couplings in approximate probabilistic relational Hoare logic (apRHL), introduced for reasoning about differentially private computations [7], and exploit this connection to prove differential privacy of several examples that had previously been beyond the r”
Synthesizing coupling proofs of differential privacy (2017, background): “Researchers have explored a broad array of techniques for static verification of differential privacy, including linear and dependent type systems [6, 19, 24, 39, 45], relational program logics [4, 7, 10], partial evaluation [44], and more.”