Probabilistic relational reasoning for differential privacy

By Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-B'eguelin. 2012

237 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Probabilistic & Bayesian Methods, 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 Probabilistic & Bayesian Methods

In Privacy & Security

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, background): “Verification techniques, on the other hand, allow programmers to implement a wider variety of algorithms and verify proofs of correctness (written by the developers) [2–7] or synthesize most (or all) of the proofs [1, 24, 35, 41].”
Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “…privacy seems to be a straight-forward property about probabilities in two distributions, a recent line of work initiated by Barthe et al. [6] and subsequently developed [2, 10] shows that differential privacy is a consequence of an approximate version of probabilistic coupling, called…”
Proving Differential Privacy via Probabilistic Couplings (2016, positive): “Our program logic apRHL extends apRHL, a relational Hoare logic that has been used to verify many examples of differentially private algorithms (Barthe et al. 2013).”
Proving Differential Privacy in Hoare Logic (2014, methodology): “apRHL [11] is a quantitative, probabilistic and relational program logic for reasoning about differential privacy, wi th judgments of the form3 ⊢ c1 ∼〈α,δ〉 c2 : Ψ =⇒ Φ, where c1 and c2 are probabilistic programs, Ψ and Φ are memory relations, andǫ, δ are real values.”
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 ′.”
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).”
Relational Symbolic Execution (2017, background): “Several safety and security properties can be described as relational properties: non-interference Goguen and Meseguer (1982), Goguen and Meseguer (1984), compiler optimizations Benton (2004), sensitivity and continuity analysis Chaudhuri et al.”
DStress: Efficient Differentially Private Computations on Distributed Data (2017, methodology): “The second limitation currently prevents ad-hoc queries, but we speculate that DStress could be augmented with automated sensitivity inference, e.g., using linear type systems [31, 38] or a system like CertiPriv [4].”
Coupling proofs are probabilistic product programs (2016, background): “[7] develop an approximate variant of probabilistic Relational Hoare Logic, and verify differential privacy of several algorithms.”
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.”
Differential Privacy by Typing in Security Protocols (2013, background): “have presented CertiPriv [5], a machinechecked framework for reasoning about differential privacy built on top of the Coq proof assistant.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, background): “Nonfunctional and data-centered properties [25, 60, 61] can also benefit from formal verification [6], but more research is necessary both on manual and automated approaches to verifying such properties.”
Proving differential privacy with shadow execution (2019, background): “, [6–10]) was concerned with increasing expressiveness.”
Verifiable differential privacy (2015, methodology): “[18] shows that some of these limitations can be removed by extending the type system; also, analysts with more expertise in differential privacy could use a system like CertiPriv [2] to complete the proof manually.”