Vérification et Synthèse de Contrôleur pour des Propriétés de Confidentialité

In this thesis, we investigate the problems of verifying and enforcing confidentiality on critical systems. As a confidentiality property, we consider the notion of opacity which is a very general notion modeling the absence of information flow towards inquisitive attackers. Then, we study the application to opacity properties of formal methods developed in the context of discrete event systems. In the first part, we present how some classical abstract interpretation techniques can be applied to the computation of monitors to detect confidentiality vulnerabilities. We also present how the diagnosis theory can be adapted to detect opacity violations at runtime. In the second part, we develop some new techniques to enforce the opacity properties on a critical system. We study the supervisory control theory to restrict the behavior of a system in order to avoid information leakage. We show that this problem is in general out of the scope of the classical Ramadge & Wonham synthesis techniques. Therefore, we develop new algorithms to compute a most permissive controller enforcing the opacity property on a given system. Such techniques can be applied to the design of secure systems on a component based architecture. Finally, we consider an other approach to enforce opacity which is based on modifying at runtime the observability of the events. We show that this problem can be reduced to the computation of the set of winning strategies on a safety 2-player game. A possible application of such techniques is to generate dynamic firewalls to preserve confidential information.Les systèmes fonctionnant sur un réseau ouvert tels que les bases de données médicales ou les systèmes bancaires peuvent manipuler des informations dont la confidentialité doit être impérativement préservée. Dans ce contexte, la notion d'opacité formalise la capacité d'un système à garder secrètes certaines informations critiques. Dans cette thèse, nous nous intéressons à la fois à vérifier que la propriété d'opacité est satisfaite et à la synthèse de systèmes opaques. Vérifier l'opacité est un problème décidable pour des systèmes de transition finis. Pour les systèmes infinis, nous étudions l'application de techniques d'interprétation abstraite à la détection de vulnérabilité. Nous présentons aussi une méthode alternative qui s'appuie sur des abstractions régulières et sur des techniques de diagnostique pour détecter de telles vulnérabilité à l'exécution du système. Pour la synthèse de système opaque, nous appliquons dans un premier temps la théorie du contrôle à la Ramadge et Wonham pour calculer un contrôleur assurant l'opacité. Nous montrons que les techniques habituelles de synthèse de contrôleur ne peuvent être appliqué pour ce problème d'opacité et nous développons alors de nouveaux algorithmes pour calculer l'unique système opaque qui soit maximal au sens de l'inclusion des langages. Ces résultats sont à rapprocher des techniques de construction de système sécurisé par assemblage de composant. Finalement, nous présentons une autre approche pour la synthèse de système opaque qui consiste à synthétiser un filtre qui décide, dynamiquement, de masquer des événements observable afin d'éviter que de l'information secrète ne soit révélée. Ceci permet d'étudier dans un cadre formel la synthèse automatique de pare-feu assurant la confidentialité de certaines informations critiques