Bilan LSR-IMAG fin parcours Geccoo

Marie-Laure Potet
Laboratoire LSR-IMAG

1 Équipe VASCO, LSR, Grenoble

Haddad Amal	Doctorant 2ème année
Didier Bert	CR CNRS
Sylvain Boulmé	MDC
Marie-Laure Potet	Professeur
Nicolas Stouls	Doctorant 3ème année
	BDI cofinancée STMicroelectronics

2 Rappel du positionnement des travaux du LSR

L'équipe VASCO-LSR était principalement impliquée dans les deux premières tâches du projet: Spécification de haut niveau (description B2.1 de la proposition initiale) et Raffinement et Programmation objet (description B2.2 de la proposition initiale). L'équipe a aussi largement contribuée au développement d'études de cas et particulièrement de l'application Demoney en B.

3 Résultat LSR tâche 1

Dans la tâche 1 les objectifs étaient les suivants:

définition d'un langage formel pour exprimer les propriétés de sécurité
définition précise d'une notion d'invariant de classe adaptée au modèle orienté objet
développement d'une méthode de construction de spécification par assemblage.

Ces activités combinaient des aspects méthodologiques (quelles sont les propriétés que nous voulons exprimer) et des aspects sémantiques (que signifie cette propriété). Les applications visées concernent le domaine de la carte à puce et les propriétés visées étaient de différente nature: contrôle d'accès aux commandes, intégrité et confidentialité des données, disponibilité des services, atomicité des transactions ...

Les contributions apportées par l'équipe VASCO sur la modélisation des propriétés de sécurité ont été les suivantes:

spécification en B de l'application Demoney et mise à disposition de la spécification (http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/)
proposition d'un langage de description de propriétés pour Génésyst à partir des travaux de l'équipe Lemme et expérimentation sur l'application Demoney ([])
développement d'un langage de description de différentes formes de politiques de contrôle d'accès (politique discrétionnaire, politique obligatoire multi-niveaux, politique basée rôle) et production des comportements attendus (outil MECA []).

Des travaux comparatifs ont aussi été menés avec l'équipe du LRI sur la spécification et la preuve de propriétés de sécurité exprimées sous la forme d'automates dans l'approche Java/JML comparée à l'approche B.

Un des aspects importants de la tâche 1 était l'étude de la notion d'invariant de classes (ou de modules) et la possibilité de modulariser les preuves d'invariant. Ces aspects s'avèrent essentiels pour pouvoir vérifier des applications de taille conséquente tout en maîtrisant les tâches de spécification et de vérification formelle et aussi pour pouvoir réutiliser et assembler des spécifications. Dans sa forme actuelle la méthode B offre un jeu de primitives de structuration qui permet de maîtriser finement la composition d'invariants, et les preuves associées. Dans la pratique, les règles imposées par ce jeu de primitives s'avèrent trop restrictives et obligent les spécifieurs soit à construire des architectures non nécessairement très naturelles soit à contourner d'une manière ou d'une autre ces restrictions. Dans les approches objet d'autres solutions sont adoptées, avec leurs propres difficultés et restrictions. Les résultats obtenus sont les suivants:

Analyse de la notion d'invariant dans différents langages (B, JML et Spec#) et comparaison (Dagsthul Seminar 06191 " Rigorous Methods for Software Construction and Analysis"¹).
Validation de la correction de la méthode B et proposition d'extension de cette méthode en utilisant les notions introduites dans l'approche Spec#² (statut des composants et relation d'appartenance) [].
Etude de patrons de spécification permettant aux spécifieurs de maîtriser la complexité des preuves d'invariant et de rester compatible avec un principe de substitutivité par raffinement (travaux en cours). Ces travaux ont aussi donné lieu à des collaborations avec l'équipe du LRI: en particulier une proposition d'interprétation des invariants de classe en présence de redéfinition a été élaborée.

4 Résultat LSR tâche 2

Dans la tâche 2 (Raffinement et programmation objet) les objectifs étaient les suivants :

Définition de conditions de préservation par raffinement des propriétés de sécurité définies en tâche 1.
Définition d'une notion de raffinement dans le cadre objet, et clarification de ses liens avec la structuration objet.

