Skip to Main content Skip to Navigation
Conference papers

Linear Dependent Types for Differential Privacy

Marco Gaboardi 1, 2, 3 Andreas Haeberlen 3 Justin Hsu 3 Arjun Narayan 3 Benjamin Pierce 3
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : 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 differentially private. In one approach, Reed and Pierce 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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 10:55:51 AM
Last modification on : Saturday, January 27, 2018 - 1:30:45 AM

Links full text




Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, Benjamin Pierce. Linear Dependent Types for Differential Privacy. 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013, Rome, Italy, Italy. pp.357--370, ⟨10.1145/2429069.2429113⟩. ⟨hal-00909340⟩



Record views