Rapport de stage du dea d’Informatique de Lyon








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

3.Construction d’un environnement Java Card


Tout d’abord, on indiquera les modifications apportées aux spécifications syntaxiques Java pour les adapter à Java Card. Puis on décrira un outil de vérification statique spécifié pour détecter la présence de tableaux multidimensionnels. Puis enfin notre simulateur d’application Java Card sera présenté.

3.1Définition syntaxique de Java Card


Tout le travail sur la syntaxe de Java Card repose sur le document Java Card 2.0 language subset and virtual machine specification [SUN1] écrit par Sun Microsystems. Notre rôle était de modifier ou de supprimer les types et les opérateurs adéquats de la spécification syntaxique de Java qui contenait 130 types et 209 opérateurs.
Notre première action fut donc d’enlever les types de base non supportés en Java Card (i.e. char, long, double et float).

Puis comme les threads ne sont pas supportés, le modifier synchronized (utilisé pour synchroniser l’accès à une donnée ou à une méthode lors de l’exécution multi-threadée d’un programme) fut enlevé.

Comme aucune gestion de la mémoire (garbage collector) n’est spécifiée en Java Card, les modifiers volatile (permettant d’indiquer que cette variable est une copie d’une donnée partagée par deux threads ayant comme avantage d’être remise à jour à chaque accès) et transient (permettant d’indiquer que la valeur d’un attribut d’un objet n’est pas persistante) ont été enlevés.

Java Card, contrairement à Java, ne possède que des tableaux unidimensionnels. C’est pourquoi des modifications ont dû être faites pour éviter la déclaration et l’usage de tableau à plus d’une dimension. Pour cela, il a fallu restreindre la spécification des types utilisables pour la déclaration d’un attribut, d’une variable locale, du type de retour d’une méthode, ou d’un cast. Malgré ces modifications, il est encore possible de faire une analyse syntaxiquement correcte d’un programme illégal en Java Card (i.e. contenant un tableau à 2 dimensions). En effet, Java lors de la déclaration d’une variable, d’un attribut ou du type de retour d’une méthode, laisse la possibilité au développeur de positionner les crochets indiquant un tableau soit à droite du nom du type, soit à droite du nom de la variable, de l’attribut ou de la méthode (après ses paramètres). C’est pourquoi, ces 3 déclarations int[] i , int i[] et int[] i[] sont syntaxiquement correctes en Java Card mais le dernier exemple n’a aucun sens pour un programme Java Card car le tableau déclaré a 2 dimensions. Ce type de vérification est donc à effectuer pendant la phase d’analyse statique (cf. partie 3.2 pour avoir plus de détails).

Lors de cette analyse fine de la syntaxe de Java et de Java Card, nous avons détecté des erreurs dans la description syntaxique de Java qui était trop permissive par rapport à la grammaire LALR définie par Gosling [GOS96].
Lors de notre spécification sémantique, nous avons eu besoin de définir une structure de résultat qui définit les APDUs transmises entre la carte et le lecteur. Cette structure, qui est une liste d’APDUs, a été rajoutée à la syntaxe abstraite. En voici sa spécification :

APDU_L ::= apdu_l ;

apdu_l -> APDU *… ;

APDU ::= apdu ;

apdu -> O_Id Pair_L ;
Une APDU contient la référence de l’objet (O_Id) l’ayant transmis et une liste de paires (Pair_L). Chaque paire contient le nom de l’attribut et sa valeur (comme par exemple (« cla », 0)). Les types O_Id et Pair_L étaient déjà définis dans la syntaxe abstraite de Java.

3.2Un exemple de vérification statique


Pour débuter avec le langage Typol, nous avons décidé de spécifier un outil de sémantique statique testant que les tableaux n’ont qu’une dimension (cf. partie 3.1 pour une description de la problématique). Cette spécification permettait de se familiariser au parcours de l’arbre de syntaxe abstraite d’un programme Java Card et à la syntaxe des règles Typol.

Le but était donc d’analyser un programme et de vérifier sa légalité en Javacard. En cas d’erreur, un message est affiché (cf. Figure 6).
Les emplacements possibles d’erreur

  • Déclaration des champs (i.e. variables contenues dans une classe/interface)

  • Déclaration d'une variable locale (i.e. dans un bloc (méthode, if...)) byte[] var1[]

  • Déclaration des paramètres d'une méthode/constructeur void foo(byte[] var1[]) {...}

  • Déclaration du type de retour d'une méthode byte[] foo()[] {...}



Nous avons ainsi pu identifier les nœuds de l’arbre abstrait à analyser i.e. fieldVariableDeclaration, methodDeclaration, localVariableDeclaration.
Algorithme utilisé

Début : nœud typeDeclarations de compilationUnit

Pour chaque nœud fieldVariableDeclaration

si son fils type est arrayof(TypeName)

