Les cartes à puce Java comportent plusieurs mécanismes de sécurité, dont le vérifieur de code intermédiaire (\emph{$ \ll $Java Card bytecode verifier$ \gg $}), qui est composé de deux parties, la vérification de structure et la vérification de type.
Ce mémoire porte sur la génération de tests de vulnérabilité pour la vérification de structure.
Il s'inspire des travaux sur la vérification de type de l'outil \textsc{VTG} (\emph{$ \ll $Vulnerability Tests Generator$ \gg $}) développé par Aymerick Savary.
Notre approche consiste à modéliser formellement la spécification de la structure des fichiers \textsf{CAP} avec le langage \textsf{Event-B}, en utilisant des contextes.
Cette modélisation permet de donner une définition formelle d'un fichier \textsf{CAP} valide.
Nous utilisons ensuite la mutation de spécification pour insérer des fautes dans cette définition dans le but de générer des fichiers \textsf{CAP} (\emph{$ \ll $Converted APplet$ \gg $}) invalides.
Nous utilisons \textsc{ProB}, un explorateur de modèles \textsf{Event-B}, pour générer des tests abstraits de fichiers CAP invalides.
La spécification formelle étant d'une taille importante qui entraîne une forte explosion combinatoire (plus de 250 constantes, 450 axiomes, 100 contextes), nous guidons \textsc{ProB} dans sa recherche de modèles en utilisant des valeurs prédéterminées pour un sous-ensemble de symboles de la spécification.
Ce mémoire propose un ensemble de patrons de spécification pour représenter les structures des fichiers CAP.
Ces patrons limitent aussi l'explosion combinatoire, tout en facilitant la tâche de spécification.
Notre spécification \textsf{Event-B} comprend toute la définition des structures des fichiers CAP et une partie des contraintes.
Des tests abstraits sont générés pour une partie du modèle, à titre illustratif.
Ces tests ont permis de mettre en lumière des imprécisions dans la spécification \textsf{Java Card}.
Ces travaux ont permis d'étendre la méthode de génération de test de vulnérabilité aux contextes \textsf{Event-B}.
De plus, le modèle proposé permet de tester, à l'aide du \textsc{VTG}, une partie plus importante de la vérification de structure du vérifieur de code intermédiaire.
| Identifer | oai:union.ndltd.org:usherbrooke.ca/oai:savoirs.usherbrooke.ca:11143/8563 |
| Date | January 2016 |
| Creators | Lassale, Mathieu |
| Contributors | Frappier, Marc |
| Publisher | Université de Sherbrooke |
| Source Sets | Université de Sherbrooke |
| Language | French |
| Detected Language | French |
| Type | Mémoire |
| Rights | © Mathieu Lassale |
Page generated in 0.0022 seconds