Formal method applied to vulnerability testing

Sujets de thèse

Intitulé de la thèse
Formal method applied to vulnerability testing
Publication du sujet sur le site de l’ABG : NON
Nature du financement : Non connu à ce jour
Domaine de compétences principal (pour l’ABG) : Informatique, électronique
Domaine de compétences secondaire (pour l’ABG) : Mathématiques
Spécialité de doctorat : Informatique et Applications

Lieu de travail
Limoges ET Sherbrooke
Laboratoire d’accueil : XLIM/DMI

Introduction
Le test de vulnérabilité consiste à répondre à la question: existe il un chemin menant à un état donné si une pré condition de cet état n’est pas valide.
Pour ce faire nous utilisons un modèle formel (une représentation sous forme d’équation mathématique) pour lequel nous faisons subir des transformation puis nous cherchons une trace pouvant mener à un état désiré.

Présentation de l’équipe de recherche
voir: http://secinfo.msi.unilim.fr/

Résumé de la thèse en français
Dans le monde de la carte à puce l’activité de test représente 50% de l’effort total de développement. Elle est orienté fonctionnalité, elle est donc incapable de traiter les portes dérobées. Il s’agit donc de générer des suites de test pour détecter ce code non souhaité. On partira d’un modèle formel pour automatiser cette tâche.

Résumé de la thèse en anglais
Smart card testing represents around 50% of the development effort. Mostly oriented functionnal testing, it appears to be unable to detect backdors. For that purpose we have developped a methodology based on formal method to detect such code.

Description complète du sujet de thèse
Smart cards are the safer way to execute sensible algorithms. Nevertheless recent attacks have shown the ability to produce viruses in a smart card that exploit vulnerabilities in the card. In particular one providing an ill typed applet to upload in the card can beak the security of the platform. Thanks to byte code verification (BCV), such an applet could be detect. Most of the smart card manufacturers do not propose a complete BVC. This PhD thesis aims at characterizing the functionalities of the platform with security testing. In particular the student will pay attention to model testing i.e. using a formal model to generate security tests which are more efficient to detect vulnerabilities. The expected skills are:
– Formal methods:
– Languages: B, Coq, Alloy
– Proof, Model checking.

Objectifs scientifiques de la thèse
Développement d’une méthodologie de test de vulnérabilité.

Compétences à l’issue de la thèse
Modélisation mathématique de programme informatique, recherche de propriétés de sécurité.

Mots clés (séparés par des virgules)
Formal methods, smart card, vulnerability testing.
Conditions restrictive de candidature (nationalité, âge, …) : NON

Expérience/profil souhaité(e)
Bonne connaissance des méthodes formelles et de la théorie du test.

Directeur de thèse
Jean-Louis Lanet
Adresse mail du directeur de thèse : jean-louis.lanet@unilim.fr
Téléphone Directeur de thèse : 05 55 43 69 82

Co-directeur de thèse
Marc Frappier (Université de Sherbrooke)
Cofinancement LABEX SigmaLIM demandé : NON

Recherche

Menu principal

Haut de page