DEMONEY : Modélisation en B et vérification de propriétés

Nicolas Stouls

(nicolas.stouls@imag.fr)

Laboratoire LSR de Grenoble / IMAG

Travaux financés par une bourse CNRS / STMicroelectronics

Le 6 mai 2004

Objectifs

Expression et vérification de propriétés de sécurité

Choix méthodologiques :

Construction par raffinement

Utiliser au maximum la preuve

Invariants, préconditions, etc.

Compléter par vérification d'un automate des comportements autorisés

Génération automatique d'un graphe comportemental

Outil GénéSyst

Comparaison automatique d'un graphe comportemental avec une propriété

Extension à venir de GénéSyst

Plan

I. Rappels généraux sur DEMONEY

II. Exemple de propriétés et objectifs de sécurité

III. Présentation du modèle

IV. Vérification de propriétés et politiques de sécurité

V. Conclusion

I. Rappels généraux sur DEMONEY

DEMONEY

Applet JavaCard d'un porte monnaie électronique

Développée par : Trusted Logic

Cadre : projet SecSafe

Objectif : faire une étude de cas représentative des Applets JavaCard

Différentes implantations avec différentes API mais le même comportement

Ici,on ne traite que du cas DEMONEY StandAlone

I. Présentation générale de DEMONEY

Concepts de base d'une architecture carte à puce

La carte possède :

CPU, RAM, ROM, OS (Java Card) et programmes (Applets)

Une communication est menée par le terminal

La carte ne fait que répondre

Communication = échange de paquets APDU

APDU = Tableau de bytes contenant une commande et des données

Carte (RAM+

ROM+CPU+OS+

Applets)

CPU

Terminal

Echange de paquets

APDU

Terminal

I. Présentation générale de DEMONEY

Cycle de vie d'une applet

CAP File

(Applet)

Class File

(Applet)

Java File

(Applet)

JCRE

+ Applet

+ Instance

initialisée

JCRE

+ Applet

JCRE

Compilation

en ByteCode

Vérifications statiques

et simplifications

Loading

Téléchargement de

l'Applet sur la carte

INSTALLATION

Instanciation de

l'Applet

Appel d'une

instruction

JCRE

+ Applet

+ Instance

I. Présentation générale de DEMONEY

Possibilité d'utilisation

partielle de la carte pour

sa configuration

(PROCESSING limité)

PERSONALIZATION

Initialisation de certains paramètres de l'instance

PROCESSING

Vie de la carte

2 interfaces différentes

Interface avec le système d'exploitation

Méthodes

Interface avec le terminal

APDU reçus par la méthode process

I. Présentation générale de DEMONEY

Quelques méthodes externes

Select :

Informe l'Applet qu'elle est sélectionnée

process :

Transmet une commande APDU

deselect :

Informe l'Applet qu'elle n'est plus sélectionnée

II. Spécification de DEMONEY

Quelques commandes APDU
passées à l'Applet par la commande process

Seul CodeOp imposé par JavaCard

II. Spécification de DEMONEY

Différents niveaux de sécurité
imbriqués

Publique

Accès aux données publiques (GETDATA)

Sécurisation du canal (INITIALIZEUPDATE, EXTERNALUPDATE, VERIFYPIN)

Débit (terminal de débit et canal chiffré)

Débit de la carte (INITIALIZETRANSACTION[Debit], COMPLETE TRANSACTION)

Crédit (terminal de crédit et canal chiffré)

Crédit de la carte avec des espèces (INITIALIZETRANSACTION [Credit par espèces])

Crédit-Identifié (terminal bancaire de crédit et code PIN vérifié)

Crédit de la carte par virement (INITIALIZETRANSACTION[Credit par virement bancaire])

