Rapport de stage du dea d’Informatique de Lyon

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