Vérification de code Java/JavaCard

Je me suis intéressé à la vérification de code JavaCard au sein du projet européen Verificard. Celui-ci regroupe plusieurs partenaires académiques (l'INRIA, l'université de Nimègue aux pays-bas, l'université technique de Munich en Allemagne, SICS en Suède, etc.) mais aussi des partenaires et utilisateurs industriels (notamment SchlumbergerSema, Oberthur, Ericsson, etc.) qui fournissent des études de cas issues de leurs groupes de développement. Il concerne la vérification d'une nouvelle génération de cartes à puces.

J'ai séjourné (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. J'ai comparé 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.

Nous avons défini deux modèles logiques différents permettant de représenter les applets JavaCard dans l'assistant de preuve Coq :

• 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.

Dans le même temps, j'ai travaillé à la définition de méthodes permettant de distinguer les programmes Java/JavaCard contenant des alias, seuls susceptibles de rendre la traduction fonctionnelle incorrecte. Des critères (vérifiables statiquement) dits de linéarité ont été proposés afin de pouvoir sélectionner, parmi les modèles Coq de représentation des objets qui ont été définis, le plus pertinent : par valeurs, dans le cas sans alias, ou avec représentation du tas, si des alias sont détectés.

Mise en œuvre.

Je suis coauteur (avec Claude Marché) de l'outil de traduction fonctionnelle Krakatoa. Il fournit, sur l'entrée d'un programme Java ou JavaCard (et donc impératif) annoté en JML, un programme ayant la même sémantique mais destiné au générateur d'obligations de preuve Why, c'est-à-dire fonctionnel avec quelques traits impératifs : exceptions et références. Ce travail est arrivé à maturité et un premier prototype a permis de traiter des exemples de programmes simples. Une version de distribution est prévue pour janvier 2003. Un exposé ainsi qu'une démonstration ont été présentés au workshop Verisafe de Nice les 19 et 20 septembre 2002. Un article sur cette approche a paru dans le journal JLAP [ps.gz].