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

• Main Author: Dubreil, Jérémy
• Language: ENG
• Published: Université Rennes 1 2009
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; Sécurité; Confidentialité; Opacité; Model Checking; Interprétation Abstraite; Synthèse de Contrôleur; Théorie des Jeux
• Online Access: http://tel.archives-ouvertes.fr/tel-00461306; http://tel.archives-ouvertes.fr/docs/00/46/13/06/PDF/main.pdf

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.