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.

Mots-clés: méthodes formelles; Event-B; vérification de modèle; ProB; Java Card; Tests de vulnerabilité; sécurité et sûteré

Abstract (AI English translation)

Information popover about translation disclaimer

It becomes important to ensure that any critical system is reliable. For this, different techniques exist, such as testing or the use of formal methods. Ensuring that the behavior of a Java Card byte code verifier will not result in a security breach is a complex task. Total automation of this verification has not yet been achieved. Expensive test sets have been produced manually, but they must be redone with each new specification.

The work presented in this dissertation proposes a new method for the automatic generation of vulnerability tests. These are based on the use and automatic transformation of formal models. To validate this method, a tool was developed and then used on different implementations of the Java Card byte code checker.

The modeling language we used is Event-B. Our models represent the normal behavior of the system that we wish to test. Each instruction is modeled as an event. Their custody represents all the conditions that an instruction must satisfy to be acceptable.

From this initial model, a succession of automatic derivations generates a set of derived models. Each of these derived models represents a particular fault. We extract abstract vulnerability tests from these new models. These are then concretized and sent to a system to be tested. This process is ensured by our software which is based on the Rodin, ProB, CapMap and OPAL APIs.

Keywords: formal methods; Event-B; model checking; ProB; Java Card; Vulnerability testing; security and safety