LightDP: Towards Automating Differential Privacy Proofs

Abstract

The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is the natural rise in the development and publication of incorrect algorithms, thus demonstrating the necessity of formal verification tools. However, existing formal methods for differential privacy face a dilemma: methods based on customized logics can verify sophisticated algorithms but come with a steep learning curve and significant annotation burden on the programmers, while existing programming platforms lack expressive power for some sophisticated algorithms. In this paper, we present LightDP, a simple imperative language that strikes a better balance between expressive power and usability. The core of LightDP is a novel relational type system that separates relational reasoning from privacy budget calculations. With dependent types, the type system is powerful enough to verify sophisticated algorithms where the composition theorem falls short. In addition, the inference engine of LightDP infers most of the proof details, and even searches for the proof with minimal privacy cost bound when multiple proofs exist. We show that LightDP verifies sophisticated algorithms with little manual effort.

References in corpus (6)

• RAPPOR: Randomized Aggregatable Privacy-Preserving Ordinal Response
• LightDP: Towards Automating Differential Privacy Proofs
• Proving differential privacy in Hoare logic
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• On the Privacy Properties of Variants on the Sparse Vector Technique
• Understanding the Sparse Vector Technique for Differential Privacy

Cited by in corpus (21)

• Detecting Violations of Differential Privacy
• LightDP: Towards Automating Differential Privacy Proofs
• Proving Differential Privacy with Shadow Execution
• Ektelo: A Framework for Defining Differentially-Private Computations
• CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
• Chorus: a Programming Framework for Building Scalable Differential Privacy Mechanisms
• Approximate Span Liftings
• Guidelines for Implementing and Auditing Differentially Private Systems
• A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
• A Language for Probabilistically Oblivious Computation
• DPGen: Automated Program Synthesis for Differential Privacy
• Deciding Accuracy of Differential Privacy Schemes
• The Complexity of Verifying Boolean Programs as Differentially Private
• Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing 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
• Asymmetric Differential Privacy
• Privacy accounting $\epsilon$conomics: Improving differential privacy composition via a posteriori bounds
• Testing Differential Privacy with Dual Interpreters