Proving Differential Privacy via Probabilistic Couplings

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.

References in corpus (5)

• Relational reasoning via probabilistic coupling
• Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation
• On the Privacy Properties of Variants on the Sparse Vector Technique
• Understanding the Sparse Vector Technique for Differential Privacy
• Computer-aided verification in mechanism design

Cited by in corpus (32)

• Privacy Loss in Apple's Implementation of Differential Privacy on MacOS 10.12
• Detecting Violations of Differential Privacy
• Advanced Probabilistic Couplings for Differential Privacy
• Proving Differential Privacy with Shadow Execution
• Synthesizing Coupling Proofs of Differential Privacy
• Proving Expected Sensitivity of Probabilistic Programs
• CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
• Coupling proofs are probabilistic product programs
• Relational Proofs for Quantum Programs
• Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms
• Approximate Relational Hoare Logic for Continuous Random Samplings
• Guidelines for Implementing and Auditing Differentially Private Systems
• Differentially Private Bayesian Programming
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• Detecting Violations of Differential Privacy for Quantum Algorithms
• DPGen: Automated Program Synthesis for Differential Privacy
• A novel analysis of utility in privacy pipelines, using Kronecker products and quantitative information flow
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• The Complexity of Verifying Boolean Programs as Differentially Private
• Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy
• Lexicographic Ranking Supermartingales with Lazy Lower Bounds
• The Sparse Vector Technique, Revisited
• The Complexity of Verifying Loop-Free Programs as Differentially Private
• Fuzzi: A Three-Level Logic for Differential Privacy
• Differential Privacy in Cognitive Radio Networks: A Comprehensive Survey
• Free Gap Information from the Differentially Private Sparse Vector and Noisy Max Mechanisms
• Verifying Pufferfish Privacy in Hidden Markov Models
• Divergences on Monads for Relational Program Logics
• Testing Differential Privacy with Dual Interpreters
• Privacy accounting $\epsilon$conomics: Improving differential privacy composition via a posteriori bounds
• Proving Almost-Sure Termination of Probabilistic Programs via Incremental Pruning
• Relational $\star$-Liftings for Differential Privacy