Ouvrir cette fenêtre en pleine page
  • Imprimer
  • Partager
    • Courriel
    • Twitter
    • Facebook
    • del.icio.us
    • Viadeo
    • LinkedIn

Détection de vulnérabilités appliquée à la vérification de code intermédiaire de Java Card

(Document en Français)

Accès au(x) document(s)

Modalités de diffusion de la thèse :
  • Thèse consultable sur internet, en texte intégral.
  • Accéder au(x) document(s) :
    • https://www.theses.fr/2016LIMO0048/abes
    • https://theses.hal.science/tel-01369017
    Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Informations sur les contributeurs

Auteur
Savary Aymerick
Date de soutenance
30-06-2016

Directeur(s) de thèse
Lanet Jean-Louis
Président du jury
Clavier Christophe
Rapporteurs
Julliand Jacques - Laleau Régine
Membres du jury
Lanet Jean-Louis - Girard Gabriel - Frappier Marc

Laboratoire
XLIM - UMR CNRS 7252
Ecole doctorale
École doctorale Sciences et ingénierie pour l'information, mathématiques (Limoges ; 2009-2018)
Etablissement de soutenance
Limoges,
Université de Sherbrooke (Québec, Canada)

Informations générales

Discipline
Informatique
Classification
Informatique

Mots-clés libres
Sécurité, Java Card, Vérification de code intermédiaire, Test d'intrusion, Mutation de spécification, Test à base de modèle, Event-B, ProB
Mots-clés
Systèmes informatiques -- Mesures de sûreté
Résumé :

La 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.

Informations techniques

Type de contenu
Text
Format
PDF

Informations complémentaires

Entrepôt d'origine
STAR : dépôt national des thèses électroniques françaises
Identifiant
2016LIMO0048
Numéro national
2016LIMO0048

Pour citer cette thèse

Savary Aymerick, Détection de vulnérabilités appliquée à la vérification de code intermédiaire de Java Card, thèse de doctorat, Limoges, Université de Limoges, 2016. Disponible sur https://aurore.unilim.fr/ori-oai-search/notice/view/2016LIMO0048