Étude de la sécurité d’un vérifieur de byte code et génération de tests de vulnérabilité

Abstract

Les cartes à puce sont considérées comme étant des supports d’exécution d’applications et de stockage d’informations très sécurisés. Donc, elles doivent faire face aux accès malveillants en assurant leur propre sécurité par l’implémentation de plusieurs mécanismes de défense. En effet, la sécurité de Java Card repose sur le bon fonctionnement d’un ensemble de composants dédiés et qui opèrent de façon complémentaire. Mais vue la complexité de tels composants, leur éveloppement s’avère très délicat. Il devient alors primordial de s’assurer qu’ils sont bien implémentés car toute erreur à ce niveau peut être exploitée pour mener une attaque et éventuellement conduire à une défaillance du système ou encore révéler des données sensibles de la carte. Cependant, garantir la conformité d’un système n’est pas toujours suffisante et il devient donc nécessaire de détecter ses vulnérabilités en vue d’améliorer le niveau de sécurité. Dans ce présent travail, on s’est intéressé à un composant crucial pour la sécurité de la plateforme Java Card : le vérifieur de byte code. Nous avons proposé une approche d’analyse de vulnérabilité de ce composant dans le but de découvrir d’éventuelles failles de sécurité dans différentes implémentations de ce dernier. Cette approche se base sur un modèle formel B, construit à partir de la spécification du vérifieur, pour la génération de suites de test de sécurité qui seront soumises au vérifieur de byte code pour analyser sa réaction. Cette génération de données de test s’appuie sur la négation et la résolution de contraintes