差分隐私耦合证明的自动综合

差分隐私已成为一种有前景的概率隐私形式，在学术界和工业界引起了广泛关注。我们提出了一种一键式自动化技术，用于验证复杂随机算法的 $\varepsilon$-差分隐私。我们做出了几项概念、算法和实际方面的贡献：(i) 受近似耦合和随机性对齐最新进展的启发，我们提出了一种名为耦合策略的新证明技术，将差分隐私证明转化为一种博弈中的获胜策略，在该博弈中我们拥有有限的隐私资源可供消耗。(ii) 为了发现获胜策略，我们将问题表述为基于耦合的 Horn 模 (Horn modulo couplings, HMC) 约束集，这是一阶 Horn 子句与概率约束的新颖结合。(iii) 我们提出了一种通过将概率约束转化为带未解释函数的逻辑约束来求解 HMC 约束的技术。(iv) 最后，我们在 FairSquare 验证器中实现了该技术，并为差分隐私文献中的许多具有挑战性的算法提供了首个自动化隐私证明，包括 Report Noisy Max、指数机制和稀疏向量机制。