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é
|
