Probabilistic relational reasoning for differential privacy
Probabilistic relational reasoning for differential privacy
复制标题
DOI：
10.1145/2103621.2103670
复制
发表时间：
2012-01-01
影响因子：
--
通讯作者：
Zanella Beguelin, Santiago
中科院分区：
文献类型：
--
作者：
Barthe, Gilles;Koepf, Boris;Zanella Beguelin, Santiago
差分隐私是一种保密性概念，它保护个人隐私，同时允许对他们的私人数据进行有用的计算。为真实的程序推导差分隐私保证是一项困难且容易出错的任务，需要有原则的方法和工具支持。最近出现了基于线性类型和静态分析的方法;然而，越来越多的程序使用这些方法无法分析的技术来实现隐私。例子包括以较弱的近似差分隐私保证为目标的程序，使用指数机制的程序，以及在不使用任何标准机制的情况下实现差分隐私的随机程序。提供支持推理的隐私，这样的程序一直是一个悬而未决的问题。我们报告CertiPriv，一个机器检查的框架，用于推理的差异隐私建立在Coq证明助理。CertiPriv的核心组件是概率关系Hoare逻辑的定量扩展，它使人们能够从第一原则中推导出程序的差分隐私保证。我们证明了CertiPriv的表现力，使用一些例子，其形式分析是以前的技术所无法达到的。特别是，我们提供了第一个机器检查证明的拉普拉斯和指数机制的正确性和隐私的随机和流算法从最近的文献。
Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential privacy guarantees for real programs is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that cannot be analyzed by these approaches. Examples include programs that aim for weaker, approximate differential privacy guarantees, programs that use the Exponential mechanism, and randomized programs that achieve differential privacy without using any standard mechanism. Providing support for reasoning about the privacy of such programs has been an open problem.We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of a probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the expressiveness of CertiPriv using a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian and Exponential mechanisms and of the privacy of randomized and streaming algorithms from the recent literature.