Rapport de stage du dea d’Informatique de Lyon








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

4.Discussion et travaux futurs

4.1Le modèle


Notre modèle n’inclut pas toutes les possibilités de Java Card. Pour le rendre plus réaliste, il faudrait que les applets puissent utiliser des tableaux de bytes, les nombres hexadécimaux beaucoup employés pour la programmation des cartes et plus tard les APIs (Application Programming Interface) de Java Card 2.0.

Il faudrait aussi que modèle gère l’authentification grâce au PIN (Personal Identifier Number) en début de communication entre le lecteur et la carte pour s’assurer de l’identité de la personne employant la carte.

Les retraits de carte ou coupures de courant devront également être simulés avec sauvegarde du contexte. Ces deux événements asynchrones auront comme conséquence de cesser toute activité sur la carte. Lors de la remise du courant, toutes les opérations atomiques interrompues seront annulées.

Le JCRE devrait stocker, pour chaque applet contenue sur la carte, l’état en plus de l’AID et de la référence. Les différents états possibles sont : none, loaded, registred, selectable.

4.2La sémantique

4.2.1Spécifications communes Java/ Java Card


Actuellement la sémantique de Java n’est pas encore totalement spécifiée. Le mécanisme d’exception est en cours de spécification par Marjorie Russo. Il faudra juste l’adapter à Java Card (i.e. enlever les exceptions n’appartenant pas à Java Card et rajouter celles propres à Java Card).

De plus, les nombres hexadécimaux ainsi que certaines opérations binaires comme le décalage droit (>>), gauche (<<), droit non signé (>>>), le modulo (%), le xor bit à bit (^), le et bit à bit (&) ou le ou bit à bit (|) n’ont pas été spécifiées. La plupart de ces opérations sont nécessaires pour travailler avec des nombres en hexadécimal (ex. pour faire des masques) utilisés intensément par les développeurs d’applications en assembleur pour les cartes.

Il faudra aussi faire migrer la sémantique Java de JDK 1.0 vers JDK 1.1 pour pouvoir traiter les inner classes et interfaces.

De plus, il faudra aussi être capable de spécifier le mécanisme de package qui permet à une application d’être modulaire multi-fichiers.

4.2.2Spécifications Java Card


La première chose à faire serait de spécifier les comportements du JCRE, CAD et de la classe Applet en Typol. Cela permettrait de réduire la taille de notre programme à quelques lignes seulement et donc d’améliorer les performances de l’interprétation. Ainsi la gestion des threads serait complètement cachée.

Il faudrait pouvoir spécifier toutes les classes et les méthodes de Java Card. Cette solution paraît acceptable au vue du faible nombre de classes en Java Card (51 classes dont 18 classes d’exception pour 5 packages).

Dans un sens Java Card peut être vu comme un sous-ensemble de Java, mais pourtant il possède des mécanismes qui lui sont propres et qui sont liés aux spécificités des cartes à puce.

Par exemple, notre sémantique devra tenir compte des objets transients. Pour cela, il faudra définir une nouvelle structure : une liste d’objets transients contenant également le moment où la remise aux valeurs par défaut doit être faite. Cette liste sera consultée et mise à jour après chaque transaction, desélection, simulation de coupure de courant ou de retrait de carte.

Notre sémantique doit pouvoir intégrer le mécanisme de transactions atomiques. La solution serait de faire lors de la rencontre de l’appel système beginTransaction() (méthode indiquant le début d’une transaction atomique) une copie de la liste des objets persistents. Ainsi on pourrait restaurer les valeurs modifiées en cas de simulation de retrait de carte ou de coupure de courant dans une transaction atomique ou en cas d’appel de la méthode abortTransaction() (pour annuler la transaction).

La sémantique devrait enfin définir le partage d’objets entre applets (caractéristique absente des outils commerciaux).

4.3Les Performances


L’interprétation de notre programme (environ 500 lignes) grâce à la sémantique modifiée de Java montre que des programmes assez gros peuvent être traités sur station de travail. Pour donner un ordre d’idée de la vitesse de notre interprète nous pouvons dire que l’interprétation se fait en 7 mn sous un DEC PWS 500 à 500 MegaHertz, avec 256 Mø de mémoire vive et 600 Mø de swap sur disque dur. Ces performances sont acceptables en présence de l’animation de l’exécution. En effet le développeur doit pouvoir suivre le déroulement de l’exécution.

4.4L’Interface


Actuellement le comportement du l’utilisateur est décrit dans le programme et est donc figé. En offrant une fenêtre d’entrée au CAD, nous permettrons à l’utilisateur de choisir l’applet et l’opération à exécuter. De cette manière, l’utilisateur ne sera plus simulé. Cette fenêtre aura l’apparence d’un vrai lecteur de carte avec des boutons et un écran LCD. Le problème sera bien sûr d’avoir un CAD générique i.e. indépendant des applications de la carte. Pour cela, il faudra une phase d’initialisation entre le CAD et la carte pour donner les AIDs et les opérations possibles des applets contenues par la carte. Actuellement les fabricants de carte et de terminaux sont en train de réfléchir à ce problème. En effet, jusqu'à présent comme nos cartes étaient mono-applications, les CADs connaissaient les opérations qui pouvaient être réalisées sur cette application. Mais maintenant avec l’arrivée des cartes multi-applications, les CADs devront devenir « intelligents ».

D’autres fenêtres d’interfaces pourraient être créées pour visualiser le fonctionnement du JCRE et objets de type File (très couramment utilisés dans la programmation des cartes à puces).

5.Conclusion


