Abstract

In this thesis, we present a formalization, realized within the Coq proof assistant, of the JavaCard 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 JavaCard 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.

Thesis

@phdthesis{ Dufay-PhD,
  author =       {Guillaume Dufay},
  title =        {V{\'e}rification formelle de la plate-forme JavaCard},
  month =        dec,
  year =         2003,
  type =         {Th{\`e}se de Doctorat},
  school =       {Universit{\'e} de Nice Sophia-Antipolis},
}

Defense