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.
Type de document :
Communication dans un congrès
40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013, Rome, Italy, Italy. ACM, pp.357--370, 2013, POPL '13. 〈10.1145/2429069.2429113〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909340
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:55:51
Dernière modification le : samedi 27 janvier 2018 - 01:30:45

Lien texte intégral

Identifiants

Collections

Citation

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. ACM, pp.357--370, 2013, POPL '13. 〈10.1145/2429069.2429113〉. 〈hal-00909340〉

Partager

Métriques

Consultations de la notice

191