Abstract FR:

Un des aspects de la sécurité en informatique concerne le contrôle des accès aux données d'un systèm. 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, il s'agit de mécaniser cette formalisation. Nous présentons un exemple d'implantation d'un modèle de contrôle d'accès au sein de l'atelier Focal, nous permettant de concevoir un moniteur de référence appliquant la politique de Bell et LaPadula au sein d'un SGBD. 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 modèles de contrôle d'accès. Ce cadre caractérise des propriétés de simulation entre implantations permettant d'exprimer qu'un modèle est plus restrictif qu'un autre