MORISSET Charles

PhD graduated
Team : SPI
Departure date : 10/01/2007
Supervision : Thérèse HARDIN

Sémantique des systèmes de contrôle d'accès

Un des aspects de la sécurité des systèmes d'information concerne le contrôle des accès aux données d'un système pour lequel différentes politiques de sécurité peuvent être mises en oeuvre. Toutefois, rien ne sert de mettre en place une politique de sécurité pour gérer un système si les programmes chargés de garantir le bon fonctionnement de cette politique ne sont pas fiables. Ne pas apporter de garanties fortes sur la correction de tels programmes reviendrait à construire un château fort avec une porte en papier. Nous utilisons les méthodes formelles pour aborder le contrôle d'accès avec pour objectif à long terme le développement d'une bibliothèque certifiée de politiques de sécurité. Tout d'abord, il s'agit de formaliser les politiques considérées afin d'identifier les hypothèses implicites et d'expliciter le système à modéliser. Ensuite, afin de valider cette étape, il s'agit de mécaniser cette formalisation. Nous présentons un exemple complet d'implantation d'un modèle de contrôle d'accès au sein de l'atelier Focal, nous permettant ainsi de concevoir un moniteur de référence appliquant la politique de Bell et LaPadula au sein d'un système de gestion de base de données. Enfin, pour permettre une réutilisation plus facile des développements formels obtenus, nous introduisons un cadre sémantique abstrait permettant de spécifier, d'implanter et de comparer des politiques de contrôle d'accès. Ce cadre permet d'identifier les "ingrédients" présents dans une politique de contrôle d'accès, et d'en comprendre le rôle dans une implantation. Il caractérise des propriétés de simulation entre implantations permettant d'exprimer qu'une politique est plus restrictive qu'une autre.
Defence : 09/24/2007 - 14h30 - Institut des Cordeliers 15 rue de l'Ecole de Médecine Escalier C, RdC.
Jury members :
Pr. Pierre-Yves SCHOBBENS, Université de Namur, Rapporteur
Pr. Luca VIGANÒ, Università di Verona, Rapporteur
Pr. Serge FDIDA, Université Paris 6, Examinateur
Pr. Claude KIRCHNER, INRIA/LORIA, Examinateur
Pr. Ludovic MÉ, Supélec Rennes, Examinateur
Pr. Thérèse HARDIN, Université Paris 6, Encadrante
M. Mathieu JAUME, Université Paris 6, Encadrant

2005-2009 Publications

 Mentions légales
Site map |