Proving differential privacy in Hoare logic

Abstract

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.

Published at the Computer Security Foundations Symposium (CSF), 2014

References in corpus (1)

• A simple and practical algorithm for differentially private data release

Cited by in corpus (22)

• Privacy Loss in Apple's Implementation of Differential Privacy on MacOS 10.12
• Detecting Violations of Differential Privacy
• Proving Differential Privacy via Probabilistic Couplings
• LightDP: Towards Automating Differential Privacy Proofs
• Advanced Probabilistic Couplings for Differential Privacy
• Proving Differential Privacy with Shadow Execution
• Synthesizing Coupling Proofs of Differential Privacy
• CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
• Coupling proofs are probabilistic product programs
• Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms
• Guidelines for Implementing and Auditing Differentially Private Systems
• Approximate Span Liftings
• Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
• Differentially Private Bayesian Programming
• Detecting Violations of Differential Privacy for Quantum Algorithms
• Quantifying Program Bias
• The Complexity of Verifying Boolean Programs as Differentially Private
• Statistical Epistemic Logic
• Curator Attack: When Blackbox Differential Privacy Auditing Loses Its Power
• Divergences on Monads for Relational Program Logics
• Fifty years of Hoare's Logic
• Privacy accounting $\epsilon$conomics: Improving differential privacy composition via a posteriori bounds