La vérification du bytecode d'applications Java Card est utilisée pour assurer la sécurité en matière de confidentialité et d'intégrité des données. En effet, il est possible d'enregistrer, au sein de la même carte à puce, plusieurs applications, et ce même après sa fabrication. Une application malveillante installée sur une carte contenant des données sensibles ou confidentielles, comme une carte de paiement bancaire, peut effectuer plusieurs actions qui pourraient mettre ces données en péril. Cette vérification permet de réduire au minimum les risques. Mise en situation Les cartes à puce sont des composants petits et peu chers, très portables, principalement utilisés pour différentes applications : cartes de crédit, cartes SIM de téléphone portable, cartes vitales... À l'origine, une carte contient une seule application, qui est développée et compilée afin de fonctionner uniquement sur cette carte. Les Java Card apportent donc de la nouveauté : Il est possible d'insérer dans une Java Card plusieurs applications, qui seront cloisonnées les unes des autres et ne pourront communiquer que d'une manière restreinte Une applet Java Card peut être installée sur toutes cartes à puce contenant une JCVM (Java Card Virtual Machine) Les paragraphes suivants présentent le déroulement classique du développement d'une applet. Les Java Card et le développement d'applications Lorsque l'on veut développer une application Java Card, il y a plusieurs similitudes avec le développement d'applications Java classiques. Néanmoins, au vu des restrictions matérielles des cartes à puce, notamment au niveau de la mémoire et de la puissance de calcul, il y a quelques étapes en plus : Écrire le code source de l'application que l'on souhaite développer, en utilisant Java dans sa version J2ME, Compiler le code source, pour créer les fichiers .class, Convertir ces fichiers .class en fichiers CAP (Converted Applet), Vérifier la validité du fichier CAP, ce qui inclut la vérification du bytecode ; cette étape est optionnelle, Installer le fichier CAP sur la carte à puce. La partie 3 est l'une des étapes ajoutées au déroulement classique. Cette conversion permet d'optimiser le code afin de l'installer sur une architecture comme celle des cartes à puce.
Dans cet article, nous allons nous intéresser particulièrement à la partie 4, mais la compréhension de ce processus aide à la compréhension de la suite. Nous allons voir maintenant l'intérêt de cette vérification. Les enjeux de la vérification de bytecode Java Card Bien que les spécificités des Java Card permettent une grande flexibilité, elles apportent des risques de sécurité. L'installation d'une application malveillante sur la carte à puce expose au risque que cette application accède à des informations sensibles, telles des données bancaires ou médicales. L'environnement Java réduit ces risques en cloisonnant chaque application dans une "sandbox", qui sert d'interface de contrôle d'accès entre l'application et les ressources matérielles, comme le support de stockage. La machine virtuelle Java Card (JCVM) ajoute une abstraction au niveau des données. On n'accède pas aux données à partir d'une adresse mémoire, mais à partir d'une référence. On évite donc d'accéder directement à une zone mémoire.
Malgré cela, il est toujours possible, dans certains cas, d'accéder à tout ou partie de la mémoire, en outrepassant les sécurités mises en place. C'est pourquoi la vérification de bytecode a été mise en place. Elle analyse les instructions, afin de s'assurer qu'aucune action illégale n'est effectuée.
Techniques de vérification de bytecode Java Card Il existe différentes manières de vérifier le bytecode Java Card. Une des manières est la vérification Off-Card, ce qui signifie que la vérification est effectuée en dehors de la carte. Vérifications Off-Card Description On effectue la vérification de bytecode lors de la vérification des fichiers CAP. Les fichiers CAP contiennent des composants (traduit de Component). Il existe plusieurs types de composants : composant de classe, composant de méthode, etc. et chaque composant contient un indicateur pour déterminer son type, et des données. Le composant qui nous intéresse est le composant de méthode (Method Component). En effet, c'est à partir de ces composants que l'on va commencer la vérification.
Cette vérification de bytecode a été développée par Sun. Elle se nomme Type Deduction (Déduction de type) et a été créée par Gosling et Yallin.
Fonctionnement La vérification d'un fichier CAP se fait en deux étapes : Lire les données du composant Vérifier les données Le composant de méthode contient une méthode verify(). En l'exécutant, on va parcourir l'ensemble des méthodes du composant, et exécuter l'action verifyMethod().
Cette fonction a plusieurs usages : Vérifier la validité de quelques informations de base : les bornes, les en-têtes et les exception handlers, Faire une vérification de type La vérification de type sert à s'assurer que le bytecode n'essaye pas de convertir un entier de type short en entier de type int, ou bien d'utiliser une valeur entière comme référence mémoire. Elle démarre en appelant la méthode typecheck().
Elle fonctionne en deux temps : Un appel à static_check(), qui va vérifier que les instructions de la méthode en cours de vérification contiennent des opérandes avec des valeurs appropriées. Par exemple, une instruction de branchement, qui est chargée d'effectuer un saut vers une autre instruction, doit obligatoirement faire un saut vers une instruction appartenant à la même méthode. Cette partie de la vérification est relativement aisée et rapide. Ensuite, elle se charge de vérifier le contexte de chaque instruction, à l'aide de ce que l'on appelle un interpréteur abstrait (an abstract interpreter). Cet interpréteur va simuler l'exécution de chaque instruction, mais au lieu d'utiliser les valeurs des données, il va utiliser leur type. Afin de comprendre un peu mieux le fonctionnement, voyons comment la Machine Virtuelle Java Card exécute des instructions. La JCVM et l'interpréteur abstrait utilisent les mêmes outils pour exécuter une instruction : Un pointeur d'instruction, qui indique l'emplacement de l'instruction en cours d'exécution (program counter), Une pile d'opérandes, qui contient différentes choses selon qu'il s'agit de la JCVM ou de l'interpréteur abstrait (operand stack), Un ensemble de variables locales (set of local variables), Un curseur sur la pile d'opérandes, qui s'incrémente ou se décrémente selon qu'on ajoute un opérande dans la pile ou inversement (stack pointer). La pile d'opérandes, ainsi que les variables locales, contiennent lors d'une exécution normale sur une JCVM un ensemble de valeurs, correspondant à des données. Lors d'une exécution à partir d'un interpréteur abstrait, elles ne contiennent pas les valeurs, mais leur type.
Ces quatre point définissent l'état d'exécution de la méthode.
Afin de mieux comprendre ce qui est fait lors de la vérification, prenons l'exemple d'une instruction de multiplication de deux entiers : imul.
Cette instruction ne prend aucun paramètre. Elle va prendre les deux premières valeurs de la pile d'opérandes, faire la multiplication puis insérer le résultat dans la pile. L'interpréteur abstrait, lui, ne va pas faire de multiplication. Il va tout simplement vérifier que les deux premières valeurs de la pile sont des entiers, les retirer, puis ajouter un type Entier dans la pile (là où on aurait dû mettre le résultat de la multiplication). Si jamais le vérificateur détecte une anomalie, la vérification s'achève en échec.
Jusque-là, la vérification ne semble pas si difficile à mettre en place. Mais lorsque l'on tombe sur des instructions de type "branchement" ou "exception", cela se complique.
En effet, au moment où on tombe sur un branchement, il est impossible de déterminer à quelle instruction on va arriver, tout simplement parce qu'on utilise les types et non les valeurs. Par exemple, on peut savoir qu'il y a un booléen, mais impossible de savoir s'il vaut "true" ou "false". Il faut ainsi vérifier tous les cas possibles. On utilise pour ce faire un "dictionnaire".
Pour faire simple, une entrée dans le dictionnaire correspond à un cas possible de branchement ou d'exception. Chaque entrée dispose de sa propre pile et de ses variables locales. On va donc parcourir l'ensemble des instructions, pour chaque possibilité, et ajouter, retirer ou modifier la pile. Puis on passe à l'étape d'unification, qui consiste à trouver, parmi la pile de type de l'instruction de branchement et la pile de type de l'instruction en cours, le type parent le plus proche. On peut apparenter cela à l'héritage de classes, où toutes les classes découlent de la classe Object. On a donc un arbre de types, et le but ici est de trouver le nœud dans l'arbre qui contient, dans ses branches, les deux types recherchés, tout en n'ayant aucun autre nœud comportant cette caractéristique. Le dictionnaire est donc susceptible d'être modifié. Ces étapes sont exécutées, jusqu'à ce que toutes les instructions aient été vérifiées sans avoir modifié le dictionnaire. Lors de l'opération d'unification, on va comparer les deux piles, afin de trouver les types parents communs. Si jamais les deux piles n'ont pas la même taille, la vérification renvoie une erreur.
Cette partie est la plus couteuse, en particulier en termes de mémoire, car il faut stocker le dictionnaire qui peut atteindre des tailles assez importantes, par rapport à ce qu'on peut trouver sur une carte à puce. De plus, il faut le stocker sur la mémoire vive, car le nombre de lectures/écritures est souvent important.
Certains chercheurs ont analysé cet algorithme de vérification, et ont cherché à l'optimiser pour que l'exécution puisse se faire directement sur la carte.
Vérifications On-Card Description La vérification permet à l'application générée de contenir du bytecode fiable, qui ne pose aucune problématique de sécurité. Mais une applet, même vérifiée, peut être modifiée et redistribuée. Le schéma suivant illustre parfaitement ce principe : thumb|centré|Principe de la Vérification de bytecode Java-Card On-Card Ainsi donc, entre la phase de vérification et celle d'installation de l'applet, il y a un risque. En intégrant la vérification sur la carte, on fait tomber ce risque à zéro.
Mais les problématiques matérielles expliquées plus haut font qu'il est impossible d'intégrer un vérificateur tel quel sur une carte à puce, à moins de procéder à quelques optimisations. C'est ce qu'ont tenté de faire certains chercheurs, notamment Xavier Leroy ou encore Tongyang Wang et son équipe.
Ces derniers ont tenté de mettre en place un vérificateur basé sur celui de SUN, mais en essayant d'optimiser la place en mémoire. En effet, afin que la vérification fonctionne, les structures utilisées (pile, dictionnaire...) doivent être stockées en mémoire RAM. Or, une Java Card typique contient en moyenne de 3 à 6 ko, ce qui n'est pas suffisant. Ces chercheurs ont donc implémenté un algorithme, nommé Cache Scheduling Policy, qui va permettre d'utiliser le stockage de la carte, et de basculer les données nécessaires à l'instant t en RAM, à la manière d'un cache. L'algorithme détermine à quel moment telle données sera nécessaire, pour que l'opération soit performante. Cet algorithme utilise les graphes LFG (Logical Flow Graph).
Dans cet article, nous allons parler de la méthode expliquée par Xavier Leroy. Fonctionnement Algorithme D'après l'analyse de Xavier Leroy, on peut arriver à un constat concernant la vérification Off-Card : bien souvent, la pile d'opérandes est vide, et un registre (une variable locale) est toujours du même type du début à la fin. Évidemment, il peut arriver que ces deux points soient erronés, mais cela arrive suffisamment peu souvent pour que l'on optimise le vérificateur pour ces deux cas.
Il a donc imposé deux prérequis au vérificateur :