Vérification et analyse des politiques de contrôle d'accès : Application au langage XACML
Mémoire présenté comme exigence partielle de la maîtrise en informatique
par
Mahdi Mankai
Université du Québec en Outaouais
Janvier 2005

Résumé

Le contrôle d'accès définit des contraintes et des règles
d'autorisation. Pour exprimer les politiques de contrôle d'accès,
plusieurs langages tels que XACML, EPAL ou PONDER, sont utilisés. Ces
langages spécifient quels sujets sont (ou ne sont pas) autorisés
à accéder à un ensemble de ressources ou services pour actions
spécifiques.  Ces langages peuvent définir plusieurs règles et
politiques de contrôle d'accès, mais ils n'e s de mécanisme pour
éviter les conflits et les incohérences. Par exemple, il est possible
d'avoir plusieurs règles ou politiques appliquées à un contexte donné
et aboutissant à des décisions contradictoires.

Nous proposons dans ce mémoire, une méthode basée sur la modélisation
en logique de premier ordre pour analyser et détecter les interactions
ainsi que les conflits présents dans un ensemble de politiques de
contrôle d'accès exprimées en XACML. Le modèle logique obtenu
est traduit vers le langage ALLOY. ALLOY permet de spécifier des
ensembles de prédicats et d'assertions définissant les propriétés
d'un système. Nous pouvons ainsi analyser les interactions et les
conflits au sein des politiques de contrôle d'accès en utilisant un
outil spécifique. Nous avons développé cet outil afin de permettre
de visualiser les politiques XACML dans un format plus lisible et de
les transformer automatiquement en un modèle ALLOY. De plus, cet outil
utilise ALLOY Analyzer pour analyser et détecter les dts et incohérences
potentiels.e


Abstract

Access control requires authorization rules and constraints. To express
access control policies, several languages, such as XACML, EPAL or PONDER,
are used. These languages specify which subjects can (or cannot) access
sets of resources or services to perform specific actions. These languages
can define several access control policies and rules, but they do not
ny mechanism to avoid conflicts and inconsistencies among them. In fact,
it can happen that more than a rule or a policy, with opposite decisions,
is applicable in a given context.

We propose a method based on first order logic modeling to analyze and
detect possible conflicts and interactions within sets of access control
policies expressed in XACML.  We translate the model into a relational
first order logic language called ALLOY. ALLOY allows to specify sets of
predicates and assertions defining the properties of a system.  We can
then analyze interactions and conflicts among access control policies by
using a dedicated tool. We developed this tool to visualize XACML policies
and to translate them into ALLOY. In addition, this tool uses ALLOY
Analyzer to verify and analyse potential interactions and inconsistencies.