Rapport de stage du dea d’Informatique de Lyon








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

2.Etat de l’art


Il existe de nombreux travaux liés à la sémantique et à la sécurité de Java et plus récemment de Java Card. C’est pourquoi cette étude commence par une présentation des sémantiques formelles de Java (dont celle utilisée pour notre travail). De plus, il est nécessaire pour juger de la pertinence de notre travail de connaître les outils existants adaptés à Java Card i.e. le vérificateur statique (appelé checker) fourni par Sun et les outils commerciaux Odyssey-Lab de Bull, GemXpresso RAD de Gemplus et Cyberflex de Schlumberger.

2.1Les Sémantiques Formelles de Java

2.1.1Travaux Formels sur Java


Un important domaine de recherche est la preuve de la sûreté des types en Java. Drossopoulou, Einsenbach [DRO98] et Syme [SYM97] spécifient la sémantique de différents sous-ensembles Java séquentiels (incluants les types primitifs, les classes, l’héritage, les variables et méthodes d’instances, les interfaces, la surcharge des variables d’instance, la création d’objet Java, les tableaux et les exceptions) pour prouver que l’exécution d’un programme préserve les types. En rapport avec leurs travaux, Nipkow et Oheimb [NIP98] définissent et prouvent des propriétés sur leur sous-ensemble Java Light avec le prouveur de théorème Isabelle/HOL.

Börger et Schulte [BOR98a], pour leur part, définissent une sémantique dynamique par empilement de différents sous-ensembles Java.

2.1.2Travaux Formels sur le Byte Code


Une autre approche pour prouver la sûreté des types est de travailler au niveau du byte code de la JVM. Qian [QIA98] a défini une sémantique pour un sous-ensemble d’instructions de la JVM. Les comportements de ces instructions dans la mémoire lors du runtime sont décrites comme des transitions d’états. Son but comme Börger et Schulte [BOR98b] est de prouver le bon fonctionnement du byte code lors de son exécution.

Joachim Posegga et Harald Vogt [POS98] définissent, pour leur part, un système à état fini pour la vérification de byte code pour Java Card. Eva Rose [ROS97] a elle aussi spécifiée un sous ensemble Java, JavaOb, assez restreint pour modéliser Java Card. Puis elle a définit une traduction de JavaOb vers un sous-ensemble de la JVM, JVMOb dont la sémantique statique correspond au vérificateur Java de byte code. Ainsi elle a obtenu une formalisation de son sous-ensemble et peut proposer une procédure de vérification de la sûreté du byte code.

2.1.3Une sémantique naturelle pour Java


Cette sémantique [RUS97], [ATT97] (spécifiée par Marjorie Russo, doctorante du projet CROAP) est celle sur laquelle notre sémantique Java Card est basée (en modifiant le moins possible sa syntaxe et sa sémantique pour les adapter à Java Card).

Pour cette description formelle du langage, une sémantique big-step est adoptée pour l’héritage et les caractéristiques objets alors que le multithreading est spécifié par une sémantique small-step (ou opérationnelle). L’ensemble de cette spécification représente environ 400 règles Typol.

Cette sémantique naturelle spécifie un large sous-ensemble Java et est exécutable dans le système Centaur.
Le système Centaur est un outil de génération d’environnements de langages de programmation développé par le projet CROAP. Il permet de spécifier formellement des langages aussi différents qu’Eiffel, Esterel ou ASN1.

Pour spécifier un langage avec cet outil, il faut tout d’abord définir sa syntaxe concrète et sa syntaxe abstraite à l’aide du langage Metal. Cette première étape permet de générer un analyseur syntaxique (parseur). Son rôle est d’analyser syntaxiquement un programme et de créer son arbre de syntaxe abstraite. La deuxième étape est la spécification de règles d’affichage en Ppml pour générer un pretty-printer. Enfin la dernière étape est la spécification de la sémantique du langage à l’aide de règles Typol. De cette sémantique, on pourra constituer des outils d’aide à la programmation (comme par exemple un interprète ou vérificateur de type). La Figure 2 permet d’avoir une vue simplifiée du système.




Figure 2 Environnement de programmation construit avec Centaur

La Syntaxe

Le langage Metal permet de spécifier la grammaire de langages de programmation. Il se décompose en 2 parties :

  • la syntaxe concrète utilisée pour analyser syntaxiquement un programme.

  • la syntaxe abstraite utilisée pour construire l’arbre abstrait du programme.

