SuperDP: Differential Privacy Refutation via Supermartingales
This work addresses the need for reliable verification tools in privacy-preserving data analysis, offering an automated solution for researchers and practitioners to detect DP violations, though it is incremental as it builds on existing probabilistic program analysis techniques.
The paper tackles the problem of automated formal refutation of differential privacy (DP) properties, which is challenging and error-prone, by presenting a novel method that uses supermartingales and submartingales to search for input pairs and functions that violate DP, resulting in a prototype tool, SuperDP, that achieves superior performance and refutes DP for challenging examples beyond prior methods.
Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of $ε$-DP. Our method refutes $ε$-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for $ε$-DP refutation. To the best of our knowledge, our method is the first method for $ε$-DP refutation to offer the following four desirable features: (1)~it is fully automated, (2)~it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3)~it provides soundness guarantees, and (4)~it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute $ε$-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.