Simulation d'Applications
Java Card

L'informatique a pris une place prépondérante dans notre vie de tous les jours durant ces vingt dernières années. Elle est utilisée partout : pour la gestion des capteurs dans nos voitures, pour aider les chirurgiens à opérer, pour les télécommunications, pour retirer de l'argent d'un guichet automatique avec une carte à puce, etc. Cette formidable évolution fut possible grâce au développement des technologies (aux progrès fulgurants de l'électronique) qui a permis, en autre, la réduction de la taille des éléments de stockage d'information (les transistors) dans les composants. Cette miniaturisation a permis d'augmenter la taille de la mémoire d'un composant et donc de passer d'une programmation proche de la machine (assembleur) à une programmation haut niveau avec, par exemple, des langages à objet (Java, C++, etc.).

Ce phénomène est en train d'apparaître dans le domaine très fermé des cartes à puces intelligentes (les smart cards) très populaires en Europe et au Japon mais encore peu développées aux Etats-Unis où on préfère utiliser les cartes magnétiques. Mais tout cela est en train de changer grâce à l'apparition de nouvelles puces plus puissantes permettant d'installer plusieurs applications sur le même composant. Par exemple, elles pourront contenir des données aussi disparates que de la monnaie électronique, des crédits téléphoniques, des informations médicales utiles en cas d'accident, etc. Il y a un intérêt grandissant pour les cartes à puce (la demande augmente de 40% par an [DRE98]). En effet, ces possibilités d'authentification et de stockage d'information permettent des accès sécurisés à l'Internet. Gemplus (un fabriquant de cartes à puce) estime qu'il y en aurait environ 3 000 millions à la fin de 2001.

