Show simple document record

dc.contributor.advisorFrappier, Marc
dc.contributor.authorLassale, Mathieufr
dc.date.accessioned2016-03-10T15:00:26Z
dc.date.available2016-03-10T15:00:26Z
dc.date.created2016fr
dc.date.issued2016-03-10
dc.identifier.urihttp://hdl.handle.net/11143/8563
dc.description.abstractLes 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.fr
dc.language.isofrefr
dc.publisherUniversité de Sherbrookefr
dc.rights© Mathieu Lassalefr
dc.subjectEvent-Bfr
dc.subjectVérifieur de byte codefr
dc.subjectVérification de structurefr
dc.subjectTests de vulnérabilitéfr
dc.subjectJava Cardfr
dc.subjectProBfr
dc.titleGénération de tests de vulnérabilité pour la structure des fichiers cap en Java Cardfr
dc.typeMémoirefr
tme.degree.disciplineInformatiquefr
tme.degree.grantorFaculté des sciencesfr
tme.degree.grantotherUniversité de Limogesfr
tme.degree.levelMaîtrisefr
tme.degree.nameM. Sc.fr


Files in this document

Thumbnail

This document appears in the following Collection(s)

Show simple document record