LightDP: towards automating differential privacy proofs
- 1 January 2017
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 888-901
- https://doi.org/10.1145/3009837.3009884
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 when multiple proofs exist. We show that LightDP verifies sophisticated algorithms with little manual effort.Keywords
Other Versions
This publication has 29 references indexed in Scilit:
- νZ - An Optimizing SMT SolverLecture Notes in Computer Science, 2015
- PufferfishACM Transactions on Database Systems, 2014
- Metrics for Differential Privacy in Concurrent SystemsLecture Notes in Computer Science, 2014
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic ProgramsLecture Notes in Computer Science, 2013
- Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract)Electronic Notes in Theoretical Computer Science, 2011
- Dafny: An Automatic Program Verifier for Functional CorrectnessLecture Notes in Computer Science, 2010
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- Our Data, Ourselves: Privacy Via Distributed Noise GenerationLecture Notes in Computer Science, 2006
- Type error slicing in implicitly typed higher-order languagesScience of Computer Programming, 2004
- Semantics of probabilistic programsJournal of Computer and System Sciences, 1981