Advanced Probabilistic Couplings for Differential Privacy

Abstract

Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have been developed for the formal verification of differentially private algorithms, including program logics and type systems. However, these tools do not capture fundamental techniques that have emerged in recent years, and cannot be used for reasoning about cutting-edge differentially private algorithms. Existing techniques fail to handle three broad classes of algorithms: 1) algorithms where privacy depends accuracy guarantees, 2) algorithms that are analyzed with the advanced composition theorem, which shows slower growth in the privacy cost, 3) algorithms that interactively accept adaptive inputs. We address these limitations with a new formalism extending apRHL, a relational program logic that has been used for proving differential privacy of non-interactive algorithms, and incorporating aHL, a (non-relational) program logic for accuracy properties. We illustrate our approach through a single running example, which exemplifies the three classes of algorithms and explores new variants of the Sparse Vector technique, a well-studied algorithm from the privacy literature. We implement our logic in EasyCrypt, and formally verify privacy. We also introduce a novel coupling technique called \emph{optimal subset coupling} that may be of independent interest.

References in corpus (7)

• RAPPOR: Randomized Aggregatable Privacy-Preserving Ordinal Response
• Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds
• Privacy Odometers and Filters: Pay-as-you-Go Composition
• Coupling proofs are probabilistic product programs
• Understanding the Sparse Vector Technique for Differential Privacy
• The Large Margin Mechanism for Differentially Private Maximization
• Make Up Your Mind: The Price of Online Queries in Differential Privacy

Cited by in corpus (21)

• Deep Models Under the GAN: Information Leakage from Collaborative Deep Learning
• More Than Privacy: Applying Differential Privacy in Key Areas of Artificial Intelligence
• Detecting Violations of 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
• Guidelines for Implementing and Auditing Differentially Private Systems
• Approximate Span Liftings
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• Detecting Violations of Differential Privacy for Quantum Algorithms
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• DPGen: Automated Program Synthesis for Differential Privacy
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy
• The Sparse Vector Technique, Revisited
• Curator Attack: When Blackbox Differential Privacy Auditing Loses Its Power
• Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions
• Higher-order probabilistic adversarial computations: Categorical semantics and program logics
• Relational $\star$-Liftings for Differential Privacy
• Testing Differential Privacy with Dual Interpreters