LightDP: towards automating differential privacy proofs
From MaRDI portal
Publication:5370924
DOI10.1145/3009837.3009884zbMATH Open1380.68136arXiv1607.08228OpenAlexW2565203757MaRDI QIDQ5370924FDOQ5370924
Authors: Danfeng Zhang, Daniel Kifer 
Publication date: 20 October 2017
Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1607.08228
Recommendations
- Probabilistic relational reasoning for differential privacy
- Formal verification of differential privacy for interactive systems (extended abstract)
- Proving differential privacy via probabilistic couplings
- Linear dependent types for differential privacy
- Distance makes the types grow stronger: a calculus for differential privacy
Cited In (11)
- Proving differential privacy via probabilistic couplings
- Formal verification of differential privacy for interactive systems (extended abstract)
- Higher-order approximate relational refinement types for mechanism design and differential privacy
- Linear dependent types for differential privacy
- Probabilistic relational reasoning for differential privacy
- Verifying Pufferfish privacy in hidden Markov models
- Coupled relational symbolic execution for differential privacy
- LightDP
- Model checking differentially private properties
- Certifying private probabilistic mechanisms
- Proving that programs are differentially private
Uses Software
This page was built for publication: LightDP: towards automating differential privacy proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370924)
