Formal Verification of Differential Privacy in Concurrent Systems

Lili Xu 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Résumé : La vérification des systèmes de protection des données sensibles et confidentielles est un défi important que le monde moderne doive relever à l’ère du tout numérique. De nombreux protocoles pour la protection de ces données sensibles utilisent des mécanismes aléatoires pour masquer le lien entre une donnée secrète ou sensible et l’information publique qui lui est associée. Les systèmes de protection tels que DCNets, Crowds protocol, Onion Routing, Freenet et Tor sont des exemples typiques. L’autre dénominateur commun de ces systèmes est le fait que différentes entités impliquées dans le système se produisent simultanément, et présentent généralement un comportement non-déterministe. Cette thèse est consacrée au développement des nouvelles techniques de raisonnement pour vérifier le concept de la “differential privacy” dans les systèmes concurrents. Differential privacy est une notion prometteuse provenant de la communauté des bases statistiques. Elle est maintenant largement adoptée dans différents modèles de calcul. Nous l’utilisons dans cette thèse comme un critère pour mesurer le niveau de confidentialité qu’un système probabiliste et non-déterministe satisfait. Dans la première partie de cette thèse, nous considérons le raisonnement modulaire sur la differential privacy dans une variante probabiliste de “Calcul des Systèmes Communicants” (CCS) de Robin Milner. Nous montrons que les opérateurs du modèle de calcul tels que le choix non-déterministe, le choix probabiliste, la restriction ainsi qu’une forme restreinte de la composition parallèle préservent tous la differential privacy, dans le sens que combiner des composantes (ayant un certain niveau de protection au sens de la differential privacy) avec ces opérateurs ne compromet pas la differential privacy du système entier ainsi obtenu. La deuxième partie porte sur l’applicabilité de bisimulation - une technique fondamentale dans le domaine de la concurrence - pour caractériser le comportement du système au sens de la differential privacy. Nous adoptons l’idée de l’amortissement, qui a d’abord été appliquée sur certaines bisimulations avec des actions en fonction des coˆuts, et construisons une bisimulation probabiliste amortie. Cette bisimulation nous a permis de vérifier la differential privacy. Nous avons également montré que notre notion est plus flexible que celle dans le travail de Tschantz et al. Dans la troisième partie l’attention porte sur le développement des systèmes de preuve : une manière axiomatique pour prouver les propriétés de systèmes concurrents. Nous fournissons deux systèmes de preuve cohérents et complets pour notre bisimulation amortie et son homologue (c’est-à-dire la bisimulation) faible. Les systèmes de preuve permettent de raisonner sur le comportement (observable) sur le long terme d’un système grˆace à la manipulation syntaxique de son modèle. La dernière partie présente une extension de la métrique de bisimulation basée sur la distance de Kantorovich. C’est une mesure qui est devenue très populaire dans le domaine de la concurrence, grˆace à ses fondements mathématiques solides. Mais la notion standard est de nature additive et donc pas appropriée à prouver la propriété de la differential privacy (qui est de nature multiplicative), l’extension développée dans la thèse est paramétrique par rapport à la distance sous-ajacente, et donc appropriée pour capturer une vaste gamme de propriétés, y compris la differential privacy.
Type de document :
Thèse
Cryptography and Security [cs.CR]. Ecole Polytechnique (Palaiseau, France), 2015. English
Liste complète des métadonnées

Littérature citée [91 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01384363
Contributeur : Konstantinos Chatzikokolakis <>
Soumis le : mardi 25 octobre 2016 - 10:18:54
Dernière modification le : jeudi 10 mai 2018 - 02:06:27

Identifiants

  • HAL Id : tel-01384363, version 1

Citation

Lili Xu. Formal Verification of Differential Privacy in Concurrent Systems. Cryptography and Security [cs.CR]. Ecole Polytechnique (Palaiseau, France), 2015. English. 〈tel-01384363〉

Partager

Métriques

Consultations de la notice

294

Téléchargements de fichiers

174