Quand un fichier (contenant un programme du langage décrit) est lu sous Centaur, le parseur associé au langage utilisé dans le fichier construit l’arbre de syntaxe abstraite (cf. Figure 3) représentant le programme. Cet arbre sert de base pour faire de l’édition structurée, de la sémantique statique ou dynamique. En cas d’erreur syntaxique, l’arbre n’est pas généré et un message d’erreur apparaît. Le Tableau 1 présente des exemples de spécification de syntaxe concrète et abstraite écrits en Metal.


Exemple de syntaxe concrète en Metal:

::= ;

::="[""]"; array() (1)

 : := %ID ; identifier-atom(%ID) ;
Exemple de syntaxe abstraite en Metal:

VariableDeclaratorId ::= array Identifier ;

Identifier ::= identifier class ;

Identifier -> implemented as IDENTIFIER ;

Array -> Identifier ; (2)

Class -> implemented as SINGLETON ;

Explications

Le non terminal VariableDeclaratorId est utilisé lors de la déclaration d’une variable. Il décrit les variables de type tableau.

Int varT[] ;

Dans ce cas varT est analysé par la règle (1) de VariableDeclaratorId. L’arbre construit aura pour l’opérateur array et pour feuille un identifier i.e. dans ce cas varT En effet, comme cette règle s’applique, la fonction de construction d’arbre array() est appelée. Elle correspond à un opérateur de syntaxe abstraite (2).

Tableau 1 Exemples de spécification de syntaxe écrits en Metal

Il faut spécifier un pretty-printer en langage Ppml pour qu’un arbre de syntaxe abstraite du langage soit visible dans une représentation textuelle (cf. Figure 4).
F
igure 3 Arbre de syntaxe abstraite du célèbre programme HelloWorld.java (présentation arborescente)

F
igure 4 Arbre de syntaxe abstraite du célèbre programme HelloWorld.java (présentation textuelle Java)
La Sémantique

Les sémantiques statiques et dynamiques doivent être spécifiées en Typol, qui est un langage dédié à la sémantique naturelle. C’est un langage déclaratif, logique, typé, manipulant la syntaxe abstraite du langage. Il fournit des mécanismes de filtrage, d’unification et de retour arrière.

Les règles peuvent être regroupées dans des sets

Le Tableau 2 présente un exemple de règle écrite en Typol.
A partir des spécifications décrites en Typol, Centaur permet de générer des outils sémantiques comme un vérificateur de type ou un interprète pour le langage. Le résultat d’un vérificateur de type sur un programme donné est une liste d’erreurs avec une référence de l’emplacement de chaque erreur dans l’arbre de syntaxe abstraite (ainsi l’erreur pourra être mise en exergue dans le programme). Au cours de l’interprétation d’un programme des structures sémantiques (contenant des informations utiles sur le comportement du programme comme par exemple la liste des objets créés par le programme ou bien la liste des variables statiques) sont construites. Donc un résultat possible de l’interprète pourrait être une de ces structures sémantiques (ex : la liste des objets et leurs attributs à la fin de l’interprétation). Ces résultats sont montrés dans des fenêtres spécifiques (textuelles ou graphiques). De plus, Centaur permet d’animer l’exécution d’un programme en utilisant des mises à jour incrémentales des fenêtres contenant les résultats.


Exemple de règle en Typol :

Jugdement Object_L, O_Id |- Object ;
find_Apdu_attribute(identifier "commandApdu" |- ObjL1, AttrL1 -> AttrL2)

--------------------------------------------------------------------------

ObjL1, OthId1 |- object(_, identifier "CAD", AttrL1, _, _, _, _);

Do

Update_apduL(APDU(OthId1, AttrL2) -> ApduL) &

emit_tree("APDU", ApduL) ;

Explications

Cette règle d’inférence ne s’applique que si l’objet a comme nom de classe CAD (mécanisme utilisé : le filtrage) et si la prémisse find_Apdu_attribute n’échoue pas. Cette prémisse recherche la référence de l’objet APDU, contenu par l’objet de type CAD donné, dans la liste d’attributs (AttrL1). Puis elle recherche cet objet dans la liste des objets du programme (ObjL1) pour en extraire la liste d’attributs pour une APDU de commande (AttrL2).

Donc si la règle réussit, une mise à jour de la liste des APDUs est faite (update_apduL), suivie par son affichage dans la fenêtre APDU (cf. Figure 10).

Tableau 2 Exemple d’une règle Typol
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