Linear Dependent Types for Differential Privacy
Linear Dependent Types for Differential Privacy
复制标题
DOI：
10.1145/2480359.2429113
复制
发表时间：
2013-01-01
影响因子：
--
通讯作者：
Pierce, Benjamin C.
中科院分区：
文献类型：
--
作者：
Gaboardi, Marco;Haeberlen, Andreas;Pierce, Benjamin C.
差异隐私提供了一种方法来回答关于敏感信息的查询，同时提供强大的、可证明的隐私保证，确保数据库中单个个体的存在或不存在对查询结果的统计影响可以忽略不计。要证明给定查询具有此属性，需要建立查询敏感性的界限，即在添加或删除单个记录时其结果可以改变多少。已经开发了各种工具来证明给定的查询是差异私有的。在一种方法中，Reed和Pierce提出了一种函数式编程语言Fuzz，用于编写差分私有查询。Fuzz用线性类型跟踪灵敏度，用概率单子表示随机计算；它保证任何具有特定类型的程序都是差分私有的。Fuzz可以成功验证许多有用的查询。然而，当灵敏度分析依赖于非静态已知值时，它就失败了。我们提出了DFuzz，它是Fuzz的扩展，结合了线性索引类型和轻量级依赖类型。这种组合允许进行更丰富的灵敏度分析，从而能够将更大的查询类认证为差异私有，包括那些灵敏度依赖于运行时信息的查询类。与Fuzz一样，微分隐私保证直接遵循类型系统的稳健性定理。我们通过证明一大类迭代算法的差分隐私性来证明DFuzz的增强表达性，这些算法以前无法类型化。
Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity-how much its result can change when a single record is added or removed.A variety of tools have been developed for certifying that a given query is differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation; it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically.We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.