Rapport de stage du dea d’Informatique de Lyon








télécharger 152.95 Kb.
titreRapport de stage du dea d’Informatique de Lyon
page1/7
date de publication31.01.2018
taille152.95 Kb.
typeRapport
ar.21-bal.com > droit > Rapport
  1   2   3   4   5   6   7
Simulation d’Applications

Java Card
Carine Courbis

Rapport de stage du DEA d’Informatique de Lyon

INRIA de Sophia-Antipolis

Projet CROAP (Conception et Réalisation d’Outils d’Aide à la Programmation)

2004, route des Lucioles, BP 93

06 902 Sophia-Antipolis Cedex

Carine.Courbis@sophia.inria.fr

Juillet 1998

Stage financé par Dyade (G.I.E. Bull/INRIA)
Responsables : Dr. Isabelle Attali & Pr. Denis Caromel

Résumé

Le développement de nouveaux composants plus puissants va permettre l’installation de plusieurs applications sur une même carte à puce. Elles pourront contenir des données aussi disparates que de la monnaie électronique, des crédits téléphoniques ou des informations médicales utiles en cas d’accident. L’apparition d’un nouveau langage de haut niveau adapté aux standards 7816 de la carte à puce, Java Card (sous-ensemble de Java), offre de nouvelles possibilités en matière de portabilité et de sécurité. Nous étudions la sémantique du langage Java Card afin de construire un environnement de développement et de vérification de programmes Java Card.

Mots-clés : Java Card, applets, carte à puce intelligente, sémantique, environnement graphique

Sommaire

1. Introduction 3

2. Etat de l’art 5

2.1 Les Sémantiques Formelles de Java 5

2.1.1 Travaux Formels sur Java 5

2.1.2 Travaux Formels sur le Byte Code 6

2.1.3 Une sémantique naturelle pour Java 6

2.2 Le checker Java Card 9

2.3 Les outils commerciaux adaptés à Java Card 10

2.3.1 Odyssey-Lab de Bull [BUL98] 10

2.3.2 GemXpresso Rapid Applet Development (RAD) de Gemplus 10

2.3.3 Cyberflex 2.0 Multi8K de Schlumberger [SLB97] 10

3. Construction d’un environnement Java Card 11

3.1 Définition syntaxique de Java Card 11

3.2 Un exemple de vérification statique 12

3.3 Le simulateur d’applets Java Card 15

3.3.1 Le modèle 15

3.3.2 Modifications de la sémantique 20

3.3.3 Résultats obtenus lors de cette simulation 22

4. Discussion et travaux futurs 23

4.1 Le modèle 23

4.2 La sémantique 24

4.2.1 Spécifications communes Java/ Java Card 24

4.2.2 Spécifications Java Card 24

4.3 Les Performances 25

4.4 L’Interface 25

5. Conclusion 25

Remerciements

Je tiens à remercier Isabelle Attali et Denis Caromel pour m’avoir accueillie pour ce stage. Leurs conseils, encouragements, aide, patience me furent d’une grande utilité durant ces quatre mois.

Je voudrais aussi remercier toutes les personnes du projet CROAP pour m’avoir si rapidement adoptée et pour m’avoir aidée à «vaincre Centaur ».

Je tiens à remercier plus particulièrement :

  • Yves Bertot, responsable du projet CROAP, et Laurence Rideau pour leur l’intérêt qu’ils ont porté à mon travail et pour leur aide.

  • Marjorie Russo pour son inestimable aide, sa patience, ses encouragements. Elle fut toujours disponible pour répondre à mes trop nombreuses questions sur sa sémantique et sur Typol.

  • Valérie Pascual, ma personnelle « hot-line Centaur ». Que de fois je l’ai dérangée ! Elle fut d’une grande aide lors de la spécification de la syntaxe avec Metal et du pretty printer en Ppml. De plus, elle est capable de donner une explication à tous les messages d’erreur de Centaur (même lors de la rencontre du quatrième type avec des heaps OVNI et des PPML UFO).

  • Francis Montagnac, le magicien d’Unix. Le monde Unix n’a plus de secret pour lui. C’est aussi un champion pour trouver les bugs dans le protocole de communication entre Typol et Centaur.


Je tiens à remercier aussi Claire Loiseaux et Dominique Bolignano de Dyade (GIE Bull/INRIA) pour avoir répondu si gentiment à mes questions sur Java Card.

  1   2   3   4   5   6   7

similaire:

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage 2ème année dut informatique
«Les travaux dont IL est question dans le présent document ont été exécutés durant un stage de formation effectué au Centre international...

Rapport de stage du dea d’Informatique de Lyon iconRésumé Ce rapport concerne mon stage de fin d’étude de Master 2 Informatique...

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage
«Etudes Référentiels Internet» (eri) pour avoir eu la gentillesse de m’accepter en stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage

Rapport de stage du dea d’Informatique de Lyon iconRapport de stage








Tous droits réservés. Copyright © 2016
contacts
ar.21-bal.com