Fuzzi: a three-level logic for differential privacy
Fuzzi: a three-level logic for differential privacy
复制标题
Fuzzi：差分隐私的三级逻辑
DOI：
10.1145/3341697
复制
发表时间：
2019
影响因子：
--
通讯作者：
Aaron Roth
中科院分区：
文献类型：
--
作者：
Hengchu Zhang;Edo Roth;Andreas Haeberlen;B. Pierce;Aaron Roth
敏感数据集的管理员有时需要知道对数据的查询是否具有不同的隐私性。已经提出了两种类型的逻辑来检查这个属性：(1)类型系统和其他静态分析，它们完全自动化了与“程序敏感性”和“隐私损失”等概念的直接推理；(2)成熟的程序逻辑，如apRHL（一种近似的、概率的、关系的Hoare逻辑），它支持对微妙的隐私保护算法技术进行更灵活的推理，但只提供最小的自动化。我们提出了一种命令式环境下差分隐私的三层逻辑，并提出了一个名为Fuzzi的原型实现。Fuzzi的最低层次是通用逻辑；中层为apRHL；它的顶层是一种新的敏感逻辑，它改编自一种差分私有函数语言Fuzz的线性逻辑启发型系统。关键的新颖之处在于敏感逻辑与两个低级逻辑之间的高度集成：敏感逻辑的判断和证明可以很容易地转化为apRHL；相反，关键算法构建块的隐私属性可以在apRHL和基本逻辑中手工证明，然后打包成类型规则，敏感逻辑的检查器可以应用这些规则自动构建任意大小的组合程序的隐私证明。我们通过实现四种不同的私有机器学习算法来展示Fuzzi的效用，并展示Fuzzi的检查器能够推导出严格的灵敏度界限。
Curators of sensitive datasets sometimes need to know whether queries against the data are differentially private. Two sorts of logics have been proposed for checking this property: (1) type systems and other static analyses, which fully automate straightforward reasoning with concepts like “program sensitivity” and “privacy loss,” and (2) full-blown program logics such as apRHL (an approximate, probabilistic, relational Hoare logic), which support more flexible reasoning about subtle privacy-preserving algorithmic techniques but offer only minimal automation. We propose a three-level logic for differential privacy in an imperative setting and present a prototype implementation called Fuzzi. Fuzzi’s lowest level is a general-purpose logic; its middle level is apRHL; and its top level is a novel sensitivity logic adapted from the linear-logic-inspired type system of Fuzz, a differentially private functional language. The key novelty is a high degree of integration between the sensitivity logic and the two lower-level logics: the judgments and proofs of the sensitivity logic can be easily translated into apRHL; conversely, privacy properties of key algorithmic building blocks can be proved manually in apRHL and the base logic, then packaged up as typing rules that can be applied by a checker for the sensitivity logic to automatically construct privacy proofs for composite programs of arbitrary size. We demonstrate Fuzzi’s utility by implementing four different private machine-learning algorithms and showing that Fuzzi’s checker is able to derive tight sensitivity bounds.
影响因子：
1.8
作者：
Albarghouthi, Aws;Hsu, Justin
通讯作者：
Hsu, Justin