transpa-these-gdufay
56 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
56 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

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 ...

Informations

Publié par
Nombre de lectures 51
Langue Français

Extrait

Vérification formelle de plate-formeJava Card
Thèse de doctorat
GuillaumeDufay
INRIA Sophia Antipolis
la
Cartes à puce intelligentes
Java Card de programmation dédié.: Environnement
Dernières générations de cartes à puce pourvues d’un microprocesseuret d’unsystème d’exploitation.
Stockent et gèrent de l’information
Communiquent
Contiennent plusieurs applications
Partagent de l’information
Information manipuléesensibleouconfidentielle.
vendredi 5 décembre – p.1/32
Architecture Java Card Java sourceClass file
package fr.inri import javacarJava compiler public class no  public Object
 Applet 011100011 101011010 011111001 110110111 100100110
011011100101001110Class File Converter 011111001Cap File Builder 110110111 100100110 Chargement Liaison
 Applet 011100011 101011010 011111001 110110111 100100110
Extensions spécifiques pour l'Industrie
 APIs
Machine Virtuelle (JCVM)
 Environnement d'Exécution (JCRE)
 Applet 011100011 101011010 011111001 110110111 100100110
Cap file
011100011 101011010 011111001 110110111 100100110
Vérification de bytecode
vendredi5décembre.p2/32
Problématique
Assurer la sécurité de la plate- forme.
Formaliser la plate- forme pour raisonner sur celle-ci
Méthodologie pour vérifier des propriétés statiques de la plate- forme
Automatisation pour faciliter l’application de la méthodologie
vendredi 5 décembre – p.3/32
Méthodes formelles
Exigées pour garantir la sécurité de systèmes complexes.
Langage de spécification suffisamment expressif
Système logique et techniques de démonstration
Génération de code exécutable et certifié
Utilisation de l’outil C
OQ
.
vendredi 5 décembre – p.4/32
Méthodologie
Vérification d’une propriété statiqueP.
MachinePevsienff-o
proche de l’implémentation supposePdéjà vérifié
MachinePd-evisnefé
proche des spécifications Pvérifié à l’exécution
MachineP-abstraite
vérifiePuniquement
Ovendredi 5 décembre – p.5/32
Méthodologie
Vérification d’une propriété statiqueP.
MachineP-oevisneff
MachinePd-féveensi
Abstractions
MachineP-abstraite
P-BCV
Analyse statique
Ovendredi 5 décembre – p.5/32
Méthodologie
Application à la sûreté du typage.
MachineT ypesneffo-eiv
MachineT ypeensive-déf
manipule :valeurs typées types :vérifiés à l’exécution
manipule :valeurs non typées correction typage assuré parBCV
MachineT ype-abstraite
manipule :types comme valeurs
vendredi 5 décembre – p.5/32
Plan
de la JCVM
Introduction Formalisation Programmes Mémoire Instructions Abstractions Vérification de bytecode
Conclusion
vendredi 5 décembre – p.6/32
Réalisations
Formalisation en COQde la JCVM et du JCRE.
Intégralité des instructions (sémantique opérationnelle à petit pas)
Environnement d’exécution (sauf méthodes natives)
Spécifications fonctionnelles et exécutables
Comparable aux machines virtuelles de référence.
vendredi 5 décembre – p.7/32
Programmes
Représentation des programmes après la phase de liaison (réalisée par le JCVM Tools).
Recordjcprogram : Set := { classes : (list Class); methods : (list Method); interfaces : (list Interface); sheap type : (list type) _
}.
Ovendredi 5 décembre – p.8/32
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents