Show simple document record

dc.contributor.advisorFrappier, Marcfr
dc.contributor.authorSavary, Aymerickfr
dc.date.accessioned2015-02-24T14:39:54Z
dc.date.available2015-02-24T14:39:54Z
dc.date.created2013fr
dc.date.issued2013fr
dc.identifier.urihttp://hdl.handle.net/11143/6604
dc.description.abstractIl devient important d'assurer que tout système critique est fiable. Pour cela différentes techniques existent, telles que le test ou l'utilisation de méthodes formelles. S'assurer que le comportement d'un vérifieur de byte code Java Card n'entraînera pas de faille de sécurité est une tâche complexe. L'automatisation totale de cette vérification n'à popr le moment pas été realisee. Des jeux de tests coûteux ont été produits manuellement, mais ils doivent être refaits à chaque nouvelle spécification. Les travaux présentés dans ce mémoire proposent une nouvelle méthode pour la génération automatique de tests de vulnérabilité. Ceux-ci reposent sur l'utilisation et la transformation automatique de modèles formels. Pour valider cette méthode, un outil à été développé puis utilisé sur différentes implémentations du vérifieur de byte code Java Card. Le langage de modelisation que nous avons utilisé est Event-B. Nos modèles représentent le comportement normal du système que l'on souhaite tester. Chaque instruction est modélisée comme un événement. Leur garde représente l'ensemble des conditions que doit satisfaire une instruction pour être acceptable. À partir de ce modèle initial, une succession de dérivations automatiques génère un ensemble de modèles dérivés. Chacun de ces modèles dérivés représente une faute particulière. On extrait de ces nouveaux modèles les tests de vulnérabilité abstraits. Ceux-ci sont ensuite concrétisés puis envoyés à un système à tester. Ce processus est assuré par notre logiciel qui repose sur les API Rodin, ProB, CapMap et OPAL.fr
dc.language.isofrfr
dc.publisherUniversité de Sherbrookefr
dc.rights© Aymerick Savaryfr
dc.subjectSécurité et sûretéfr
dc.subjectTests de vulnérabilitéfr
dc.subjectJava Cardfr
dc.subjectProBfr
dc.subjectVérification de modèlefr
dc.subjectEvent-Bfr
dc.subjectMéthodes formellesfr
dc.titleGénération de tests de vulnérabilité pour vérifieur de byte code 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