Nous avons présenté nos travaux sur le langage Java Card: nous avons tout d'abord étudié le langage, les standards liés aux cartes à puces, puis modélisé les applications Java Card en y incluant tous les acteurs, et pas seulement ce qui se passait effectivement sur la carte.

Nous avons modifié une sémantique formelle de Java existante afin de prendre en compte ce modèle, en particulier le fait qu'un seul thread est actif à un instant donné. Enfin, cette modélisation ainsi que la sémantique ainsi décrite permettent de comprendre le comportement des applications Java Card. L'environnement de développement construit pour Java Card facilite la mise au point des applets Java Card grâce à la visualisation des acteurs du modèle et des transactions entre terminal et carte.

Notre objectif est, dans un premier temps, de compléter la description formelle du langage (et du modèle), puis de proposer d'autres outils pour permettre la mise au point. Enfin, nous souhaitons étudier et formaliser des propriétés liées à la sécurité qui, une fois vérifiées, pourront garantir le bon fonctionnement d'une application Java Card.

A terme, nous pourrons ainsi disposer d'un environnement complet de développement et vérification d'applications Java Card.

Références

[ATT97]

Isabelle Attali, Denis Caromel, Marjorie Russo

Vers une sémantique Formelle de Java

Journées du GDR Programmation 12, 13, 14 novembre 1997 Rennes

file:://babar.inria.fr:/pub/croap/attali/GDR_97.ps

[BOR98a]

E. Börger and W. Schulte

A programmer friendly modular definition of the semantics of Java

Formal syntax et semantics of Java. LNCS. Springer-Verlag, 1998. A paraître

[BOR98b]

E. Börger and W. Schulte

Defining the Java Virtual Machine as platform for Provably correct Java compilation

23rd International Symp. On Mathematical foundations of computer sciences

LNCS. Springer-Verlag, 1998. A paraître

[BUL98]

Bull CP8

Odyssey I : Your passport to the Java world

http://www.bull.gr/bull/www.cp8.bull.net/news/021798a.htm

http://www.bull.gr/bull/www.cp8.bull.net/products/javacara.htm

[CHE98]

Zhiqun Chen (with special contribution by Rinaldo Di Giorgio)

Understanding Java Card 2.0 (learn the inner workings of the Java Card architecture, API, and runtime environment) JavaWorld March 1998

http://www.javaworld.com/javaworld/jw-03-1998/jw-03-javadev.html

[DRE98]

Henry Dreifus, J. Thomas Monk

Smart Cards (Chapitres 1, 2, 3, 10)

John Wiley & Sons 1998 ISBN 0-471-15748-1

[DRO98]

S. Drossopoulou, S. Eisenbach

Towards an operationnal semantics and proof of type soundness for Java

Formals Syntax and Semantics of Java, LNCS. Springer-Verlag, 1998 A paraître

[GEM98]

Gemplus

Gemplus ships GemXpresso RAD, a Java-Based Development Plateform for smart cards Gemplus presse 23/03/98

http://www.gemplus.com/presse/1998/gemxpresso.htm

[GOS96]

James Gosling, Bill Joy and Guy Steele

The Java Language Specification (Chapitre 19 LALR Grammar) Addison-Wesley 1996 http://java.sun.com/docs/books/jls/htlm/19.doc.html#52996

[GUT97]

Scott B. Guthery (Schumberger Electronic Transactions)

Java Card : Internet Computing on a Smart Card IEEE Internet Computing Volume 1 Jan. Feb. 1997

[NIP98]

T. Nipkow and D. Von Oheimb

Java Light is Type Safe- Definitely

25th ACM Symp. Principles of Programming Languages, 1998

[QIA98]

Z Qian

A formal specification of the Java Virtual Machine Instructions for objets, methods and subroutines

Formal syntax et semantics of Java. LNCS. Springer-Verlag, 1998. A paraître

[ROS97]

Eva Rose

Towards a Secure Bytecode Verification on a Java Card

Workshop on security and languages, Palo Alto. Oct 97

[SYM97]

D. Syme

Proving Java type soundness

Technical report 427, University of Cambridge Computer laboratory. 1997

[RUS97]

Marjorie Russo

Une sémantique formelle de Java

Mémoire de DEA de Mathématiques Discrètes de Fondements de l’Informatique de Marseille Juin 1997

file:://babar.inria.fr:/pub/croap/mrusso/Sout_Dea.ps.gz

[POS98]

Joachim Posegga, Harald Vogt

Byte Code Verification for Java Smart Cards Based on Model Checking

5th European Symposium on Research in Computer Security (ESORICS) 1998

Springer LNCS 1998

[SLG97]

Schlumberger

Presenting … the butterfly effect ? 1997-1998

http://www.cyberflex.austin.et.slb.com/cyberflex

Simulation Tool Aids Development of Cyberflex Cardlets ™ for smart card

http://www.cyberflex.austin.et.slb.com/cyberflex/top/news/032398-m8ksim.html

[SUN1]

Sun Microsystems

Java Card 2.0 Language Subset and Virtual Machine Specification Révision finale 1.0 du 13 octobre 1997 http://java.sun.com/products/javacard

[SUN2]

Sun Microsystems

Java Card 2.0 Programming Concepts Révision finale 1.0 du 15 octobre 1997

http://javaworld.com/javaworld/jw-04-1998/iButtons/JC20-Concepts.pdf

[SUN3]

Sun Microsystems

Java Card Checker User’s Guide Révision finale 1.5 du 20 Février 1998

[SUN4]

Sun Microsystems

Java Card Application Programming Interface (package javacard.framework) Révision finale 1.0 du 13 Octobre 1997

http://javaworld.com/javaworld/jw-04-1998/iButtons/JC20API-prtrat.pdf





/


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