MORISSET Charles
Direction de recherche : Thérèse HARDIN
Co-encadrement : Jaume Mathieu
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.
Soutenance : 24/09/2007
Membres du jury :
Pr. Pierre-Yves SCHOBBENS, Université de Namur [Rapporteur]
Pr. Luca VIGANÒ, Università di Verona [Rapporteur]
Pr. Serge FDIDA, Université Paris 6
Pr. Claude KIRCHNER, INRIA/LORIA
Pr. Ludovic MÉ, Supélec Rennes
Pr. Thérèse HARDIN, Université Paris 6
M. Mathieu JAUME, Université Paris 6
Publications 2005-2009
-
2009
- L. Habib, M. Jaume, Ch. Morisset : “Formal definition and comparison of access control models”, Journal of information assurance and security (JIAS), vol. 4 (4), pp. 372-381 (2009)
-
2008
- Ph. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, Th. Hardin, M. Jaume, Ch. Morisset, F. Pessaux, R. Rioboo, P. Weis : “Trusted Software within Focal”, Trusting Trusted Computing ?, Rennes, France, pp. 162-179 (2008)
- L. Habib, M. Jaume, Ch. Morisset : “A formal comparison of the Bell & LaPadula and RBAC models”, Fourth International Conference on Information Assurance and Security, IAS'2008, Naples, Italy, pp. 3-8, (IEEE) (2008)
- M. Jaume, Ch. Morisset : “Un cadre sémantique pour le contrôle d’accès”, Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 27 (8), pp. 951-976, (Lavoisier) (2008)
-
2007
- Ch. Morisset : “Sémantique des systèmes de contrôle d’accès”, soutenance de thèse, soutenance 24/09/2007, direction de recherche Hardin, Thérèse, co-encadrement : Jaume, Mathieu (2007)
- M. Jaume, Ch. Morisset : “Contrôler le contrôle d’accès : Approches formelles”, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'07),, Namur, Belgium, pp. 227-244 (2007)
- A. Santana De Oliveira, Ch. Morisset : “Automated Detection of Information Leakage in Access Control”, Second International Workshop on Security and Rewriting Techniques - SecReT 2007, Paris, France (2007)
-
2006
- M. Jaume, Ch. Morisset : “Towards a formal specification of access control”, Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), Seattle, Washington, United States (2006)
- Th. Hardin, M. Jaume, Ch. Morisset : “Access control and Rewrite Systems”, 1st International Workshop on Security and Rewriting Techniques, SecReT'06, Venice, Italy, pp. 2-17 (2006)
- M. Jaume, Ch. Morisset : “A formal approach to implement access control”, Journal of Information Assurance and Security, vol. 1 (2), pp. 137-148, (Dynamic Publishers Inc., USA) (2006)
- J. Blond, Ch. Morisset : “Formalisation et implantation d’une politique de sécurité d’une base de données”, Journées Francophones des Langages Applicatifs (JFLA), Pauillac, France, pp. 71-86, (INRIA) (2006)
-
2005
- M. Jaume, Ch. Morisset : “Formalisation and Implementation of Access control models”, ITCC 2005 - International Conference on Information Technology: Coding and Computing, Las Vegas, United States, pp. 703-708, (IEEE) (2005)