论文分享_08_05

CheckDP: 一个验证差分隐私或寻找精确反例的集成自动化方法

          今天分享的文章是来自CCS ’20的CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples,作者是The Pennsylvania State University的Yuxin Wang, Zeyu Ding, Daniel Kifer, Danfeng Zhang.

摘     要

        差分隐私目前已在学术、工业界得到广泛运用,允许数据使用者收集一定量统计信息的同时,保护数据库里个体的隐私。然而,隐私机制涉及添加随机噪声,其正确性往往要求数学家复杂严格的手写证明,极易出错,所以需要形式化验证、测试等自动化方法去验证差分隐私机制的正确性。本文主要贡献:

  1. 开发了工具CheckDP,既能为正确的差分隐私机制生成证明,又能为不正确的机制找出反例,是当今相关工作中最早产生的自动化工具之一;
  2. 基于randomness alignment方法将概率程序语义转化为非概率目标程序,并带有明确的证明目标;
  3. 通过交替寻找证明/反例的迭代方法不断细化证明和反例;
  4. 实验表明,对于经典的差分隐私机制,其工具能在数分钟内找出证明或寻找到反例。代码发布在:https://github.com/cmla-psu/checkdp。

一、差分隐私图片

图片

        验证差分隐私是否成立,即验证上式是否对于任意的相邻数据库和输出都满足,若不满足即存在反例。

二、Randomness Alignment

       相比于手写证明,randomness alignment是一个更适合于程序验证的方法,其将寻找证明的过程转化为寻找一个合适的alignment。简单来说,randomness alignment可被看作为随机变量之间的距离,其反应了两个分布之间的单射关系。
 

三、运行示例

四、证明与反例

接下来分开介绍寻找证明和反例的过程,在实际运行中这俩过程是交替进行的,即寻找证明过程无法进行时,会进入寻找反例过程,反之亦然,整个流程如下图所示。

五、程序转化

六、实验结果

        文章验证了经典差分隐私机制及其对应的变体,包括改变加入的噪声值大小,改变输出为噪声值、下标值等等。其中对于正确的差分隐私机制,与以往工作如基于coupling的证明工作,同样基于Shadow Execution和randomness alignment的工具ShadowDP,基于有限输入输出遍历的验证工具DiPC相比,其寻找正确的证明所需时间要快,且自动化程度高,如下图所示:
    对于几个不正确的差分隐私机制,文章也与基于测试的工具StatDP和DP-Finder作了比较,结果表明反例生成速度都要快于这些工具:
    更多关于生成反例,Alignment模板等参数寻找的相关实验数据如下图表所示: