Proving Differential Privacy via Probabilistic Couplings

Abstract : Over the last decade, differential privacy has achieved widespread adoption within the privacy community. Moreover, it has attracted significant attention from the verification community, resulting in several successful tools for formally proving differential privacy. Although their technical approaches vary greatly, all existing tools rely on reasoning principles derived from the composition theorem of differential privacy. While this suffices to verify most common private algorithms, there are several important algorithms whose privacy analysis does not rely solely on the composition theorem. Their proofs are significantly more complex, and are currently beyond the reach of verification tools. In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on deep connections between differential privacy and probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by a coupling argument. We demonstrate our methods on two algorithms: the Exponential mechanism and the Above Threshold algorithm, the critical component of the famous Sparse Vector algorithm. We verify these examples in a relational program logic apRHL + , which can construct approximate couplings. This logic extends the existing apRHL logic with more general rules for the Laplace mechanism and the one-sided Laplace mechanism, and new structural rules enabling pointwise reasoning about privacy; all the rules are inspired by the connection with coupling. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community.
Type de document :
Communication dans un congrès
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2016, New York, United States. pp.749 - 758, 2016, 〈10.1145/2933575.2934554〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger
Contributeur : Benjamin Gregoire <>
Soumis le : mercredi 7 décembre 2016 - 08:47:25
Dernière modification le : jeudi 11 janvier 2018 - 16:48:46
Document(s) archivé(s) le : lundi 20 mars 2017 - 18:07:47


Fichiers produits par l'(les) auteur(s)




Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Proving Differential Privacy via Probabilistic Couplings. Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2016, New York, United States. pp.749 - 758, 2016, 〈10.1145/2933575.2934554〉. 〈hal-01411097〉



Consultations de la notice


Téléchargements de fichiers