FORMALISATION DES PROPRIETES DE SECURITE DES OBSERVATEURS POUR LA VALIDATION DES TRANSFORMATIONS

Abstract

La modélisation des politiques de contrôle d’accès et les contraintes de sécurité ont comme objectif de décrire les aspects des différentes exigences de sécurité à un niveau d'abstraction plus élevé. Elle offre un cadre logique qui permet une meilleure caractérisation des propriétés qu’elles doivent satisfaire et donne un langage d’expression commun sans ambiguïtés. Pour réunir ces conditions, plusieurs méthodes ont été proposées, afin d'enrichir les formalismes des outils de modélisation existants et faciliter également la description et l'analyse de toutes les contraintes du contrôle d’accès et les contraintes spatio-temporelles. Une fois que la politique de contrôle d’accès est modélisée, la difficulté se situe dans l’expression et la vérification formelle des propriétés de cette politique. La formalisation permet également d’utiliser des outils mathématiques pour raisonner sur les modèles et vérifier les propriétés souhaitées. Cette vérification doit être effectuée quelle que soit la politique déterminée. Dans cette thèse, nous proposons d’élaborer un cadre formel et pratique pour la spécification et la validation de politiques de contrôle d’accès hybrides. Dans les situations d'urgence, les utilisateurs doivent parfois accéder à des ressources non autorisées dans des situations normales. Pour augmenter la flexibilité du contrôle d’accès, une extension du modèle UACML au modèle RBAC d’urgence (E-RBAC) est proposée. Nous commençons par la spécification semi-formelle des règles de contrôle d’accès à l’aide d’un méta-modèle que nous nommons E-UACML accompagnées de contraintes de contrôle d’accès et des contraintes spatio-temporelles. Un ensemble d’outils (E-UACML, Fiacre, OBP/CDL) pour exprimer et vérifier les propriétés de contrôles d’accès est introduit. Les modèles d’activité associés à E-UACML sont ensuite traduits en une spécification formelle exprimée dans le langage Fiacre et les exigences en automate observateur à l’aide du langage CDL. Ce dernier est utilisé pour vérifier formellement les propriétés avec l’outil OBP Explorer exploitant une technique de vérification formelle de propriétés de sécurité par Model-checking. Nous évaluons notre approche avec une étude de cas. Ainsi, nous concevons un modèle de contrôle d’accès générique, et de vérifier que les propriétés de sécurité sont respectées dans ce modèle.