Testing Differential Privacy with Dual Interpreters

TL;DR

DPCheck is an automated framework that tests differential privacy implementations without annotations, effectively distinguishing correct from buggy algorithms, and has been successfully applied to real-world privacy systems like the US Census DAS.

Contribution

It introduces the first fully automated testing framework for differential privacy that handles all verified algorithms and distinguishes correct from incorrect implementations.

Findings

DPCheck accepts correct privacy algorithms and rejects incorrect variants.

The probability of false acceptance can be exponentially reduced with larger test sizes.

DPCheck successfully tested real-world privacy systems like the US Census DAS.

Abstract

Applying differential privacy at scale requires convenient ways to check that programs computing with sensitive data appropriately preserve privacy. We propose here a fully automated framework for {\em testing} differential privacy, adapting a well-known "pointwise" technique from informal proofs of differential privacy. Our framework, called DPCheck, requires no programmer annotations, handles all previously verified or tested algorithms, and is the first fully automated framework to distinguish correct and buggy implementations of PrivTree, a probabilistically terminating algorithm that has not previously been mechanically checked. We analyze the probability of DPCheck mistakenly accepting a non-private program and prove that, theoretically, the probability of false acceptance can be made exponentially small by suitable choice of test size. We demonstrate DPCheck's utility empirically by implementing all benchmark algorithms from prior work on mechanical verification of differential privacy, plus several others and their incorrect variants, and show DPCheck accepts the correct implementations and rejects the incorrect variants. We also demonstrate how DPCheck can be deployed in a practical workflow to test differentially privacy for the 2020 US Census Disclosure Avoidance System (DAS).