Deciding Differential Privacy for Programs with Finite Inputs and Outputs

Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan

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

Abstract

Differential privacy is a de facto standard for statistical computations over databases that contain private data. Its main and rather surprising strength is to guarantee individual privacy and yet allow for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work develops and uses logical methods for proving privacy. A more recent and complementary line of work uses statistical methods for finding privacy violations. Although both lines of work are practically successful, they elide the fundamental question of decidability. This paper studies the decidability of differential privacy. We first establish that checking differential privacy is undecidable even if one restricts to programs having a single Boolean input and a single Boolean output. Then, we define a non-trivial class of programs and provide a decision procedure for checking the differential privacy of a program in this class. Our procedure takes as input a program P parametrized by a privacy budget and either establishes the differential privacy for all possible values of or generates a counter-example. In addition, our procedure works for both to -differential privacy and (, δ)-differential privacy. Technically, the decision procedure is based on a novel and judicious encoding of the semantics of programs in our class into a decidable fragment of the first-order theory of the reals with exponentiation. We implement our procedure and use it for (dis)proving privacy bounds for many well-known examples, including randomized response, histogram, report noisy max and sparse vector.

Original languageEnglish (US)
Title of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
PublisherAssociation for Computing Machinery
Pages141-154
Number of pages14
ISBN (Electronic)9781450371049
DOIs
StatePublished - Jul 8 2020
Event35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany
Duration: Jul 8 2020Jul 11 2020

Publication series

NameACM International Conference Proceeding Series

Conference

Conference35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
CountryGermany
CitySaarbrucken
Period7/8/207/11/20

Keywords

  • decision procedure
  • differential privacy
  • sparse vector

ASJC Scopus subject areas

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Deciding Differential Privacy for Programs with Finite Inputs and Outputs'. Together they form a unique fingerprint.

Cite this