Vérification formelle de la vie privée dans les systèmes concurrents

The verification of systems for protecting sensitive and confidential information is becoming an increasingly important issue in the modern world. Many protocols for protecting confidential information have used randomized mechanisms, to obfuscate the link between the secret and the public information. Typical examples are DCNets, Crowds, Onion Routing, Freenet and Tor. Another common denominator of them is that various entities involved in the system to verify occur as concurrent processes, and present typically nondeterministic behavior.This dissertation is devoted to the development of novel reasoning techniques for verifying differential privacy in concurrent systems. Differential privacy is a promising notion of privacy originated from the community of statistical databases, and now widely adopted in various models of computation. We use the principle of differential privacy as a criterion to measure the level of privacy that a concurrent system satisfies.The first part of the present thesis is focused on modular reasoning about differential privacy in a probabilistic variant of Robin Milner’s Calculus of Communicating Systems (CCS). We show that the calculus operators such as non-deterministic choice, probabilistic choice, restriction and a restricted form of parallel composition are safe, in the sense that combining components with these operators does not compromise the privacy of the entire system.The second part focuses on the applicability of bisimulation - a fundamental technique in Concurrency Theory - for characterizing differentially private behavior. We borrow the idea of amortisation, which was initially applied on some bisimulations with cost-based actions, and coin an amortised probabilistic bisimulation. We show that it allows us to verify differential privacy and it is a more liberal notion than the work of Tschantz et al.In the third part the focus is shifted to the development of proof systems - an axiomatic way for proving properties of concurrent systems. We provide sound and complete proof systems for our amortised bisimulation and its weak counterpart. The proof systems make it possible to reason about long-term (observable) differentially private behavior by syntactic manipulation.The last part presents an extension of the bisimulation metric based on the Kantorovich distance. This is a metric that has become very popular in Concurrency Theory, thanks to its principled and solid mathematical foundations. While the standard notion is additive in nature and therefore not suitable to prove the property of differential privacy (which is multiplicative), the extension developed in the thesis is parametric with respect to the underlying distance, and therefore suitable to capture a vast range of properties, including differential privacy.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