Au cours de mon stage post-doctoral au sein du projet Everest de l’INRIA Sophia-Antipolis, j’ai participé au développement de Jakarta.

Jakarta un outil de vérification formelle de plate-formes embarquées développé dans le cadre du projet RNTL CASTLES.

Après une revue intégrale du code, j’ai développé un système de types polymorphe et d’ordre supérieur pour le langage JSL qui est le langage d’entrée de Jakarta.

Le principe de base de Jakarta était de permettre de dériver (quasi)-automatiquement à partir d’une implantation de différentes stratégie de sécurité sur la plate-forme JavaCard, une machine abstraite ne tenant plus compte de cette stratégie et un vérificateur de bytecode permettant d’assurer que toute applet validée par ce dernier ne corromperait pas la machine d’execution. Une telle séparation permettant de valider les applets une fois pour toute AVANT la mise en service de ces dernières.

• Publications

This document was translated from L^AT_EX by H^EV^EA.