LightDP: towards automating differential privacy proofs

By Danfeng Zhang, Daniel Kifer. 2016

84 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Sociology and Political Science

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Sociology and Political Science

Citations in the corpus

EKTELO: A Framework for Defining Differentially-Private Computations (2018, background): “LightDP allows for verification of sophisticated differentially private algorithms with little manual effort.”
Synthesizing coupling proofs of differential privacy (2017, methodology): “This construction is inspired by ideas from Zhang and Kifer [45], who demonstrate how the pairing between samples (randomness alignment) can be selected depending on the result of the first sample.”
Proving differential privacy with shadow execution (2019, methodology): “LightDP [42] was the first system that could verify Sparse Vector with very few annotations, but it could not verify tight privacy bounds on Report Noisy Max [20].”