Boîte d'outils industrielle pour l'évaluation sécuritaire de composants de systèmes embarqués aux plus hauts niveaux des Critères Communs 3.0 – EDEN2

1. Introduction
Domaine : systèmes embarqués
Mots clés : évaluation sécuritaire, critères communs, méthodes formelles
Le projet pré-compétitif EDEN2 vise à industrialiser une nouvelle méthodologie et à offrir une boîte d'outils permettant de produire différents éléments essentiels répondant aux exigences de la nouvelle version 3.0 de la norme Critères Communs, et ce pour les plus hauts niveaux de sécurité (EAL5-7) : les modèles des différents niveaux d'abstraction, les preuves de raffinement, les tests et les documents associés. Pour atteindre cet objectif, nous identifions les difficultés rencontrées dans le milieu industriel et proposons des solutions adéquates. Notre objectif est de fournir un environnement industriel (EDEN) intégrant différents outils de modélisation, de preuve et de test et, à montrer l'efficacité de notre approche sur une application industrielle majeure. L'intégration des outils fournis par les différents partenaires du projet s'effectue en utilisant un format commun basé sur la technologie XML.

2. Objectifs de recherche
Le projet EDEN2 s'articule autour des deux objectifs principaux suivants :
1) Le premier objectif est d'industrialiser la méthodologie et les outils développés dans le projet exploratoire EDEN qui se termine en novembre 2005. Ce premier objectif porte sur les aspects suivants :
a) Interface
- Développement : gérer plusieurs niveaux d'abstraction dans les modèles jusqu'à l'implantation
- Réutilisation : permettre la réutilisation des modèles semi-formels (UML) définissant la vue conceptuelle des produits : ces modèles sont déjà réalisés par les concepteurs/développeurs
- Test : mettre en oeuvre des outils d'édition afin d'obtenir des plans de test conformes aux Critères Communs
- Propriété de sécurité : permettre l'expression de politiques de sécurité sous la forme de state charts UML ou de spécification dans le langage pivot de EDEN
b) Évolutions techniques du langage pivot du projet EDEN et des outils associés
- Expressivité : enrichir le langage de spécification pour exprimer des propriétés de sécurité plus complexes
- Développement : améliorer la mise au point par l'automatisation de l'abstraction et la génération de contre-exemples
- Certification : faciliter l'interprétation des résultats du model-checking
- Test : raffiner les jeux de tests générés à partir d'un niveau abstrait afin de produire des plans de tests exécutables sur le produit développé et tirer partie de ces opérations de concrétisation pour la complétude des couvertures de test de chaque niveau des modèles
- Raffinement : garantir la compatibilité entre le raffinement descendant (de la spécification informelle jusqu'aux modèles de différents niveaux) et le raffinement ascendant (rétro-ingénierie du code source pour reconstruire son modèle)
- Mise au point : utiliser au mieux la complémentarité test/preuve dans le cadre d'une évaluation Critères Communs : comment utiliser le test lorsque la preuve échoue (utiliser les outils de test pour caractériser les comportements qui font échouer la preuve).

2) Le deuxième objectif est d'évaluer la méthodologie et les outils dans le cadre d'une évaluation Critères Communs
a) Prise en compte de tous les niveaux d'architecture logicielle proposés par les Critères Communs : à cette occasion, les évolutions associées à la nouvelle version 3.0 de la norme seront prises en compte.
b) Mise à jour des fonctionnalités de production de fournitures d'évaluation, preuve et plans de test pour la version 3.O des CC
c) Validation d'une étude de cas industrielle par une évaluation de type CC : appliquer la méthodologie au composant Administrateur de carte développé par AXALTO. Cette validation consiste à réaliser la modélisation, le test et à fournir tous les éléments nécessaires répondant aux exigences des CC 3.0 pour les deux classes d'assurance ADV et ATE. L'intérêt de cette tâche est double : d'une