MORISSET Charles
Supervision : Thérèse HARDIN
Co-supervision : 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.
Defence : 09/24/2007
Jury members :
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
2005-2009 Publications
-
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”, thesis, phd defence 09/24/2007, supervision Hardin, ThĂ©rèse, co-supervision : 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)