Proving Differential Privacy with Shadow Execution

Abstract

Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two requires substantial changes to program logics: one recent paper is able to verify Report Noisy Max automatically, but it involves a complex verification system using customized program logics and verifiers. In this paper, we propose a new proof technique, called shadow execution, and embed it into a language called ShadowDP. ShadowDP uses shadow execution to generate proofs of differential privacy with very few programmer annotations and without relying on customized logics and verifiers. In addition to verifying Report Noisy Max, we show that it can verify a new variant of Sparse Vector that reports the gap between some noisy query answers and the noisy threshold. Moreover, ShadowDP reduces the complexity of verification: for all of the algorithms we have evaluated, type checking and verification in total takes at most 3 seconds, while prior work takes minutes on the same algorithms.

23 pages, 12 figures, PLDI'19

References in corpus (12)

• RAPPOR: Randomized Aggregatable Privacy-Preserving Ordinal Response
• Renyi Differential Privacy
• A simple and practical algorithm for differentially private data release
• Detecting Violations of Differential Privacy
• Proving Differential Privacy via Probabilistic Couplings
• LightDP: Towards Automating Differential Privacy Proofs
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• Proving differential privacy in Hoare logic
• Advanced Probabilistic Couplings for Differential Privacy
• Proving Differential Privacy with Shadow Execution
• Synthesizing Coupling Proofs of Differential Privacy
• Ektelo: A Framework for Defining Differentially-Private Computations

Cited by in corpus (13)

• Proving Differential Privacy with Shadow Execution
• CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
• Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms
• DPGen: Automated Program Synthesis for Differential Privacy
• Minimax Rates of Estimating Approximate Differential Privacy
• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
• Computationally Bounded Robust Compilation and Universally Composable Security
• Verifying Pufferfish Privacy in Hidden Markov Models
• Free Gap Information from the Differentially Private Sparse Vector and Noisy Max Mechanisms
• Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions
• Privacy accounting $\epsilon$conomics: Improving differential privacy composition via a posteriori bounds
• Asymmetric Differential Privacy
• Testing Differential Privacy with Dual Interpreters