Différentes équipes ont travaillé sur ce thème, en particulier l'équipe de Besançon sur la préservation de propriétés temporelles par raffinement. Pour notre part, nous nous sommes intéressés au raffinement des données en lien avec les exigences de sécurité. En effet, dans le cas de politiques de contrôle d'accès une des difficultés est de manipuler des politiques à différents niveaux de spécifications (utilisateurs, pare-feux ...). Nous avons proposé une approche permettant de construire de manière systématique, par raffinement, des moniteurs de surveillance dans le cas des réseaux [, ]. Dans cette approche les données manipulées par les politiques sont raffinées et l'approche proposée permet de garantir la préservation de la politique abstraite. Ce travail a été réalisé en collaboration avec l'ACI Potestat.

Toujours dans la tâche Raffinement et programmation objet des études ont été menées pour développer un calcul du raffinement objet, en étendant l'approche B. Étendre le raffinement à la programmation OO suppose de pouvoir prendre en compte les fonctions impératives d'ordre supérieur (un objet étant une valeur du langage qui "transporte" des méthodes effectuant des effets de bords). Nous avons décrit en Coq un calcul de raffinement d'ordre supérieur et proposé une méthodologie pour prouver les fonctions impératives d'ordre supérieur via cette notion de raffinement [].

Parallèlement à nos travaux, le thème d'étendre les logiques de Hoare avec des fonctions d'ordre supérieur est devenu à la mode. En particulier, K. Honda, N. Yoshida et M. Berger³ ont proposé une logique complète. Par rapport à ce travail, nous supportons "moins" de fonctions d'ordre supérieur. Mais notre proposition se situe dans le cadre du raffinement: une extension de la logique de Hoare qui a prouvé son intérêt dans les gros développements industriels.

4.1 Les outils développés au LSR

Génésyst est un outil développé au-dessus de la boite à outils B (la BoB). Il permet de représenter un système B événementiel par un système de transitions étiqueté. La description peut correspondre à une spécification ou un raffinement. L'utilisateur caractérise dans la description B, l'ensemble des états qu'il souhaite voir apparaître. GénéSyst produit alors des obligations de preuve permettant de calculer les conditions de franchissement des transitions en terme de déclenchabilité et d'atteignabilité. Le fonctionnement de Génésyst est décrit dans [, ]. Il est disponible en téléchargement⁴ sous la licence CeCILL.

Des travaux été menés pour pouvoir utiliser d'autres démonstrateurs automatiques que celui intégré dans l'atelier B. L'adaptation de Barvey (interface développée au LIFC pour le démonstrateur haRVey du Loria) a du être reportée ultérieurement. C'est finalement le démonstrateur automatique de l'outil B4free qui a été adapté à GénéSyst.

Un prototype de l'outil Méca a été développé []. Il est actuellement en cours de reconception.

4.2 Les retombées pour le LSR

La première retombée des travaux développés dans le cadre de l'ACI Geccoo, pour l'équipe VASCO-LSR, est le montage du projet RNTL POSE avec les partenaires de Besançon. Sans ce projet, l'équipe Vasco est en charge de la définition d'un formalisme de description d'exigences de sécurité basé sur la méthode B, technologie utilisée par les partenaires industriels (Leirios et Gemalto). Dans ce cadre, nous redéveloppons une version de l'outil Méca, adaptée aux formes de politiques de contrôle préconisées par les Critères Communs⁵ et aux études de cas (plates-formes pour l'identification, l'authentification et la signature).

La seconde retombée concerne les travaux sur la modularité dans les langages de spécifications à états. Nous continuons à développer ces travaux, à la fois sur des aspects théoriques et sur les aspects méthodologiques.

1: http://kathrin.dagstuhl.de/06191/Materials2/Dagsthul
2: K.R.M. Leino and P. Müller, Object invariants in dynamic contexts, ECOOP, LNCS 3086, 2004
3: An Observationally Complete Logic for Imperative Higher-Order Functions, LICS'05
4: http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/
5: Common Criteria for Information Technology Security Evaluation, ISO/CEI 15408

Ce document a �t� traduit de L^AT_EX par H^EV^EA