Direction de recherche : Thérèse HARDIN

Co-encadrement : JAUME Mathieu

Formalisations et comparaisons de politiques et de systèmes de sécurité

L'objectif de cette thèse est d'améliorer le degré de confiance qu'il est possible d'avoir dans le domaine de la sécurité de l'information, en s'appuyant sur les méthodes formelles. Pour ce faire, nous définissons un cadre sémantique générique qui permet de formaliser et de comparer des politiques et des systèmes de sécurité. Nous décrivons deux approches de formalisation des politiques de sécurité, et nous montrons de quelle manière nous exprimons des politiques de sécurité administratives selon ces deux approches. Nous présentons la notion de systèmes de sécurité qui consiste à mettre en oeuvre une politique de sécurité par un système de transition selon deux techniques permettant d'obtenir des systèmes de sécurité qui respectent des politiques de sécurité par construction, ce qui participe à remplir notre objectif. Nous introduisons trois préordres permettant de comparer des politiques et des systèmes de sécurité, qui caractérisent leur pouvoir d'expression. Nous appliquons les définitions introduites dans notre cadre en formalisant et en comparant des politiques de contrôle de permissions, d'accès et de flots d'information, des politiques de sécurité administratives, et des systèmes de sécurité. D'autre part, nous mettons en perspective notre travail avec des travaux connexes. Enfin, nous exposons deux applications pratiques réalisées avec l'atelier Focalize, le test d'une politique de contrôle d'accès multi-niveaux, et le développement d'une bibliothèque de politiques de sécurité, ce qui nous permet de montrer que notre approche formelle, destinée à obtenir un niveau d'assurance élevé, est viable dans la pratique.

Publications 2008-2011

• 2011
  • L. Habib : “Formalisations et comparaisons de politiques et de systèmes de sécurité”, soutenance de thèse, soutenance 16/06/2011, direction de recherche Hardin, Thérèse, co-encadrement : Jaume, Mathieu (2011)
• 2009
  • M. Carlier, C. Dubois, L. Habib, M. Jaume : “Politique de contrôle d’accès multi-niveaux : test de conformité vis à vis des flots avec l’outil FoCaL”, AFADL'09 - Approches formelles dans l'assistance au développement des Logiciels, Toulouse, France, pp. 145-160 (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)