Vérification formelle de la plate-forme Java Card
Institution:
NiceDisciplines:
Directors:
Abstract EN:
In this thesis, we present a formalization, realized within the Coq proof assistant, of the Java Card platform. This programming environment derived from Java is intended to smart cards and to their security requirements. More precisely, we describe the formalization of the Java Card virtual machine and of a substantial part of its runtime environment. Then, we explain how to obtain, from this virtual machine dynamically verifying type safety, a bytecode verifier (BCV) and a virtual machine more effective for execution but as safe. We bring for the BCV a generic framework, expressed with modules, applying the most recent techniques from this domain and simplifying proofs needed to insure soundness of the built BCV. Finally, we show how the methodology applied for type safety can be generalized and describe tools realized to automate this task.
Abstract FR:
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 à puces intelligentes et aux impératifs de sécurités qu'elles requièrent. Nous décrivons alors la formalisation de la machine virtuelle Java Card et d'une partie conséquente de son environnement d'exécution. Nous explicitons ensuite comment, à partir de cette machine virtuelle vérifiant dynamiquement la sûreté du typage, obtenir un vérificateur de bytecode et une machine virtuelle plus efficace à l'exécution, mais aussi sûre. Nous apportons pour le BCV un cadre générique, exprimé sous forme de modules, appliquant les techniques les plus récentes de ce domaine et simplifiant les preuves à apporter pour assurer la correction du BCV construit. Nous montrons enfin comment la méthodologie appliquée pour la sûreté du typage peut être généralisée et décrivons les outils réalisés pour automatiser cette tâche.