Testing Differential Privacy with Dual Interpreters
This provides a practical tool for developers and organizations to ensure privacy compliance in sensitive data applications, though it is incremental as it builds on existing pointwise techniques.
The paper tackles the problem of verifying differential privacy in programs by introducing DPCheck, a fully automated testing framework that requires no annotations and handles complex algorithms like PrivTree, demonstrating its utility by correctly accepting verified implementations and rejecting incorrect variants, including deployment in the 2020 US Census Disclosure Avoidance System.
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).