Génération de tests de vulnérabilité pour vérifieur de byte code Java Card

Abstract

Il devient important d'assurer que tout système critique est fiable. Pour cela différentes techniques existent, telles que le test ou l'utilisation de méthodes formelles. S'assurer que le comportement d'un vérifieur de byte code Java Card n'entraînera pas de faille de sécurité est une tâche complexe. L'automatisation totale de cette vérification n'à popr le moment pas été realisee. Des jeux de tests coûteux ont été produits manuellement, mais ils doivent être refaits à chaque nouvelle spécification. Les travaux présentés dans ce mémoire proposent une nouvelle méthode pour la génération automatique de tests de vulnérabilité. Ceux-ci reposent sur l'utilisation et la transformation automatique de modèles formels. Pour valider cette méthode, un outil à été développé puis utilisé sur différentes implémentations du vérifieur de byte code Java Card. Le langage de modelisation que nous avons utilisé est Event-B. Nos modèles représentent le comportement normal du système que l'on souhaite tester. Chaque instruction est modélisée comme un événement. Leur garde représente l'ensemble des conditions que doit satisfaire une instruction pour être acceptable. À partir de ce modèle initial, une succession de dérivations automatiques génère un ensemble de modèles dérivés. Chacun de ces modèles dérivés représente une faute particulière. On extrait de ces nouveaux modèles les tests de vulnérabilité abstraits. Ceux-ci sont ensuite concrétisés puis envoyés à un système à tester. Ce processus est assuré par notre logiciel qui repose sur les API Rodin, ProB, CapMap et OPAL.