JAUME Mathieu

Habilitation
Forschungsgruppe : SPI
Datum, an dem das LIP6 verlassen wurde : 06.11.2008
https://lip6.fr/Mathieu.Jaume

Descriptions formelles : Comprendre, Corriger, Implanter, Résutiliser. Application au contrôle d'accès

Ce document présente une vue synthétique des travaux de recherche que j'ai menés de 1996 à 2008, d’abord comme doctorant puis comme enseignant-chercheur. Ces travaux reposent tous sur l’utilisation de méthodes formelles et ont pour objectif : obtenir une formalisation des entités étudiées à un niveau de détail proche d’une implantation, afin de les cerner complètement, d’en garantir les propriétés requises, d’en construire des implantations certifiées et également, de pouvoir réutiliser cette formalisation.
La section 1.1 du chapitre 1 présente quelques formalisations faites au cours de l’étude de la sémantique de la programmation logique dans l’assistant à la preuve Coq. Est ainsi décrite la SLD-résolution et donc, l’unification des termes, ce qui permet de construire une preuve du théorème de validité et de complétude validée par Coq. Suit une étude des exécutions infinies, faite en Coq, en les comparant à des lambda-termes de type co-inductif. Figurent également dans cette section la formalisation en Coq de la politique de sécurité de Bell et Lapadula et celle de l’algèbre de Mac Lean. La section 1.2 expose une étude sur la réutilisabilité de preuves en s’appuyant sur celles de la section 1.1. Est d’abord dégagé un critère de réutilisation de preuves concernant des entités de structure semblable (unification de termes/unification de pré-termes) mais différant par les techniques d’encodage de leurs propriétés (deep/shallow embeddings).
Le chapitre 2 est consacré aux politiques de sécurité. La section 2.1 porte sur le développement dans l’atelier FOCAL d’un cadre sémantique générique. Il caractérise les éléments communs à ces politiques et permet d’en dériver différentes implantations. Les constituants du modèle sont les ensembles de sujets, d’objets, d’accès et d’états ainsi que le prédicat définissant un état sûr. Un modèle de politique est défini par des informations statiques de sécurité et un langage de requêtes. Une implantation est définie par des états initiaux et une fonction de transition.
La section 2.2 étudie des critères de comparaison entre modèles : pré-ordre « plus restrictif » entre modèles sans obligation de partage des requêtes, définition d’un modèle réduit versus d’un implantation maximale et preuve que les comparaisons peuvent toujours être ramenées à celles des éléments minimaux (maximaux pour les implantations). Ces résultats permettent de comparer les flots d’information associés à ces politiques de sécurité et fournissent des critères de détection de flots non autorisés pour assurer confidentialité et intégrité. Les notions introduites permettent d’établir formellement que le modèle de la Muraille de Chine est strictement plus restrictif que le modèle de Bell et Lapadula, lui-même strictement plus restrictif que le modèle discrétionnaire HRU (à base de matrice de droits d’accès) qui est équivalent au modèle RBAC (à base de rôles).
La section 2.3 contient une étude des flots d’information engendrés par l’exécution d’un moniteur de référence implantant une politique de sécurité donnée. Elle porte sur la cohérence entre ces flots et les politiques de confidentialité et d’intégrité induits par le contrôle d’accès.
L‘annexe A présente l’atelier FOCAL. L’annexe B décrit les plongements de la sémantique des programmes logiques faits en Coq. Des exemples de réutilisation de preuve et de généralisation de modèles sont donnés dans l’annexe C et l’annexe D détaille certains exemples présentés dans le chapitre 2.

Verteidigung einer Doktorarbeit : 06.11.2008

Mitglieder der Prüfungskommission :

Hélène Kirchner (INRIA Bordeaux) [Rapporteur]
César Munoz (National Institute of Aerospace) [Rapporteur]
Luca Vigano (Università di Verona - Italie) [Rapporteur]
Irène Guessarian (LIAFA)
Thérèse Hardin (SPI - LIP6 - UPMC)
Ludovic Mé (Supelec Rennes), Isabelle Simplot-Ryl (Université Lille 1)

Datum, an dem das LIP6 verlassen wurde : 06.11.2008

2 Doktoren 2007 - 2011

Mentions légales
Plan