{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/104913"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/104913","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Automated methods for checking differential privacy","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Ravi, Vishal Jagannath"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Viswanathan, Mahesh"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-08-23T20:01:16Z","date_published":"2019-08-23T20:01:16Z","updated_at":"2026-07-22T22:24:42Z","subjects":["differential privacy","sparse vector"],"languages":["en"],"rights":["Copyright 2019 Vishal Jagannath Ravi"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/104913","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Viswanathan, Mahesh"]},{"key":"dc:creator","label":"Author","values":["Ravi, Vishal Jagannath"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-08-23T20:01:16Z","2019-04-24","2019-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["differential privacy","sparse vector"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Vishal Jagannath Ravi"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/104913"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Vishal Jagannath Ravi, accepted the attached license on 2019-04-23 at 20:11.","The student, Vishal Jagannath Ravi, submitted this Thesis for approval on 2019-04-23 at 20:17.","This Thesis was approved for publication on 2019-04-24 at 13:31.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13853 on 2019-08-22 at 14:46:19","Made available in DSpace on 2019-08-23T20:01:16Z (GMT). No. of bitstreams: 2 RAVI-THESIS-2019.pdf: 453531 bytes, checksum: 72b8e0d97ab2daed016520cf05bbf106 (MD5) LICENSE.txt: 4218 bytes, checksum: f1800d46e9985d8021b212d9d7a7b71d (MD5) Previous issue date: 2019-04-24"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Automated methods for checking differential privacy"]}]}],"canonical_facts":{"dc:contributor":["Viswanathan, Mahesh"],"dc:creator":["Ravi, Vishal Jagannath"],"dc:date":["2019-08-23T20:01:16Z","2019-04-24","2019-05"],"dc:description":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Vishal Jagannath Ravi, accepted the attached license on 2019-04-23 at 20:11.","The student, Vishal Jagannath Ravi, submitted this Thesis for approval on 2019-04-23 at 20:17.","This Thesis was approved for publication on 2019-04-24 at 13:31.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13853 on 2019-08-22 at 14:46:19","Made available in DSpace on 2019-08-23T20:01:16Z (GMT). No. of bitstreams: 2 RAVI-THESIS-2019.pdf: 453531 bytes, checksum: 72b8e0d97ab2daed016520cf05bbf106 (MD5) LICENSE.txt: 4218 bytes, checksum: f1800d46e9985d8021b212d9d7a7b71d (MD5) Previous issue date: 2019-04-24"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/104913"],"dc:language":["en"],"dc:rights":["Copyright 2019 Vishal Jagannath Ravi"],"dc:subject":["differential privacy","sparse vector"],"dc:title":["Automated methods for checking differential privacy"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:42Z"}