RESPONSABLES : Didier BERT, Nicolas Stouls

TEL : 04 76 82 72 16
ADRESSE ELECTRONIQUE : Didier.Bert@imag.fr Nicolas.Stouls@imag.fr

LABORATOIRE ET EQUIPE : LSR - Équipe VASCO

TITRE : Détermination des états significatifs pour l'analyse de propriétés de sécurité.

RESUME :
Les logiciels mettant en jeu la sécurité doivent assurer l'intégrité (non altération des données), la confidentialité (accès contrôlé) et la disponibilité des informations qu'ils manipulent. Ces propriétés doivent être assurées, non seulement en fonctionnement normal, mais encore en cas d'attaques. Les "Critères Communs" permettent de déterminer la qualité des logiciels par rapport à ces objectifs. Il est donc important, pour les concepteurs de logiciels sécuritaires, de disposer de modèles et d'outils pour construire et analyser leurs applications, afin qu'elles soient sûres par rapport aux propriétés de sécurité.

Participant à des projets sur la sécurité (ACI Sécurité Informatique : projet GECCOO, IMAG : projet MODESTE) notre équipe travaille sur des méthodes et des outils pour la description de modèles de comportement et l'analyse de ces comportements. Nous utilisons la méthode B pour décrire les propriétés des logiciels à un haut niveau d'abstraction. La méthode permet ensuite de "raffiner" les modèles pour introduire les détails de l'implantation tout en assurant la préservation des propriétés de haut niveau. L'équipe dispose d'outils pour représenter des modèles B par des automates de transitions de manière à faire apparaître des comportements particuliers en fonction de l'état des variables à observer.

Le stage se situe dans ce cadre. Il consiste d'abord à étudier les propriétés de sécurité que l'on veut prouver sur un système. Ensuite, il devra permettre de déterminer quels sont les états significatifs minimaux d'un système dans lesquels une propriété de sécurité pourra être validée. Lorsque la technique de calcul de ces états sera mise au point, le travail consistera à écrire un programme pour réaliser ce calcul et produire un fichier d'entrée à l'outil GénéSyst. L'analyse des diagrammes produits devrait conduire à valider ou à invalider la propriété par rapport au système.

RESULTATS ATTENDUS :

Pratiques (réalisations) :
Construction des états permettant de valider une propriété de sécurité.

Théoriques (connaissances) :
Connaissance de la méthode B. Etude des propriétés de sécurité. Validation de propriétés sur un système.