Il y a deux sortes de cartes à puce : la carte à mémoire servant seulement au stockage d'information utilisant la logique pour accéder à l'information (ex : une carte de téléphone avec 50 crédits) et la carte à puce intelligente (celle qui nous intéresse dans ce rapport) qui est un mini-ordinateur. Elle contient un micro-contrôleur 8 bits (les plus connus étant les composants 6805 de Motorola et le 8051 d'Intel) qui a des propriétés de sécurité. Sa mémoire est composée de RAM où sont stockées les données temporaires (i.e. ces données sont perdues lors de la perte de courant), d'EEPROM où sont stockées les données sur le possesseur de la carte (ex : le numéro de compte bancaire, la clé privée d'encryption, etc.) et de la ROM où résident les programmes de la carte.

Le protocole ISO 7816 définit un ensemble de standards internationaux pour les cartes à circuit intégré avec contacts que doivent suivre les programmeurs d'application pour que les opérations soient possibles sur n'importe quel terminal (le lecteur de carte ou CAD : Card Acceptance Device) dans le monde entier qui fournit le pouvoir électrique à la carte. La structure de communication utilisée entre le CAD et la carte est un format standardisé de donnée : une APDU (Application Protocol Data Unit) qui est un message de commande du CAD vers la carte ou un message de réponse de la carte vers le CAD (cf. Figure 1 ).

Cla indique la classe de la commande, ins le code de l'instruction à faire, p1 et p2 sont les paramètres de la commande, lc est la longueur en octet des données, le est le nombre maximum des octets attendus pour la donnés de l'APDU de réponse. Sw1 et sw2 indiquent comment s'est passée la commande (le mot d'état).

En mars 1996, un petit groupe d'ingénieurs de Schumberger au Texas ont souhaité simplifier la programmation des cartes à puces tout en préservant la sécurité des données [GUT98]. Presque immédiatement, ils ont analysé que ce problème avait déjà été posé par le chargement de code sur le World Wide Web. La solution avait été Java. Malheureusement vu la taille de la mémoire disponible sur une carte à puce seulement un sous-ensemble de Java pouvait être utilisé (la taille de la JVM (Java Virtual Machine) et du système de runtime ne devant pas dépasser 12 kø). C'est ainsi qu'est né Java Card, le premier langage à objets adapté aux cartes à puces. Schlumberger et Gemplus sont les co-fondateurs du JavaCard Forum qui recommande des spécifications à JavaSoft (la division de Sun à qui appartient Java Card) en vue d'obtenir un standardisation du langage et il s'occupe aussi de la promotion des APIs (Application Programming Interface) Java Card pour qu'il devienne la plate-forme standard de développement des applications pour les smart cards

Java présente trois avantages majeurs pour la programmation des cartes à puce :

• C'est un langage haut niveau, à objets permettant l'encapsulation des données et la réutilisation de code. Ainsi les programmeurs n'auront plus besoin d'apprendre les langages assembleur 6805 ou 8051 pour réaliser une application pour une carte. La mise au point de programmes sera plus rapide et les temps de développement seront beaucoup plus courts. De plus, c'est un langage sûr : pas de manipulation de pointeurs, pas d'allocation de mémoire, ... C'est un langage fortement typé, avec des niveaux de contrôle d'accès (public, protected ou private) de ses membres (classe, méthodes, variables).
• Il est exécutable sur n'importe quel système d'exploitation (Motorola ou Intel) car son code est pré-compilé en byte-code qui est exécuté par la machine virtuelle Java (JVM). Donc cette portabilité permettra d'écrire du code qui fonctionnera sur n'importe quel micro-processeur de cartes à puces (" Write Once, Run Anywhere ").
• Il possède un modèle de sécurité qui permet à plusieurs applications de coexister en sécurité sur la même carte.

C'est un sous-ensemble de Java adapté aux cartes à puce. Sa syntaxe est légèrement moins riche à cause de la faible capacité mémoire d'une puce. C'est pourquoi, les utilisations de tableaux multidimensionnels, des types float, double ou long ou des modifiers transient et volatile ne sont pas autorisées [SUN1] ainsi que les threads. Ses APIs sont basées sur les standards 7816 et ont été adoptées par 95% des constructeurs de cartes à puce. Les applications Java Card sont appelées des applets [SUN2], identifiées uniquement par leur AID (Application IDentifier) isolées entre elles par des applets firewall. Elles possèdent 5 méthodes : la méthode install() qui permet de créer l'applet, la methode register() qui permet d'enregistrer l'applet au JCRE (Java Card Runtime Environment), les méthodes select() et deselect() qui permettent la sélection ou la desélection d'une applet et la méthode process() qui traite les APDUs de commande. Plusieurs applets pourront cohabiter sur une carte même si elles appartiennent à des fabriquants différents. Les applets d'une carte sont gérées par le JCRE. Les minima requis pour faire tourner un programme Java Card sont 16kø de ROM, 8kø d'EEPROM et 256ø de RAM [CHE98].

Java Card, bien qu'il soit un sous-ensemble de Java, possède des mécanismes spéciaux liés aux spécificités des cartes à puce. Ainsi il a 2 types d'objets : les objets transients (i.e. stockés en RAM qui perdront leurs valeurs lors du retrait de la carte, d'une coupure de courant, de la desélection de l'applet ou après chaque transaction) et les objets persistents stockés en EEPROM. Java Card permet de garantir l'atomicité des transactions. Il permet aussi de partager des objets entre applets sous certaines conditions. Les lignes de sécurité sont implémentées par la machine virtuelle.

Le gros avantage de Java Card est la possibilité de charger dynamiquement, n'importe quand, une nouvelle applet sur la carte. Cela signifie que le code des applets pourra être remis à jour.

L'usage de Java Card au lieu des assembleurs propriétaires utilisés actuellement pour coder des applications pour les cartes à puce permettra de réduire énormément le temps de réalisation. De plus il est possible d'utiliser les environnements de développement existants pour Java (par exemple Symantec Visual Café, Microsoft Visual J++, etc.) pour Java Card.

Malheureusement les erreurs de programmation ne sont pas exclues même avec un langage de haut niveau. C'est pourquoi les développeurs ont besoin d'outils pour les aider à vérifier le comportement de leurs applets Java Card avant leur mise en mémoire dans une carte à puce.

L'idéal serait de pouvoir vérifier le fonctionnement des applets sur une station de travail. Lors de cette simulation, on pourrait visualiser les objets, les attributs contenus par la carte, les APDUs transmises. Le but de notre étude est donc de construire un environnement basé sur la sémantique pour tester le fonctionnement d'applications Java Card.

Nous nous appuyons sur deux applets Java Card : PurseFr et FrequentFlyer qui permettent d'ajouter et retirer respectivement des francs et des miles.

La section 2 présente un état de l'art sur la sémantique et les outils existants. La section 3 explique la construction de notre environnement de simulation d'application. La section 4 présente les travaux futurs.

Il existe de nombreux travaux liés à la sémantique et à la sécurité de Java et plus récemment de Java Card. C'est pourquoi cette étude commence par une présentation des sémantiques formelles de Java (dont celle utilisée pour notre travail). De plus, il est nécessaire pour juger de la pertinence de notre travail de connaître les outils existants adaptés à Java Card i.e. le vérificateur statique (appelé checker) fourni par Sun et les outils commerciaux Odyssey-Lab de Bull, GemXpresso RAD de Gemplus et Cyberflex de Schlumberger.

1. Les Sémantiques Formelles de Java

1. Travaux Formels sur Java

Un important domaine de recherche est la preuve de la sûreté des types en Java. Drossopoulou, Einsenbach [DRO98] et Syme [SYM97] spécifient la sémantique de différents sous-ensembles Java séquentiels (incluants les types primitifs, les classes, l'héritage, les variables et méthodes d'instances, les interfaces, la surcharge des variables d'instance, la création d'objet Java, les tableaux et les exceptions) pour prouver que l'exécution d'un programme préserve les types. En rapport avec leurs travaux, Nipkow et Oheimb [NIP98] définissent et prouvent des propriétés sur leur sous-ensemble Java Light avec le prouveur de théorème Isabelle/HOL.

Börger et Schulte [BOR98a], pour leur part, définissent une sémantique dynamique par empilement de différents sous-ensembles Java.

2. Travaux Formels sur le Byte Code

Une autre approche pour prouver la sûreté des types est de travailler au niveau du byte code de la JVM. Qian [QIA98] a défini une sémantique pour un sous-ensemble d'instructions de la JVM. Les comportements de ces instructions dans la mémoire lors du runtime sont décrites comme des transitions d'états. Son but comme Börger et Schulte [BOR98b] est de prouver le bon fonctionnement du byte code lors de son exécution.

Joachim Posegga et Harald Vogt [POS98] définissent, pour leur part, un système à état fini pour la vérification de byte code pour Java Card. Eva Rose [ROS97] a elle aussi spécifiée un sous ensemble Java, JavaOb, assez restreint pour modéliser Java Card. Puis elle a définit une traduction de JavaOb vers un sous-ensemble de la JVM, JVMOb dont la sémantique statique correspond au vérificateur Java de byte code. Ainsi elle a obtenu une formalisation de son sous-ensemble et peut proposer une procédure de vérification de la sûreté du byte code.

3. Une sémantique naturelle pour Java

Cette sémantique [RUS97], [ATT97] (spécifiée par Marjorie Russo, doctorante du projet CROAP) est celle sur laquelle notre sémantique Java Card est basée (en modifiant le moins possible sa syntaxe et sa sémantique pour les adapter à Java Card).

Pour cette description formelle du langage, une sémantique big-step est adoptée pour l'héritage et les caractéristiques objets alors que le multithreading est spécifié par une sémantique small-step (ou opérationnelle). L'ensemble de cette spécification représente environ 400 règles Typol.

Cette sémantique naturelle spécifie un large sous-ensemble Java et est exécutable dans le système Centaur.

 

Le système Centaur est un outil de génération d'environnements de langages de programmation développé par le projet CROAP. Il permet de spécifier formellement des langages aussi différents qu'Eiffel, Esterel ou ASN1.

Pour spécifier un langage avec cet outil, il faut tout d'abord définir sa syntaxe concrète et sa syntaxe abstraite à l'aide du langage Metal. Cette première étape permet de générer un analyseur syntaxique (parseur). Son rôle est d'analyser syntaxiquement un programme et de créer son arbre de syntaxe abstraite. La deuxième étape est la spécification de règles d'affichage en Ppml pour générer un pretty-printer. Enfin la dernière étape est la spécification de la sémantique du langage à l'aide de règles Typol. De cette sémantique, on pourra constituer des outils d'aide à la programmation (comme par exemple un interprète ou vérificateur de type). La Figure 2 permet d'avoir une vue simplifiée du système.



Figure 2 Environnement de programmation construit avec Centaur

La Syntaxe

Le langage Metal permet de spécifier la grammaire de langages de programmation. Il se décompose en 2 parties :

• la syntaxe concrète utilisée pour analyser syntaxiquement un programme.
• la syntaxe abstraite utilisée pour construire l'arbre abstrait du programme.

Quand un fichier (contenant un programme du langage décrit) est lu sous Centaur, le parseur associé au langage utilisé dans le fichier construit l'arbre de syntaxe abstraite (cf. Figure 3 ) représentant le programme. Cet arbre sert de base pour faire de l'édition structurée, de la sémantique statique ou dynamique. En cas d'erreur syntaxique, l'arbre n'est pas généré et un message d'erreur apparaît. Le Tableau 1 présente des exemples de spécification de syntaxe concrète et abstraite écrits en Metal.

 

Exemple de syntaxe concrète en Metal: <VariableDeclaratorId>::=<Identifier> ; <Identifier> <VariableDeclaratorId>::=<Identifier>"[""]"; array(<Identifier>) (1) <Identifier> : := %ID ; identifier-atom(%ID) ;   Exemple de syntaxe abstraite en Metal: VariableDeclaratorId ::= array Identifier ; Identifier ::= identifier class ; Identifier -> implemented as IDENTIFIER ; Array -> Identifier ; (2) Class -> implemented as SINGLETON ;

Explications Le non terminal VariableDeclaratorId est utilisé lors de la déclaration d'une variable. Il décrit les variables de type tableau. Int varT[] ; Dans ce cas varT est analysé par la règle (1) de VariableDeclaratorId. L'arbre construit aura pour l'opérateur array et pour feuille un identifier i.e. dans ce cas varT En effet, comme cette règle s'applique, la fonction de construction d'arbre array(<Identifier>) est appelée. Elle correspond à un opérateur de syntaxe abstraite (2).

Tableau 1 Exemples de spécification de syntaxe écrits en Metal

Il faut spécifier un pretty-printer en langage Ppml pour qu'un arbre de syntaxe abstraite du langage soit visible dans une représentation textuelle (cf. Figure 4).

 

i
Figure 3 Arbre de syntaxe abstraite du célèbre programme HelloWorld.java (présentation arborescente)

i
Figure 4 Arbre de syntaxe abstraite du célèbre programme HelloWorld.java (présentation textuelle Java)

 

La Sémantique

Les sémantiques statiques et dynamiques doivent être spécifiées en Typol, qui est un langage dédié à la sémantique naturelle. C'est un langage déclaratif, logique, typé, manipulant la syntaxe abstraite du langage. Il fournit des mécanismes de filtrage, d'unification et de retour arrière.

Les règles peuvent être regroupées dans des sets

Le Tableau 2 présente un exemple de règle écrite en Typol.

 

A partir des spécifications décrites en Typol, Centaur permet de générer des outils sémantiques comme un vérificateur de type ou un interprète pour le langage. Le résultat d'un vérificateur de type sur un programme donné est une liste d'erreurs avec une référence de l'emplacement de chaque erreur dans l'arbre de syntaxe abstraite (ainsi l'erreur pourra être mise en exergue dans le programme). Au cours de l'interprétation d'un programme des structures sémantiques (contenant des informations utiles sur le comportement du programme comme par exemple la liste des objets créés par le programme ou bien la liste des variables statiques) sont construites. Donc un résultat possible de l'interprète pourrait être une de ces structures sémantiques (ex : la liste des objets et leurs attributs à la fin de l'interprétation). Ces résultats sont montrés dans des fenêtres spécifiques (textuelles ou graphiques). De plus, Centaur permet d'animer l'exécution d'un programme en utilisant des mises à jour incrémentales des fenêtres contenant les résultats.

 

Exemple de règle en Typol : Jugdement Object_L, O_Id |- Object ;   find_Apdu_attribute(identifier "commandApdu" |- ObjL1, AttrL1 -> AttrL2) -------------------------------------------------------------------------- ObjL1, OthId1 |- object(_, identifier "CAD", AttrL1, _, _, _, _); Do Update_apduL(APDU(OthId1, AttrL2) -> ApduL) & emit_tree("APDU", ApduL) ;

Explications Cette règle d'inférence ne s'applique que si l'objet a comme nom de classe CAD (mécanisme utilisé : le filtrage) et si la prémisse find_Apdu_attribute n'échoue pas. Cette prémisse recherche la référence de l'objet APDU, contenu par l'objet de type CAD donné, dans la liste d'attributs (AttrL1). Puis elle recherche cet objet dans la liste des objets du programme (ObjL1) pour en extraire la liste d'attributs pour une APDU de commande (AttrL2). Donc si la règle réussit, une mise à jour de la liste des APDUs est faite (update_apduL), suivie par son affichage dans la fenêtre APDU (cf. Figure 10).

Tableau 2 Exemple d'une règle Typol

2. Le checker Java Card

Pour compiler des programmes Java Card (cf Figure 5), il faut utiliser le compilateur de Java, javac, en précisant dans le classpath les librairies spécifiques à Java Card (i.e. throwable.jar, jc20api.jar, jcre.jar et jcsimulation.jar). Tout emploi de méthodes, exceptions ou classes n'appartenant pas à Java Card est détecté lors de cette phase de compilation.

Le compilateur javac, qui a un analyseur syntaxique adapté à Java et non à Java Card, ne peut garantir que le programme compilé est bien écrit en Java Card car certaines erreurs syntaxiques ne pourront pas être détectées.

Pour cette raison, Sun fournit en plus des librairies Java Card un utilitaire appelé checker qui permet de vérifier si les packages/applets sont écrits en Java Card et non en Java. Son rôle est de détecter l'usage de types ou de modifiers non supportés, d'opérations arithmétiques non autorisées et de classes, méthodes ou exceptions n'appartenant pas à Java Card. Cet outil travaille sur le byte code du programme (c'est pourquoi il lui est impossible de donner le numéro de ligne où se situe l'erreur).



Figure 5 La compilation d'un programme Java Card

Cet outil peut être utilisé de deux manières :

• Sur un programme Java Card pour tester des programmes compilés avec les librairies Java Card pour s'assurer que le programme est légal.
• Sur un programme Java pour connaître les modifications à apporter pour pouvoir le transformer en programme Java Card (le checker indiquera les classes, méthodes et exceptions non supportées).

3. Les outils commerciaux adaptés à Java Card

Actuellement il en existe trois: Odyssey-Lab de Bull, GemXpresso RAD de Gemplus et Cyberflex de Schlumberger. Les seules informations disponibles sont des documentations commerciales donc non objectives.

1. Odyssey-Lab de Bull
[BUL98]

C'est un environnement de développement fournissant les outils nécessaires pour optimiser et charger les applets (compilées avec un compilateur quelconque). Odyssey I (nom de la carte) est conforme aux spécifications Java Card API 2.0 et sa JVM est l'une des plus performantes du marché selon Bull. Son composant, développé par ST (auparavant SGS Thomson), a été conçu pour les besoins des plates-formes ouvertes et pour être adapté à de nouveaux mécanismes de sécurité (accès sécurisé aux secteurs partitionnés de la mémoire permettant une séparation étanche des applications, authentification ; intégrité et confidentialité assurées lors du chargement des applets ; cryptographie). La carte Odyssey offre en standard l'application de crédit/débit CCPS de Visa et 8 kø d'EEPROM pour des applications propriétaires (ex : programmes de fidélité, porte-monnaie électronique,...).

2. GemXpresso Rapid Applet Development (RAD) de Gemplus

Il est le premier membre d'une famille de produits de carte à puce supportant les APIs Java Card 2.0 pour 8 ou 32 bits. Son kit inclut 2 cartes pour le prototypage d'applets, un lecteur de carte et un environnement de développement. Cette plate-forme de développement est basée sur les spécifications de Java Card 2.0 et sur un processeur RISC 32 bits. Selon les informations commerciales données par Gemplus [GEM98] elle permettrait d'accélérer le développement et les tests des applets pour la programmation d'un prototype ou d'un pilote car elle contiendrait un simulateur intégré. De cette façon, les tests des programmes se feraient directement sur une station de travail. Il ne serait pas nécessaire de les charger sur une carte au préalable pour cette phase de mise au point car le simulateur permettrait de représenter ce qui se passe dans la carte. Malheureusement Gemplus ne donne pas plus d'informations techniques sur ce simulateur.

3. Cyberflex 2.0 Multi8K de Schlumberger [SLB97]

Cyberflex est une carte intelligente Java (appelée J-Card) 8 bits développée par Schlumberger qui peut exécuter des applications Java Card (les Cardlets). Elle est conforme aux spécifications de Java Card 2.0. Le kit vendu pour PC comprend à peu près les mêmes éléments que celui de Gemplus mais apparemment n'a pas d'environnement de développement car il serait très facile de l'intégrer dans un environnement de développement Java existant (comme par exemple Microsoft Visual J++).

Cet outil posséderait lui aussi un simulateur qui vérifierait le code d'une cardlet après la phase de compilation et d'édition de lien faite dans un environnement de développement Java quelconque. Pour l'utiliser, il suffirait juste de le lancer en cliquant dans le menu Tool de l'environnement utilisé, puis d'exécuter la cardlet. Il suffirait ensuite d'interagir avec la carte par l'interface graphique du simulateur. Il détecterait les erreurs fonctionnelles possibles du code avant que celui ne soit chargé sur la carte. Après cette simulation le byte code de la cardlet est modifié par MakeSolo (un outil du kit qui teste l'absence de caractéristiques non supportées et qui groupe les fichiers .class en un seul fichier) puis peut être chargé sur la carte Schlumberger par l'utilitaire LoadSolo.

 

Ces trois outils ne sont pas spécifiques à Java Card car ils permettent la mise au point de programme Java. Leur spécificité Java Card intervient au niveau du byte code (généré dynamiquement) avec une phase de vérification puis de chargement.

Tout d'abord, on indiquera les modifications apportées aux spécifications syntaxiques Java pour les adapter à Java Card. Puis on décrira un outil de vérification statique spécifié pour détecter la présence de tableaux multidimensionnels. Puis enfin notre simulateur d'application Java Card sera présenté.