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 性质。