Skip to main content

LightDP: Towards automating differential privacy proofs

Publication ,  Conference
Zhang, D; Kifer, D
Published in: Conference Record of the Annual ACM Symposium on Principles of Programming Languages
January 1, 2017

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.

Duke Scholars

Altmetric Attention Stats
Dimensions Citation Stats

Published In

Conference Record of the Annual ACM Symposium on Principles of Programming Languages

DOI

ISSN

0730-8566

Publication Date

January 1, 2017

Start / End Page

888 / 901
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Zhang, D., & Kifer, D. (2017). LightDP: Towards automating differential privacy proofs. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 888–901). https://doi.org/10.1145/3009837.3009884
Zhang, D., and D. Kifer. “LightDP: Towards automating differential privacy proofs.” In Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 888–901, 2017. https://doi.org/10.1145/3009837.3009884.
Zhang D, Kifer D. LightDP: Towards automating differential privacy proofs. In: Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 2017. p. 888–901.
Zhang, D., and D. Kifer. “LightDP: Towards automating differential privacy proofs.” Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017, pp. 888–901. Scopus, doi:10.1145/3009837.3009884.
Zhang D, Kifer D. LightDP: Towards automating differential privacy proofs. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 2017. p. 888–901.

Published In

Conference Record of the Annual ACM Symposium on Principles of Programming Languages

DOI

ISSN

0730-8566

Publication Date

January 1, 2017

Start / End Page

888 / 901