Proposition n° 37

Titre : Modélisation et vérification de politiques de sécurité

Responsable(s) : Marie-Laure Potet (Email : Marie-Laure.Potet@imag.fr), Nicolas Stouls (Email : Nicolas.Stouls@imag.fr)

Spécialité(s) :
  SL - Systèmes et Logiciels
  III - Intelligence, Interaction, Information

Laboratoire(s) :
  LSR

Description du Sujet :

Contexte :
Le sujet de DEA s'inscrit dans le cadre de la maîtrise de la sécurité des systèmes logiciels, domaine en pleine expansion.En effet la sécurité devient un aspect incontournable et nécessite d'être prise en compte dès les phases amont de la conception.

Sujet :
Différentes formes de politiques de contrôle d'accès sont utilisées en pratique. Des formalisations en déjà ont été proposées (voir référence ci-dessous) et les vérifications associées à ces politiques concernent principalement leur cohérence. Nous nous intéressons ici à la vérification "du respect" d'une politique par une application. Le but du travail de DEA sera de définir formellement ce lien dans le cadre de la méthode formelle B et de développer un outil permettant, à partir de la définition d'une politique de sécurité, de produire les obligations de preuve.

Résultats attendus :
Définition formelle de la notion de préservation de politique de contrôle d'accès, définition d'un langage de description des droits d'accès, développement d'un outil permettant de produire la spécification B associée. Validation sur une étude de cas.

Mots clés :
méthodes formelles, sécurité des systèmes, politiques de contrôle d'accès, raffinement et preuve

Ce sujet s'inscrit dans le cadre de différents projets dans lesquels l'équipe est impliquée: l'ACI sécurité GECCOO (Génération de Code Certifié Orienté Object), l'ACI sécurité POTESTAT (POlitiques de sécurité : TEST et Analyse par le Test de systèmes en réseau ouvert) et le projet IMAG MODESTE (Modélisation pour la Sécurité : test et raffinement en vue d'un processus de certification).