CheckDP：一种证明差分隐私或寻找精确反例的自动集成方法
CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
摘要：
我们提出了CheckDP，第一个自动化和集成的方法来证明或反驳索赔，一个机制是差分私有的。CheckDP可以找到具有微妙错误的机制的反例，而先前的反例生成器已经失败了。此外，\emph{automatically}能够为之前未报告的形式化验证的正确机制生成证据。CheckDP是建立在静态程序分析的基础上的，与现有的反例生成器（运行机制数十万次以估计其输出分布）相比，它在捕获不频繁事件方面更有效、更精确。此外，其合理的方法还允许自动验证正确的机制。当在标准基准和更新的隐私机制上进行评估时，CheckDP在70秒内生成证明（对于正确的机制）和反例（对于不正确的机制），没有任何误报或漏报。
英文摘要：
We propose CheckDP, the first automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to \emph{automatically} generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and more precise in catching infrequent events than existing counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
