Vérification automatique de la confidentialité différentielle

Ce rapport étudie la vérification quantitative de la confidentialité différentielle dans les systèmes distribués. Tout d'abord, nous examinons l'applicabilité de la vérification des modèles probabilistes pour fournir des garanties sur le comportement des système différentiellement confidentiels. Ensuite, nous concevons des méthodes qui extraient automatiquement les modèles des systèmes à partir d'une description de haut niveau, puis nous effectuons une vérification probabiliste de ces modèles. Nous développons à cette fin une nouvelle méthodologie de la vérification quantitative. Nous décrivons des méthodes formelles pour analyser un large éventail de propriétés de confidentialité, notamment la précision et la perte de la confidentialité. Nous avons également réexprimé la notion de confidentialité différentielle pour raisonner sur deux exécutions de programmes similaires. À notre connaissance, il s'agit des analyses de confidentialité les plus genérales pour les systèmes distribués. Deuxièmement, nous fournissons des preuves de couplage basées sur les relations de levage approximatives pour prouver la confidentialité différentielle dans les chaînes de Markov. Nous proposons également des algorithmes de vérification symbolique de la confidentialité. L'avantage de notre approche est que ces algorithmes peuvent être facilement implémentés dans n'importe quel outil de vérification de modèles probabilistes. Enfin, nous définissons une approche pour extraie des contre-exemples qui peuvent être utilisés pour fin de débogage similaires en fournissant une exécution qui viole la confidentialité.

Abstract

This report studies the quantitative verification of differential privacy in distributed systems. First, we examine the applicability of probabilistic model checking to provide guarantees on the behavior of differentially private systems. Next, we design methods that automatically extract the models of the systems from a high-level description, then we perform a probabilistic verification of these models. To this end, we are developing a new methodology for quantitative verification. We describe formal methods for analyzing a wide range of privacy properties, including accuracy and privacy loss. We have also re-expressed the notion of differential privacy to reason about two executions of similar programs. To our knowledge, this is the most general privacy analysis for distributed systems. Second, we provide evidence of coupling based on approximate lifting relationships to prove differential privacy in Markov chains. We also offer symbolic algorithm for verification of confidentiality. The advantage of our approach is that these algorithms can be easily implemented in any probabilistic model checker tool. Finally, we define an approach for extracting counterexamples that can be used for similar debugging purposes by providing an execution that violates confidentiality.