Outils et techniques pour la vérification formelle de la plate-forme JavaCard
Institution:
NiceDisciplines:
Directors:
Abstract EN:
Bytecode verification is one of the key security functions of the JavaCard architecture. Its correctness is often cast relatively to a defensive virtual machine that performs checks at run-time, and an offensive one that does not, and can be summarized as stating that the two machines coincide on programs that pass bytecode verification. We review the process of establishing such a correctness statement in a proof assistant, and focus in particular on the problem of automating the construction of an offensive virtual machine and a bytecode verifier from a defensive machine.
Abstract FR:
La vérification du bytecode est l'une des pièces maîtresses de la sécurité de l'architecture JavaCard. Sa correction est souvent formulée en utilisant les notions de machine virtuelle défensive et de machine virtuelle offensive. La machine virtuelle défensive vérifie la cohérence des données manipulées pendant l'exécution alors que la machine offensive ne fait pas de telles vérifications. La correction est ainsi établie en vérifiant que l'exécution de programmes qui ont passé avec succès la vérification de bytecode, sur les deux machines, coi͏̈ncide. Dans cette thèse nous décrirons comment sont spécifiées de telles machines virtuelles et comment sont définis de tels énoncés de correction dans les assistants de preuve, et nous nous concentrerons en particulier sur le problème de l'automatisation de la construction de machines virtuelles offensives et de vérifieurs de bytecode à partir de machines virtuelles défensives.