Les cartes à puce sont en passe de prendre une place prépondérante dans notre vie quotidienne. Leur programmation, jusqu'ici réalisée en assembleur est désormais possible dans un langage évolué comme Java grâce à l'utilisation du noyau Java Card.
Notre équipe a déjà une expérience en termes de description sémantique et d'environnement de développement avec des travaux sur les langages Java [1] (http://www.inria/fr/croap/java) et JavaCard [2] (http://www.inria.fr/croap/javacard).
Il s'agit d'étudier d'une part des critères qui garantissent certaines propriétés de sécurité, et d'autre part les outils qui pourraient permettre de formaliser ces propriétés [3]. Puis il faudra choisir un outil particulier et formaliser ces propriétés en utilisant cet outil.
Cette formalisation devra s'intégrer aux travaux en cours sur la sémantique de JavaCard.
Ce sujet rentre dans le cadre d'une collaboration entre l'Inria Sophia Antipolis, l'I3S et l'institut Eurecom, et d'une collaboration avec d'autres projets INRIA (action coopérative JavaCard). Les travaux pourront être poursuivis en Thèse de Doctorat.
Encadrement : ATTALI, Isabelle
Téléphone : 04 92 38 79 10 Email : ia@sophia.inria.fr
Laboratoire ou équipe : INRIA Sophia Antipolis
Encadrement : MOLVA, Refik
Téléphone : 04 93 00 26 12 Email : molva@eurecom.fr
Laboratoire ou équipe : Institut Eurecom
Objectifs : Les objectifs du stage sont:
Prérequis : langages à objets, méthodes formelles
Matériel et logiciels utilisés : Stations de travail
INRIA ou Eurecom, Sophia Antipolis