论文标题
CheckDP：一种自动化和集成的方法，用于证明差异隐私或找到精确的反例
CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
论文作者
论文摘要
我们提出了CheckDP，这是第一种自动化和集成的方法，用于证明或证明一种机制是私人的说法。 CheckDP可以找到具有先前反例发生器失败的微妙错误的机制的反例。此外，它能够\ emph {自动}生成证据，以提供正确的机制，以前没有进行过正式验证。 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.
