De la spécification à l’implémentation de règles de controle d’accès dans les systèmes d’information.

22 novembre 2010

Jérémy Milhau (LACL)

Comment spécifier des règles de contrôle d’accès dans un système d’information en s’assurant du respect de propriétés de sécurité, du non blocage du système et d’un pouvoir d’expression suffisant ? En utilisant des notations formelles, il est possible d’exprimer des règles de controle d’accès, mais aussi de les valider ainsi que de prouver et vérifier des propriétés de sécurité. Cet exposé présentera une méthode proposée dans le cadre des systèmes bancaires et hospitalier. Elle se base nottament sur les langages et notations formelles ASTD, B et Event B. Plusieurs étapes inspirées de l’approche MDA seront présentées : la phase de spécification ; la validation du modèle ; la vérification de propriétés ; la traduction systématique ; l’implémentation par raffinement d’un filtre de sécurité pour SI.