Formalisation de propriétés de sécurité pour la protection des systèmes d'exploitation

• Main Author: Rouzaud-Cornabas, Jonathan
• Language: fra
• Published: Université d'Orléans 2010
• Subjects: [INFO] Computer Science; [INFO] Informatique; Propriétés de sécurité
• Online Access: http://tel.archives-ouvertes.fr/tel-00623075; http://tel.archives-ouvertes.fr/docs/00/62/30/75/PDF/jonathan.rouzaudcornabas_2180_vm.pdf

Cette thèse traite du problème d'une protection en profondeur qui puisse être assurée par un système d'exploitation. Elle établit la faiblesse des solutions existantes pour l'expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc un langage qui permet de formaliser un large ensemble de propriétés de sécurité. Ce langage exprime les activités système directes et transitives. Il permet de formaliser la majorité des propriétés de confidentialité et d'intégrité de la littérature. Il est adapté à l'expression de modèles de protection dynamique. A titre d'exemple, un nouveau modèle dynamique est proposé pour la protection des différents domaines d'usage d'un navigateur Web. Nous définissons une méthode de compilation du langage pour analyser les appels systèmes réalisés par les processus utilisateurs. La compilation repose sur la construction et l'analyse d'un graphe de flux d'information. Nous montrons qu'en pratique la complexité reste faible. Une implantation de ce langage est proposée sous la forme d'un contrôle d'accès mandataire dynamique pour Linux. Une expérimentation à large échelle a été réalisée sur des pots-de-miel à haute interaction. Notre protection a montré son efficacité aussi bien pour les serveurs que les postes client. Il présente des perspectives intéressantes aussi bien pour la protection des systèmes que pour l'analyse de vulnérabilités. Ce travail a contribué au projet SPACLik vainqueur du défi sécurité de l'ANR SEC&SI.