LightDP: Towards automating differential privacy proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationPOPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
EditorsAndrew D. Gordon, Giuseppe Castagna
PublisherAssociation for Computing Machinery
Pages888-901
Number of pages14
ISBN (Electronic)9781450346603
DOIs
StatePublished - Jan 1 2017
Event44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 - Paris, France
Duration: Jan 15 2017Jan 21 2017

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
CountryFrance
CityParis
Period1/15/171/21/17

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Zhang, D., & Kifer, D. (2017). LightDP: Towards automating differential privacy proofs. In A. D. Gordon, & G. Castagna (Eds.), POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (pp. 888-901). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009884