Les travaux proposés dans le projet se résument en 4 sous-projets principaux et 2 sous-projets de gestion du projet et de ses résultats :
SP1 - Modélisation comportementale des composants de sécurité
Les études de cas traitées dans le cadre du projet OSeP ont permis d’identifier des similarités de modélisation des composants de sécurité considérés. Celles-ci concernent à la fois la structures des données (clés, acteurs, codes d’erreurs, etc.) et les traitements liés à la sécurité (chiffrement/déchiffrement, contrôle d’accès, gestion des erreurs multiples, etc.). L’objectif de ce sous-projet est de se baser sur cette expérience pour faciliter la modélisation comportementale des composants de sécurité, dans le contexte de la génération automatique de tests. En particulier, nous proposons de définir un ensemble de patrons de conception permettant d’instancier une partie du modèle UML/OCL avec un DSML – Domain Specific Modelling Language –, et ainsi d’accélérer la phase de modélisation. De plus, ces artefacts stéréotypés seront optimisés en vue de simplifier les calculs réalisés durant la phase de génération des tests.
SP2 - Pilotage de la génération de tests et reporting
Ce sous-projet vise à l’amélioration de la qualité de la phase de génération de tests à deux niveaux. Le premier concerne la pertinence des tests produits, en proposant de prendre en compte des critères de génération de test basés sur une formalisation des propriétés de sécurité, en exprimant la dynamique du système dans une logique temporelle. Le second concerne la partie « reporting » qui permettra de donner aux utilisateurs des informations précises sur la couverture des propriétés de sécurité sous-jacentes. Ce sous-projet s’appuiera sur les résultats du projet ANR TASCCC ayant permis la définition d’un langage d’expression de propriétés temporelles (appelé TOCL) qui est adapté à l’expression des propriétés de sécurité dans le contexte des composants de sécurité. Les propriétés décrites dans ce langage sont traduites en automates, auxquels sont appliqués des critères de couverture spécifiques. Nous proposons ainsi de piloter la génération de test exploratoire, issue des résultats obtenus avec le prototype MBeeTle, par des propriétés TOCL ; la propriété servira de référence et fixera un objectif de couverture à atteindre. Un mécanisme de reporting, se présentant sous la forme d’un tableau de bord, viendra compléter le processus, en donnant à l’utilisateur un feedback précieux sur les parties de la propriété déjà couvertes, ou restantes à couvrir.
SP3 - Passage à l'échelle des algorithmes de génération automatique de tests
Ce sous-projet vise un saut d’un facteur 10 dans les capacités de génération automatique de tests de la technologie développée. Les limites actuelles, tant en temps de calcul qu’en consommation mémoire, rendent actuellement difficile le traitement des applications cibles dans un mode totalement automatisé. Les techniques actuellement utilisées pour contourner ces limitations (utilisation de scénarios, découpage des modèles) nécessitent des efforts supplémentaires de mise en œuvre, et ne sont parfois pas adaptées. Ce verrou technologique constitue un défi majeur pour l’acceptation dans l’industrie, et à grande échelle, des technologies de génération automatique de tests. Les algorithmes de génération automatique de tests, même guidés par le composant symbolique, engendreront des besoins de calcul de type haute performance. L'enjeu du passage à l'échelle est de taille mais peu étudié, une étude spécifique à la génération de tests sera donc nécessaire pour évaluer les méthodes de parallélisation les plus performantes et proposer une implantation adaptée aux algorithmes. L'idée initiale consiste à distribuer les parcours d'états entre différentes ressources mais ceci nécessite de résoudre le problème de synchronisation sur les parcours d'états. Ce travail s'appuiera sur les compétences développées au sein de FEMTO-ST sur les problématiques de parallélisation et de distribution d'algorithmes.
SP4 - Expérimentation sur des composants de sécurité
Ce sous-projet concerne l’évaluation expérimentale des techniques et outils proposés dans le cadre des sous-projets 1 à 3. En particulier, cette évaluation sera conduite autour de la validation de composants de sécurité. Nos études de cas reprendront celles introduites lors du projet ANR OSeP par l’équipe DGA MI / SSI associée au projet, et portant sur des composants cryptographiques matériels et logiciels. Ce sous-projet permettra de qualifier les progrès apportés par les nouvelles techniques proposées dans MBT_Sec par rapport aux objectifs fixés.