HABIB Lionel
Supervision : Thérèse HARDIN
Co-supervision : JAUME Mathieu
Formalisations et comparaisons de politiques et de systèmes de sécurité
The objective of this thesis is to improve the degree of confidence that one can have in the domain of information security, by relying on formal methods. To do so, we define a generic semantic framework allowing to formalize and to compare security policies and systems. We describe two formalization approaches of security policies, and we show how we express administrative security policies according to these two approaches. We present the notion of security systems which consists in enforcing a security policy by a transition system according to two techniques allowing to obtain security systems which respect security policies by construction, which contributes to fulfill our objective. We introduce three preorders allowing to compare security policies and systems, which characterize their expressing power. We apply the definitions introduced in our framework by formalizing and comparing permissions, access and information flows control policies, administrative security policies, and security systems. On the other hand, we put in perspective our work with some related work. Finally, we expose two practical applications realized within Focalize, the test of a multi-level access control policy, and the development of a library of security policies, which allows us to show that our formal approach, intended to obtain a high level of assurance, is viable in practice.
Defence : 06/16/2011
Jury members :
Christèle Faure, SafeRiver [Rapporteur]
Ludovic Mé, Supélec [Rapporteur]
Valérie Viêt Triêm Tông, Supélec [Rapporteur]
Horatiu Cirstea, LORIA
Christian Queinnec, UPMC
Thérèse Hardin, UPMC
Mathieu Jaume, UPMC
2008-2011 Publications
-
2011
- L. Habib : “Formalisations et comparaisons de politiques et de systèmes de sĂ©curitĂ©”, thesis, phd defence 06/16/2011, supervision Hardin, ThĂ©rèse, co-supervision : 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)