Projet : Pour L'Utilisation et l'aMÉlioration
de la déduction automatique

Précédent : Autour de Coq Remonter : Fondements scientifiques Suivant : Commerce électronique sécurisé

Une application au commerce électronique : la carte Java

 

Participants : Eva Rose, Kristoffer Rose, Pierre Lescanne.

Mots clés : Carte Java, systèmes intégrés, code mobile, applets, sécurité, réseaux, vérification de bytecode, machine virtuelle Java (JVM), Systèmes de types pour bytecode, sémantique opérationnelle .

Résumé :

Le but de cette activité est de formaliser les caractéristiques d'une architecture pour un langage «micro-Java» adapté au code mobile sur des cartes bancaires dites «intelligentes», pour des applications comme des systèmes de fichiers à même la carte, des vérificateurs, etc., et de réaliser les applications pour démontrer la validité en pratique des théories de sécurité basées sur l'approche formelle sans utiliser la cryptographie.

Par micro-Java, nous entendons un petit sous ensemble de Java, assez petit pour pouvoir être compilé dans un sous ensemble de la JVM, réalisable (ainsi que son vérificateur) sur une carte bancaire. Nous travaillons sur une spécification formelle d'une sémantique d'un tel sous-langage de Java pour carte à puce, et d'un «bytecode» correspondant, pour formaliser la traduction du sous-langage de Java vers la JVM et pour formaliser l'exécution correcte de ce sous-langage sur la carte à puce. Un algorithme, dit «Lightweight Bytecode Verification» (LBV), permet de vérifier la sûreté des codes mobiles Java, appelés aussi applets ; ceux-ci transitent, en général, sur des réseaux non sécurisés et sont exécutés sur une carte Java ou sur un processeur intégré ayant très peu de ressources. Cette technique qui repose sur la notion de certificat envoyé avec le code mobile permet d'éviter un mécanisme lourd fondé sur des signatures de codes et de la cryptographie.

Précédent : Autour de Coq Remonter : Fondements scientifiques Suivant : Commerce électronique sécurisé