CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples

Yuxin Wang, Zeyu Ding, Daniel Kifer, Danfeng Zhang

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

Abstract

We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to automatically generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and precise in catching infrequent events than sampling based counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.

Original languageEnglish (US)
Title of host publicationCCS 2020 - Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security
PublisherAssociation for Computing Machinery
Pages919-938
Number of pages20
ISBN (Electronic)9781450370899
DOIs
StatePublished - Oct 30 2020
Event27th ACM SIGSAC Conference on Computer and Communications Security, CCS 2020 - Virtual, Online, United States
Duration: Nov 9 2020Nov 13 2020

Publication series

NameProceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)1543-7221

Conference

Conference27th ACM SIGSAC Conference on Computer and Communications Security, CCS 2020
CountryUnited States
CityVirtual, Online
Period11/9/2011/13/20

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples'. Together they form a unique fingerprint.

Cite this