Distance makes the types grow stronger: a calculus for differential privacy
Distance makes the types grow stronger: a calculus for differential privacy
复制标题
DOI：
10.1145/1863543.1863568
复制
发表时间：
2010-09
期刊：
影响因子：
--
通讯作者：
J. Reed;B. Pierce
中科院分区：
文献类型：
--
作者：
J. Reed;B. Pierce
我们希望得到保证，在发布来自数据库的汇总数据时，不会泄露敏感信息。差分隐私提供了一个强有力的统计保证，即数据库中任何个人的存在的影响将是可以忽略不计的，即使对手有辅助知识。在这一领域的许多先前的工作包括证明算法是差分私有的一次，我们建议简化这个过程的函数式语言，其类型系统自动保证差分隐私，允许程序员编写复杂的隐私安全查询程序中的灵活和组合的方式。关键的新奇是我们的类型系统捕获函数敏感度的方式，这是一个函数可以放大相似输入之间距离的度量：类型良好的程序不仅不会出错，而且不会在附近的输入上走得太远。此外，通过引入一个单子的随机计算，我们可以表明，建立的定义差异隐私福尔斯下降自然作为一个特殊情况下，这一健全性原则。我们开发的例子，包括已知的差分隐私算法，隐私意识的标准函数式编程习惯的变种，和差分隐私的组合原则。
We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will be negligible, even when an adversary has auxiliary knowledge. Much of the prior work in this area consists of proving algorithms to be differentially private one at a time; we propose to streamline this process with a functional language whose type system automatically guarantees differential privacy, allowing the programmer to write complex privacy-safe query programs in a flexible and compositional way. The key novelty is the way our type system captures function sensitivity, a measure of how much a function can magnify the distance between similar inputs: well-typed programs not only can't go wrong, they can't go too far on nearby inputs. Moreover, by introducing a monad for random computations, we can show that the established definition of differential privacy falls out naturally as a special case of this soundness principle. We develop examples including known differentially private algorithms, privacy-aware variants of standard functional programming idioms, and compositionality principles for differential privacy.