Génération de tests de vulnérabilité pour des programmes Java Card itératifs

Utilisée très largement par le système bancaire actuel, la carte à puce peut être considérée comme un système critique. La majorité de ces cartes évoluent sous le système d'exploitation pour carte à puce Java Card, dont le code source est fermé. Leur évaluation repose donc sur des méthodes de tests en boîte noire, c'est-à-dire des méthodes dans lesquelles les tests générés ne se basent que sur la spécification fournie par le propriétaire du système sous test. Il existe différentes méthodes pour générer des tests en boîte noire mais l'intervention humaine nécessaire pour les concevoir est importante pour une couverture très souvent limitée. Des travaux ont donc été entrepris ces dernières années pour répondre à ces deux problématiques et ont abouti à la création de la méthode Vulnerability Test Generation (VTG). Appliquée à l'évaluation du vérifieur de code intermédiaire de Java Card (VCI), cette méthode a permis de générer de manière automatique des tests d'une grande qualité dans un temps réduit. Les travaux présentés dans ce mémoire ont permis d'aller plus loin dans l'étude de cette méthode en proposant de nouvelles approches et méthodologies. Nous avons ainsi pu expérimenter l'utilisation de différentes méthodes formelles de manière à établir un comparatif sur des critères de performance, d'adaptabilité et de coût en temps humain. Basés sur ces résultats, nous avons étendu le cas d'étude du VCI en modélisant de nouvelles instructions. Ces avancées ont rendu possible une évaluation plus complète des mécanismes de vérification du VCI