Proving Differential Privacy in Hoare Logic

By Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub. 2014

72 citations recorded by the source corpus.

Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use. We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach transforms a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy.

Subfields: Artificial Intelligence, Program Analysis & Verification, Privacy & Security

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 Program Analysis & Verification

In Privacy & Security

Citations in the corpus

Detecting Violations of Differential Privacy (2018, background): “On the other hand, static methods exist for verifying that a program obeys differential privacy during any execution, based on relational program logic [1–7] and relational type system [24, 35, 41].”
Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “…[24, 36], relational program logic [2, 6] and relational reﬁnement type systems [9], linear (dependent) type systems [29, 42], product programs [7], meth-ods based on computing bisimulations families for probabilistic automata [50, 51], and methods based on counting variants of satis-ﬁability…”
Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “Over the last 25 years, researchers have developed a wide variety of tools for reasoning about probabilistic liftings, explored applications in numerous areas including security and biology, and uncovered deep connections with the Kantorovich metric and the theory of optimal transport (for a survey,”
Proving differential privacy with shadow execution (2019, result): “, [6–10]) was concerned with increasing expressiveness.”
Coupling proofs are probabilistic product programs (2016, background): “[11] define a specialized product construction from probabilistic programs to deterministic programs, so that the original program is differentially private, provided its deterministic product program satisfies some Hoare specification.”
A Program Logic for Union Bounds (2016, unknown): “This is a useful reduction that also applies to other lightweight logics [5].”
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 ǫ ′ .”
Property Testing For Differential Privacy (2018, methodology): “There is a line of work (Barthe et al., 2014, Roy et al., 2010, Reed and Pierce, 2010, Gaboardi et al., 2013, Tschantz et al., 2011, Barthe et al., 2012, 2013, McSherry, 2009) using logical arguments (type systems, I/O automata, Hoare logic, etc.) to verify privacy.”
Synthesizing coupling proofs of differential privacy (2017, background): “[5], who, like Zhang and Kifer [45], use product constructions for proving differential privacy.”
LightDP: towards automating differential privacy proofs (2016, methodology): “Except the very recent work by Barthe et al. (2016c,b), existing formal methods (e.g., (Reed and Pierce 2010; Gaboardi et al. 2013; Barthe et al. 2012, 2014)) rely on the composition theorem, hence fail to prove that the Sparse Vector method satisfies ′-privacy for any ′.”