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

TL;DR

CheckDP is an automated tool that efficiently proves or disproves differential privacy of mechanisms, finding subtle bugs or generating proofs without false positives or negatives.

Contribution

It introduces the first integrated, automated approach combining static analysis for verifying differential privacy and finding counterexamples, outperforming prior methods.

Findings

Successfully verified several mechanisms within 70 seconds

Detected subtle bugs in mechanisms where previous tools failed

Generated formal proofs for correct mechanisms without errors

Abstract

We propose CheckDP, the first 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 \emph{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 more precise in catching infrequent events than existing 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.