Pour chaque variableDeclarator

si c'est un array ou un initializedVariable avec un

VariableDeclaratorId qui est un array

msg d'erreur

Pour chaque nœud methodDeclaration

Si ResultType est un array(TypeName) et

si MethodDeclarator est un arrayMethodDeclarator

msg d'erreur

Pour chaque parameter

Si Type = arrayof(TypeName) et VariableDeclaratorId = array

msg d'erreur

Pour chaque nœud constructorDeclaration

Pour chaque parameter

Si Type = arrayof(TypeName) et VariableDeclaratorId = array

msg d'erreur

Pour chaque nœud localVariableDeclaration

Si Type = arrayOf(TypeName)

Pour chaque variableDeclarator

si c'est un array ou un initializedVariable avec un

VariableDeclaratorId qui est un array

msg d'erreur
Ci-dessous (cf. Tableau 3) sont écrites les règles Typol nécessaires pour tester que les paramètres d’un constructeur sont corrects (i.e. ne sont pas des tableaux à plusieurs dimensions).



program javacardCheckCompilationUnit is

use javacard ;

import message(string, string, string, string, path, string) from message ;

import diff(_,_) from prolog ; …
set javacardCheckCompilationUnit is

judgement (CompilationUnit -> Bool);

checkTypeDeclaration_l(TypeDec -> Bool)

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

(compilationUnit(_, _, TypeDec) -> Bool) ; // on ne teste que le nœud typeDeclarations

end javacardCheckCompilationUnit;
set checkTypeDeclaration_l is

judgement (TypeDeclarations -> Bool);

MainRule: // on teste recursivement tous les types déclarations

CheckTypeDeclaration(TypeDec -> Bool1) &

CheckTypeDeclaration_l(TypeDecL -> Bool2) & and(|- Bool1, Bool2 -> Bool3)

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

(typeDeclarations[TypeDec.TypeDecL] -> Bool3) ;
(typeDeclarations[] -> true()) ;

end checkTypeDeclaration_l;
set checkTypeDeclaration is

judgement (TypeDeclaration -> Bool);

ClassRule: // si le typeDeclaration est une classDeclaration, on teste sa liste de FieldDeclaration

CheckClassField_l(FieldDecL -> Bool)

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

(classDeclaration(_, _, _, _, FieldDecL) -> Bool) ;

InterfaceRule: // si le typeDeclaration est une interfaceDeclaration,

//on teste sa liste de InterfaceFieldDeclaration

CheckInterfaceFieldDec_l(InterFieldDecL -> Bool)

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

(interfaceDeclaration(_, _, _, InterFieldDecL) -> Bool) ;

end checkTypeDeclaration;
set checkClassField_l is

judgement (FieldDeclarations -> Bool);

MainRule: // on teste recursivement tous les FieldDeclaration

CheckClassField(FieldDec -> Bool1) &

CheckClassField_l(FieldDecL -> Bool2) & and(|- Bool1, Bool2 -> Bool3)

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

(fieldDeclarations[FieldDec.FieldDecL] -> Bool3) ;
(fieldDeclarations[] -> true()) ;

end checkClassField_l;
set checkClassField is

judgement (javacard -> Bool);

ConstructorRule: //si le fieldDeclaration est un constructorDeclaration

//on teste sa liste de paramètres et son corps.

checkParam_l(ParamL -> Bool1) & checkConstBody(ConstBody -> Bool2) &

and(|- Bool1, Bool2 -> Bool3)

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

(constructorDeclaration(_, constructor(_, ParamL), _, ConstBody) -> Bool3) ;



end checkClassField;
set checkParam_l is

judgement (javacard -> Bool);

ItParamRule: // on teste recursivement chaque paramètre

checkParam(|- Param -> Bool1) & checkParam_l(|- ParamL -> Bool2) &

and(|- Bool1, Bool2 -> Bool3)

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

(parameters[Param.ParamL] -> Bool3) ;
ItParamEmptyRule: (parameters[] -> true()) ;

end checkParam_l;
set checkParam is

judgement |- javacard -> Bool;

ArrayArrayParamRule: //erreur car le type du paramètre est un tableau à 2 dimensions

|- parameter(_, arrayof(TName), array(Param)) -> false() ;

do

message("javacard", "checker", "errorDimArray", "Error", subject, "");

ArrayParamRule: //Le type du paramètre est un tableau à 1 dimension

|- parameter(_, arrayof(TName), Param) -> false() ;

provided diff(Param, array(_));

SimpleParamRule: //parametre

|- parameter(_, TypParam, _) -> true() ;

provided diff(TypParam, arrayof(_));

end checkParam; …

Tableau 3 Spécifications de l’outil de vérification






Sélection courante

Vérification de l’absence de tableaux multi-dimensionnels




Figure 6 Fenêtre contenant les erreurs du programme testé
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