Administration (terminal d'administration et canal chiffré)

Gestion de la carte (STOREDATA)

II. Spécification de DEMONEY

PROCESSING
Utilisation d'une Applet

Select : Renvoie les infos publiques de l'instance de l'Applet

Deselect : Par selection d'une applet.

Note : Reset n'appelle pas la méthode Deselect

Process APDU : exécution d'une commande

Select APDU (choix d'un AID – Applet IDentifier)

II. Spécification de DEMONEY

PROCESS
Envoi d'une commande à une instance de l'Applet

JCRE

Instance

de l'Applet

Terminal

APDU_1

(Commande)

Process(APDU_1)

(Commande)

AID non précisé

Message traité par l'Applet sélectionnée

APDU_2

(Résultat)

APDU_2

(Résultat)

II. Spécification de DEMONEY

SELECT APDU

JCRE

Instance

de l'Applet

Terminal

APDU_1

(SELECT + AID)

Process (APDU_1)

(APDU_2 : Données publiques

du porte monnaie)

APDU_2

(Données publiques du porte monnaie)

Select()

Deselect()

(Si nécessaire)

II. Spécification de DEMONEY

Sécurisation canal

JCRE

Instance

de l'Applet

Terminal

APDU_1

(Initialize update + challenge1 + Niveau de sécurité voulu)

APDU_2

((challenge1 + challenge2)Clef)

APDU_3

(external authenticate + ((challenge2 + challenge1)Clef))

APDU_4

(Successful execution of the command)

II. Spécification de DEMONEY

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

Select

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

Select

GetData

ReadRecord

Erreur

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

InitUpdate

Select

Erreur

Ext.Auth.

GetData

ReadRecord

Erreur

PutData

PutKey

PINChange

PINUnblock

StoreData

Erreur

II. Spécification de DEMONEY

CompleteTrans.

Erreur

InitTransaction

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

InitUpdate

InitUpdate

Select

Erreur

Erreur

Ext.Auth.

Ext.Auth.

GetData

ReadRecord

Erreur

PutData

PutKey

PINChange

PINUnblock

StoreData

Erreur

InitTransaction

CompleteTrans.

Erreur

GetData

ReadRecord

II. Spécification de DEMONEY

CompleteTrans.

Erreur

InitTransaction

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

InitUpdate

InitUpdate

Select

Erreur

Erreur

Ext.Auth.

Ext.Auth.

GetData

ReadRecord

Erreur

PutData

PutKey

PINChange

PINUnblock

StoreData

Erreur

InitTransaction

CompleteTrans.

Erreur

GetData

ReadRecord

VerifyPin

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

Erreur

VerifyPin

Erreur

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

II. Spécification de DEMONEY

CompleteTrans.

Erreur

InitTransaction

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

InitUpdate

InitUpdate

Select

Erreur

Erreur

Ext.Auth.

Ext.Auth.

GetData

ReadRecord

Erreur

PutData

PutKey

PINChange

PINUnblock

StoreData

Erreur

InitTransaction

CompleteTrans.

Erreur

GetData

ReadRecord

VerifyPin

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

Erreur

VerifyPin

Erreur

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

II. Spécification de DEMONEY

CompleteTrans.

Erreur

InitTransaction

EtatCanal=public

EtatTransaction=none

EtatCanal=Admin

EtatTransaction=Ec

EtatCanal=Admin_ec

EtatTransaction=none

EtatCanal=Admin

EtatTransaction=none

EtatCanal={Débit,Credit}_ec

EtatTransaction=none

EtatCanal={Débit,Credit}

EtatTransaction=Ec

EtatCanal={Débit,Credit}

EtatTransaction=none

EtatCanal=CreditIdent

EtatTransaction=none

DonneesChiffrées=True

EtatCanal=CreditIdent

EtatTransaction=Ec

DonneesChiffrées=True

EtatCanal=CreditIdent

EtatTransaction=none

DonneesChiffrées=False

EtatCanal=CreditIdent

EtatTransaction=Ec

DonneesChiffrées=False

Comportements possibles dans la phase de PROCESSING

Publique

Crédit-Ident

Administration

Débit ou crédit

(suivant le terminal)

InitUpdate

InitUpdate

Select

Erreur

Erreur

Ext.Auth.

Ext.Auth.

GetData

ReadRecord

Erreur

PutData

PutKey

PINChange

PINUnblock

StoreData

Erreur

InitTransaction

CompleteTrans.

Erreur

GetData

ReadRecord

VerifyPin

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

Erreur

VerifyPin

Erreur

CompleteTrans.

Erreur

InitTransaction

GetData

ReadRecord

VerifyPin

II. Spécification de DEMONEY

CompleteTrans.

Erreur

InitTransaction

InitTransaction

II. Exemples de propriétés et objectifs de sécurité

Propriété de DEMONEY

Atomicité :

Les opérations de mise à jour du solde ne doivent pas être interrompues

Les opérations de sécurisation du canal ne doivent pas être interrompues

III. Propriétés et objectifs de sécurité

Objectifs et politiques de sécurité
Sans prise en compte de la cryptographie

On ne peut pas créer d'argent :

Crédit : récupérer de l'argent avant de créditer

Solde >= 0

Il est difficile de perdre de l'argent :

Solde mis à jour seulement si débit possible

Crédit : récupérer de l'argent avant de créditer

Seul le titulaire du compte peut créditer la carte par virement :

Code PIN avec nombre d'essais limité

III. Propriétés et objectifs de sécurité

III. Présentation du modèle

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

JCRE

DEMONEY

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

JCRE

DEMONEY

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Interface :

SetAPDU

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

JCRE

DEMONEY

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Interface :

Reset_ProcessAPDU

ResetSecuLevel

INS_APDU_Select

INS_APDU_GetData

INS_APDU_StoreData

INS_APDU_InitializeUpdate

INS_APDU_ExternalAuthentification

INS_APDU_InitializeTransaction

INS_APDU_InitializeTransactionFromBank

INS_APDU_CompleteTransaction

INS_APDU_VerifyPIN

Raffinement de

ProcessAPDU

Refines

ProcessAPDU

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

JCRE

DEMONEY

ProcessAPDU

APDU

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

DEMONEY

GestionSolde

Raffinement

de DEMONEY

GestionSolde

Refines

Interface :

SW <-- PeutCrediterSolde(vv)

SW <-- PeutDebiterSolde(vv)

EffectuerTransaction

ResetTransaction

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

JCRE

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

du JCRE

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Interface :

bb <-- Select

DeSelect

Reset_DEMONEY

Process

DEMONEY

Raffinement

de DEMONEY

Refines

Organisation du modèle

Constantes

Ordonnanceur

du terminal

Terminal

DEMONEY

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du terminal

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Interface :

EmissionAPDUVersCarte

TraitementAPDU

Reset_JCRE

JCRE

Raffinement

du JCRE

Refines

Organisation du modèle

Constantes

Ordonnanceur

du terminal

JCRE

DEMONEY

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement de

l'ordonnanceur

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Terminal

Raffinement

du terminal

Refines

Interface :

EmissionReset

EmissionSelect

EmissionGetData

EmissionStoreData

EmissionInitializeUpdate

EmissionExternalAuthentification

EmissionInitializeTransaction

EmissionCompleteTransaction

EmissionVerifyPIN

TraitementErreur

Organisation du modèle

Constantes

Terminal

JCRE

DEMONEY

ProcessAPDU

APDU

DEMONEY

GestionSolde

Raffinement

du terminal

Raffinement

du JCRE

Raffinement

de DEMONEY

Raffinement de

ProcessAPDU

Raffinement

de DEMONEY

GestionSolde

Sees

Refines

Refines

Refines

Refines

Refines

Extends

Includes

Includes

Includes

Includes

Includes :	Recopie du code. Les invariants importés sont préservés

par la machine qui les importe.

Sees :	Vision des constantes.

Refines :	Raffinement d'une machine par une autre.

Extends :	Inclusion avec exportation des opérations et variables incluses.

Ordonnanceur

du terminal

Raffinement de

l'ordonnanceur

Refines

Evénements déclenchables :

AttenteCarte

RetraitCarte

EmissionsHasardeuses

EmissionsCoherentes

TraitementErreur

IV. Vérification de propriétés et politiques de sécurité

Vérification des propriétés
de DEMONEY

Atomicité :

Les opérations de mise à jour du solde ne doivent pas être interrompues

Si l'on finalise une transaction alors elle était en cours :

Si l'on interprète un APDU différent de CompleteTransaction alors aucune transaction n'est en cours :

Vérifier sur le graphe comportemental

Les opérations de sécurisation du canal ne doivent pas être interrompues

Idem.

III. Propriétés et objectifs de sécurité

PROCESS_APDU :
INS_APDU_CompleteTransaction = PRE TransactionEc=TRUE THEN .... END

PROCESS_APDU :
INS_APDU_GetData = PRE TransactionEc=FALSE THEN ... END

(pour toute les autres commandes)

Vérification des objectifs et politiques de sécurité

On ne peut pas créer d'argent :

Crédit : récupérer de l'argent avant de créditer

Vérifier sur le graphe comportemental

Solde >= 0

III. Propriétés et objectifs de sécurité

DEMONEY_GestionSolde :

INVARIANT

SoldeCourant : 0..SoldeMaxi

DEMONEY_GestionSolde :

INVARIANT

SommeTransEc : Int16 &

SommeTransEc >= 0 &

((TransactionEc = Trans_Credit) => ((SoldeCourant + SommeTransEc) : 0..SoldeMaxi))

Vérification des objectifs et politiques de sécurité

Il est difficile de perdre de l'argent :

Solde mis à jour seulement si débit possible

III. Propriétés et objectifs de sécurité

DEMONEY_GestionSolde :

INVARIANT

SommeTransEc : Int16 &

SommeTransEc >= 0 &

((TransactionEc = Trans_Debit) => ((SoldeCourant - SommeTransEc) : 0..SoldeMaxi))

Vérification des objectifs et politiques de sécurité

Seul le titulaire du compte peut créditer la carte par virement :

Code PIN avec nombre d'essais limité

III. Propriétés et objectifs de sécurité

Process_APDU :

INVARIANT

NbEssaisPINRestant>0 => PINBlocked=FALSE

OPERATIONS

INS_APDU_VerifyPIN = PRE TransactionEc=Trans_None & NbEssaisPINRestant > 0 THEN

NbEssaisPINRestant := NbEssaisPINRestant-1 ; ....

END

V. Conclusion

Travail à venir

Règles systématiques d'expression de propriétés de sécurité en B.

Méthode de conversion automatique d'un modèle B classique en un système B événementiel.

GénéSyst : la possibilité de vérifier une propriété sur un automate.

Vérification modulaire.

Références

Présentation de l'application DEMONEY C. Paulin (01/2004)

DEMONEY : a démonstrative Electronic purse
R. Marlet et C. Mesnil (Trusted Logic, 11/2002)

DEMONEY : JavaCard implementation, R. Marlet (11/2002 – 3 pages pour préciser l'annexe B)

Security properties and Java Card Specificities to be studied in the SacSafe Project, R. Marlet, D. Le Metayer (8/2001 – Spécificités des applets JavaCard. Propriétés à vérifier par analyse statique)

JavaCard 2.1 Platform Specifications

Manual for TL-FIT Draft, Trusted Logic

Références

2004-05-05T10:46:45