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é.