Show simple document record

dc.contributor.advisorFrappier, Marc
dc.contributor.advisorLanet, Jean-Louis
dc.contributor.authorSavary, Aymerickfr
dc.date.accessioned2016-10-14T13:55:36Z
dc.date.available2016-10-14T13:55:36Z
dc.date.created2016fr
dc.date.issued2016-10-14
dc.identifier.urihttp://hdl.handle.net/11143/9584
dc.description.abstractLa vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études.fr
dc.language.isofrefr
dc.publisherUniversité de Sherbrookefr
dc.rights© Aymerick Savaryfr
dc.rightsAttribution - Pas d’Utilisation Commerciale - Pas de Modification 2.5 Canada*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/ca/*
dc.subjectSécuritéfr
dc.subjectJava Cardfr
dc.subjectVérification de code intermédiairefr
dc.subjectTest d'intrusionfr
dc.subjectMutation de spécificationfr
dc.subjectTest à base de modèlefr
dc.titleDétection de vulnérabilités appliquée à la vérification de code intermédiaire de Java Cardfr
dc.typeThèsefr
tme.degree.disciplineInformatiquefr
tme.degree.grantorFaculté des sciencesfr
tme.degree.grantotherUniversité de Limogesfr
tme.degree.levelDoctoratfr
tme.degree.namePh.D.fr


Files in this document

Thumbnail
Thumbnail

This document appears in the following Collection(s)

Show simple document record

© Aymerick Savary
Except where otherwise noted, this document's license is described as © Aymerick Savary