Proving differential privacy via probabilistic couplings

DOI10.1145/2933575.2934554MaRDI QIDQ4635938zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.05047

Mathematics Subject Classification ID

Logic in computer science (03B70) Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 the observation that differential privacy has deep connections with a generalization of 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.

Recommendations

• LightDP: towards automating differential privacy proofs
• Probabilistic relational reasoning for differential privacy
• Proving uniformity and independence by self-composition and coupling
• Coupled relational symbolic execution for differential privacy
• \(*\)-liftings for differential privacy

Cited in

(23)

• Approximate relational Hoare logic for continuous random samplings
• Strassen's theorem for quantum couplings
• Verifying Pufferfish privacy in hidden Markov models
• Coupled relational symbolic execution for differential privacy
• Graded Hoare logic and its categorical semantics
• Model checking differentially private properties
• Higher-order approximate relational refinement types for mechanism design and differential privacy
• Probabilistic relational reasoning for differential privacy
• Deciding fast termination for probabilistic VASS with nondeterminism
• scientific article; zbMATH DE number 7234802 (Why is no real title available?)
• Relational reasoning via probabilistic coupling
• \(*\)-liftings for differential privacy
• Relational -liftings for differential privacy
• Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
• Coupling proofs are probabilistic product programs
• LightDP: towards automating differential privacy proofs
• Divergences on monads for relational program logics
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• On Lexicographic Proof Rules for Probabilistic Termination
• Proving that programs are differentially private
• On lexicographic proof rules for probabilistic termination
• The complexity of verifying loop-free programs as differentially private
• A linear type system for L^p-metric sensitivity analysis

This page was built for publication: Proving differential privacy via probabilistic couplings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635938)