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 :
