Vérification formelle
de la plate-forme
Java Card


Thèse de doctorat

Guillaume Dufay

Université de Nice Sophia Antipolis
INRIA Sophia Antipolis


Résumé

Dans cette thèse, nous présentons une formalisation, réalisée dans l'assistant de preuve Coq, de la plate-forme Java Card. Cet environnement de programmation est destiné aux cartes à puce intelligentes et à leurs impératifs particuliers de sécurité. Nous décrivons alors une formalisation complète et exécutable en Coq de la machine virtuelle Java Card et de son environnement d'exécution.

Nous proposons ensuite une méthodologie visant à vérifier des propriétés statiques de la plate-forme Java Card et centrée sur la machine virtuelle utilisée réellement lors de l'exécution. Nous montrons alors que cette machine virtuelle est aussi sûre que la machine virtuelle effectuant les tests de sécurité, à la condition que le programme exécuté ait passé la phase de vérification de code octet. Cette méthodologie, générique et automatisée par l'apport d'outils, est illustrée par l'application à la sûreté du typage, qui est une des composantes essentielles de la sécurité de la plate-forme Java Card.

Nous décrivons enfin la réalisation en Coq d'un vérificateur certifié et générique de code octet. Appliquant les techniques de vérification les plus récentes de ce domaine, il est implémenté à l'aide de modules, simplifiant alors les preuves à apporter pour assurer, à partir de la donnée d'une machine virtuelle, la correction du vérificateur de code octet construit.

Document

Disponible au format PDF.

Soutenance

Déroulée le vendredi 5 décembre 2003 devant le jury composé de :

Mme
Laurence Pierre
I3S, Université de Nice
Présidente
MM.
Thomas Jensen
IRISA / CNRS
Rapporteurs

Erik Poll
Université de Nijmegen, Pays-Bas

M.
Chris Hankin
Imperial College, Royaume-Uni
Examinateurs
Mme
Christine Paulin
Université Paris Sud

M.
Gilles Barthe
INRIA Sophia-Antipolis
Directeur


Transparents de la présentation disponibles au format PDF.



Guillaume Dufay