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.

翻译：差分隐私(DP)已成为保障个体数据隐私的核心标准之一。然而，对DP性质进行推理是一项具有挑战性且易出错的任务，因此近年来对DP属性形式化验证与反证方法的研究备受关注。本文提出了一种新颖的$ε$-DP自动化形式化反证方法。该方法通过搜索一对输入以及定义在输出上的非负函数——该函数在这两个输入上的期望值存在显著差异——来实现$ε$-DP的反证。这两个输入与输出上的非负函数通过同时计算获得，我们利用随机程序分析中的上期望鞅和下期望亚鞅理论，引入了一套完备且可靠的$ε$-DP反证证明规则。据我们所知，这是首个同时具备以下四个理想特性的$ε$-DP反证方法：(1)完全自动化，(2)支持包含离散与连续分布采样指令的随机机制，(3)提供可靠性保证，以及(4)提供半完备性保证。实验表明，我们的原型工具SuperDP在性能上显著优于现有技术，成功反证了文献中多个具有挑战性的示例的$ε$-DP性质，其中包括先前方法无法处理的案例。