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.

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”, 1^st 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)