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

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.

References in corpus (8)

• RAPPOR: Randomized Aggregatable Privacy-Preserving Ordinal Response
• Prochlo: Strong Privacy for Analytics in the Crowd
• Detecting Violations of Differential Privacy
• Proving Differential Privacy via Probabilistic Couplings
• LightDP: Towards Automating Differential Privacy Proofs
• Proving differential privacy in Hoare logic
• Advanced Probabilistic Couplings for Differential Privacy
• Proving Differential Privacy with Shadow Execution

Cited by in corpus (5)

• DPGen: Automated Program Synthesis for Differential Privacy
• The Complexity of Verifying Boolean Programs as Differentially Private
• QueryCheetah: Fast Automated Discovery of Attribute Inference Attacks Against Query-Based Systems
• Curator Attack: When Blackbox Differential Privacy Auditing Loses Its Power
• Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions