Action de recherche coopérative INRIA

Java Card : sémantique, optimisations et sécurité

Programmation en Java pour les cartes à puce

L'un des intérêts majeurs du langage Java est la possibilité de télécharger du code et de l'exécuter de manière transparente. Cette pratique soulève de sérieux problèmes en matière de sécurité des informations (confidentialité, intégrité notamment). Java y répond, entre autres, par une plus grande sûreté de programmation (typage, vérification de code importé, héritage simple, etc.) et un gestionnaire de sécurité et des recommandations en matière de politique de sécurité. Le langage lui-même est supposé sûr mais cette affirmation est toujours sujette à débats d'autant plus qu'il n'y a pas de définition officielle formelle de la sémantique du langage. Il ressort clairement des déclarations contradictoires sur le fait que Java intègre un certain nombre de dispositions complexes qui rendent indispensable la formalisation du langage (pour le moins de certains de ses aspects critiques). Il s'agit en effet de caractéristiques particulières de Java qui ont un impact direct sur la sécurité et dont les définitions informelles ne sont pas exemptes d'ambiguïtés ou d'insuffisances.

Récemment, Sun a publié la définition d'une version de Java, appelée Java Card, destinée à la programmation de cartes à puces. Java Card a été conçu en enlevant un certain nombre de constructions de Java jugées inutiles ou trop complexes (il n'y a pas de ``threads'', la mémoire n'est pas récupérée automatiquement, le chargement de classes est plus restreint qu'en Java etc.), et en ajoutant des facilités spécifiques pour gérer des transactions avec une carte (atomicité d'un groupe d'opérations, objets persistants, etc.). La politique de sécurité de Java (dite ``bac à sable'') qui interdit toute interaction entre les objets de différentes applets, a été modifiée et assouplie. Ainsi, Java Card permet de partager un objet entre plusieurs applets.

L'aspect d'efficacité n'était pas prioritaire dans la définition de Java. Or, les ressources d'une carte à puce sont limitées aussi bien en terme de calcul que de mémoire. Les performances d'un code destiné à être exécuté sur une carte deviennent importantes. Il est donc nécessaire de disposer de techniques d'analyse et d'optimisation puissantes pour Java Card.

Objectifs

Axiomatisation des sémantiques statique et dynamique de Java Card et preuve de la sûreté du système de typage du langage (``subject reduction theorem'') à partir de cette axiomatisation. La propriété de sûreté est un préalable à toute spécification de politique de sécurité. Il est également envisagé de spécifier la machine virtuelle, sa sémantique, et le schéma de traduction entre Java Card et byte-code de la machine virtuelle (un sous-ensemble du byte-code de la JVM).
Spécifications de politiques de sécurité pour Java Card. La politique de sécurité définie pour Java Card diffère de celle spécifiée pour Java en permettant un partage plus ou moins restreint d'objets entre les applets chargées sur une carte. L'objectif est de formaliser cette politique de sécurité afin de pouvoir étudier son effet et les exigences qu'elle impose sur les composants d'une application Java Card. À partir de cette formalisation on se propose d'étudier comment prouver la conformité d'un programme vis-à-vis de la politique de sécurité.
Optimisation d'applications Java Card. Il s'agit d'adapter et de formaliser des méthodes classiques d'optimisation de programmes à Java Card ainsi que de développer de nouvelles techniques. Le but est de minimiser le temps d'exécution et la consommation de mémoire, tout en montrant que les optimisations ne mettent pas en péril la politique de sécurité. Transparents de R. Guider sur l'analyse de forme des structures d'objets.
Réalisation d'un environnement pour l'analyse sémantique de programmes Java Card en Centaur. Cet environnement devrait servir d'outil de développement de programmes Java Card. Pendant la conception, on disposera d'informations sur le typage des variables (e.g. l'ensemble des types dynamiques que peut prendre une entité du programme) et sur les propriétés concernant la sécurité de l' applet (e.g. l'ensemble des interactions avec l'environnement). Pendant l'exécution, on visualisera la topologie du graphe d'objets, leurs attributs, la constitution de sous-systèmes et leur interaction générées par l'utilisation d'applets, les communications avec le monde extérieur, etc. Transparents de C. Courbis sur l'environnement de développement Java Card

English Version