Vérification de code Java/JavaCard

J'ai séjourné en mission de longue durée (4 mois) au sein de l'équipe Loop de l'université de Nimègue où je me suis consacré aux études de cas proposées par les partenaires industriels (SchlumbergerSema) du projet Verificard. Je compare en particulier les possibilités respectivement offertes par l'outil Loop développé dans cette équipe et Krakatoa où nos résultats sont mis en œuvre.

Les cartes à puces Java permettent de charger et d'exécuter des programmes écrits dans un sous-ensemble JavaCard du langage Java. Ces programmes sont d'une taille moyenne à cause des contraintes physiques de la carte. Comme il est important de garantir le fonctionnement sûr de ces programmes, on est amené à restreindre les constructions de langage utilisées à un sous-ensemble bien compris. Pour toutes ces raisons, les programmes JavaCard sont des candidats privilégiés à l'utilisation de méthodes de spécification et de preuve formelle.

Résultats.

• Un modèle par valeurs, de haut niveau, et
• Un modèle mémoire comportant une modélisation du tas où les objets sont alloués.

Une réflexion sur différentes approches de représentation du tas d'allocation a conduit au développement de prototypes permettant un traitement de programmes codés en un langage incluant strictement JavaCard, à l'aide de traduction du code source puis de génération des obligations de preuves Coq à partir d'annotations fournies par l'utilisateur.

Notre implantation de cette approche s'est établie suivant une architecture à trois outils :

1. Traduction fonctionnelle des programmes ( Krakatoa ),
2. Génération d'obligation de preuves (utilisant Why) et
3. Preuve assistée par Coq.

Mise en œuvre