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

Soutenance