VØri cat ion formelle de laplate-forme Java Card• ThŁse de doctorat •Guillaume DufayINRIA Sophia AntipolisCartes à puce intelligentesJava Card : Environnement de programmation dØdiØ.DerniŁres gØnØrations de cartes à puce pourvues d’unmicroprocesseur et d’un systŁme d’exploitation.Stockent et gŁrent de l’informationCommuniquentContiennent plusieurs applicationsPartagent de l’informationInformation manipulØe sensible ou con dentielle .vendredi 5 dØcembre – p.1/32Architecture Java CardJava source Class file Cap filepackage fr.inri 011100011011100011101011010Class File Converter101011010import javacar 011111001Java compiler011111001Cap File Builder110110111110110111public class no 100100110100100110 public Object Vérification Chargement de bytecodeLiaison Applet Applet Applet011100011 011100011 011100011101011010 101011010 101011010011111001 011111001 011111001110110111 110110111 110110111100100110 100100110 100100110Extensions spécifiques pour l’Industrie APIsMachine Virtuelle (JCVM) Environnement d’Exécution (JCRE)vendredi 5 dØcembre – p.2/32ProblØmatiqueAssurer la sØcuritØ de la plate-forme.Formaliser la plate-forme pour raisonner sur celle-ciMØthodologie pour vØri er des propriØtØs statiquesde la plate-formeAutomatisation pour faciliter l’application de lamØthodologievendredi 5 dØcembre – p.3/32MØthodes formellesExigØes pour garantir la sØcuritØ de systŁmes complexes.Langage de spØci c ation suf ...