=============================================================================== | | | Etude de cas DEMONEY | | | | Lundi 17 mai 2004 | =============================================================================== 1) Description des fichiers =========================== Archive Concernée : ------------------- EtudeCasDEMONEY.arc Contenu de l'archive : ---------------------- Dossier src : APDU.mch Constantes.mch DEMONEY.mch DEMONEY_GestionSolde.mch DEMONEY_GestionSolde_R1.ref DEMONEY_R1.ref JCRE.mch JCRE_R1.ref OrdonanceurDuTerminal.mch OrdonanceurDuTerminal_R1.ref ProcessAPDU.mch ProcessAPDU_R1.ref Terminal.mch Terminal_R1.ref Dossier lang : vide Dossier bdp : Les preuves des machines 2) Description de l'étude de cas ================================ 2.1) Description globale ------------------------ Dans le projet GECCOO, nous nous sommes intéressés à réaliser un modèle de l'applet DEMONEY à partir de sa spécification publique, afin de visualiser les différentes contraintes d'expression et de vérification des propriétés de sécurité. Lors de la réalisation de ce modèle, nous nous sommes concentrés sur la précision des messages d'erreur et l'expression des différents états des transactions et des canaux de communication. De plus, certaines parties de la spécification ne sont pas implantées car l'intéret était faible par rapport aux objectifs visés. C'est le cas notamment de la partie cryptographie qui est actuellement spécifiée de manière non déterministe. 2.2) Description succinte de chacun des composants -------------------------------------------------- Constantes : Ensemble des constantes et des ensembles utilisés. APDU : Structure de données permettant de stocker les paramètres et les résultats des appels. Terminal : Ensemble des opérations qui peuvent être effectuées par le terminal. OrdonanceurDuTerminal : Système événementiel appelant les fonctions du terminal et permettant de modéliser l'ensemble des comportements possibles du terminal. JCRE : Modèlise le comportement du Java Card Runtime Environment qui laisse passer les appels à DEMONEY, si celui et selectionné, et interprète l'APDU SELECT. DEMONEY : Interface d'avec le JCRE. Mise en place des méthodes Select, Deselect et Process. Le rôle de cette dernière est d'appeler la méthode du ProcessAPDU qui correspond à l'APDU reçu. ProcessAPDU : Interface APDU de DEMONEY. Ensemble d'opérations permettant de traiter les différents APDU reçus. Les fonctions sont appelées par la méthode Process du composant DEMONEY. (Limitation du nombre d'essais du code PIN ; Vérification de l'atomicité des opérations de transaction et d'ouverture de canal.) DEMONEY_GestionSolde : Délocalisation de la partie de gestion et contrôle du solde courant de la carte. (Vérification de la faisabilité d'une transaction avant de l'effectuer.) 3) Récupération et installation de ce projet sous AtelierB version 3.6 ====================================================================== Avant de débuter, vous dévez vérifier que vous avez déjà récupérer l'archive EtudeCasDEMONEY.arc. Si cela est bien le cas alors passez directement au point 3.2. 3.1) Récupération ----------------- L'archive EtudeCasDEMONEY.arc.gz peut être récupérée directement à l'adresse : http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/GECCOO/DEMONEY/EtudeCasDEMONEY.arc.gz Sinon, la page y faisant référence est ici : http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/ Dans tous les cas, il faut d'abord décompresser cette archive avant de pouvoir passer au point 3.2. Pour cela il suffit de taper gzip -d EtudeCasDEMONEY.arc.gz sur la ligne de commande UNIX. 3.2) Installation ----------------- -> Lancez l'atelier 3.6 -> Cliquez sur le bouton "restore" -> Avec les champs "Directories list" et "Archives list" sélectionnez l'archive -> Entrez l'adresse du dossier de destination dans "Project Directory" (vous pouvez vous aider de "Project directory list") -> Entrez un nom pour ce projet dans le champs "Project Name" -> Selectionnez le type de restauration "B Source Files And Proof Files" -> Validez avec le bouton OK. -> Une fenêtre apparait et vous demande confirmation : validez avec le bouton OK. Le projet est maintenant installé avec tous ses fichiers de preuves et ses librairies. 3.3) Vérification ----------------- Si vous voulez voir le magnifique tableau suivant : +--------------------------+----+-----+------+-----+-----+-----+-----+-----+-----+-----+ | COMPONENT | TC | POG | Obv | nPO | nUn | %Pr | B0C | C | Ada | C++ | +--------------------------+----+-----+------+-----+-----+-----+-----+-----+-----+-----+ | APDU | OK | OK | 14 | 4 | 0 | 100 | - | | | | | Constantes | OK | OK | 1 | 0 | 0 | 100 | - | | | | | DEMONEY | OK | OK | 164 | 27 | 0 | 100 | - | | | | | DEMONEY_GestionSolde | OK | OK | 56 | 15 | 0 | 100 | - | | | | | DEMONEY_GestionSolde_R1 | OK | OK | 165 | 39 | 0 | 100 | - | | | | | DEMONEY_R1 | OK | OK | 1655 | 179 | 0 | 100 | - | | | | | JCRE | OK | OK | 14 | 0 | 0 | 100 | - | | | | | JCRE_R1 | OK | OK | 184 | 22 | 0 | 100 | - | | | | | OrdonanceurDuTerminal | OK | OK | 11 | 0 | 0 | 100 | OK | | | | | OrdonanceurDuTerminal_R1 | OK | OK | 35 | 0 | 0 | 100 | - | | | | | ProcessAPDU | OK | OK | 135 | 12 | 0 | 100 | - | | | | | ProcessAPDU_R1 | OK | OK | 1170 | 100 | 0 | 100 | - | | | | | Terminal | OK | OK | 30 | 0 | 0 | 100 | - | | | | | Terminal_R1 | OK | OK | 182 | 32 | 0 | 100 | - | | | | +--------------------------+----+-----+------+-----+-----+-----+-----+-----+-----+-----+ | TOTAL | OK | OK | 3816 | 430 | 0 | 100 | - | OK | OK | OK | +--------------------------+----+-----+------+-----+-----+-----+-----+-----+-----+-----+ Alors il se peut que vous soyez obliger de relancer le prouveur (avec la méthode replay). 4) Contacts =========== En cas de problème, contacter : M. Nicolas Stouls (Nicolas.Stouls@imag.fr) ou Mme Marie-Laure Potet (Marie-Laure.Potet@imag.fr) ou M. Sylvain Boulme (Sylvain.Boulme@imag.fr) ou M. Didier Bert (Didier.Bert@imag.fr)