University of Illinois Urbana-Champaign

Automated methods for checking differential privacy

Ravi, Vishal Jagannath

Content Files
RAVI-THESIS-2019.pdf

Permalink

https://hdl.handle.net/2142/104913

Description

Title
Automated methods for checking differential privacy
Author(s)
Ravi, Vishal Jagannath
Issue Date
2019-04-24
Director of Research (if dissertation) or Advisor (if thesis)
Viswanathan, Mahesh
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Date of Ingest
2019-08-23T20:01:16Z
Keyword(s)
  • differential privacy
  • sparse vector
Abstract
Differential privacy is a de facto standard for statistical computations over databases that contain private data. The strength of differential privacy lies in a rigorous mathematical definition which guarantees individual privacy and yet allows for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work uses logical methods for proving privacy. However, these methods are not complete, and only partially automated. A recent and complementary line of work uses statistical methods for finding privacy violations. However, the methods only provide statistical guarantees (but no proofs). We propose the first decision procedure for checking differential privacy of a non-trivial class of probabilistic computations. Our procedure takes as input a program P parametrized by a privacy budget epsilon and either proves differential privacy for all possible values of epsilon, or generates a counterexample. In addition, our procedure applies both to epsilon-differential privacy and (epsilon, δ)-differential privacy. Technically, the decision procedure is based on a novel and judicious encoding of the semantics class 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.
Graduation Semester
2019-05
Type of Resource
text
Permalink
http://hdl.handle.net/2142/104913
Copyright and License Information
Copyright 2019 Vishal Jagannath Ravi

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science