Une m´ethodologie d’analyse d’applications sur carte `a puce 

Des speci cations de nissent les aspects fonctionnels d’une application et garan-tissent des exigences de securit . Durant les etapes de creation de la carte a puce, la notion de securit est traitee. Un produit dit certi a generalement et test non seulement durant la phase de developpement par le constructeur mais aussi par un laboratoire de certi cation a n de garantir son bon fonctionnement vis a vis des speci cations. Ce processus de certi cation permet de reconna^tre un niveau de securit par un laboratoire externe a l’entreprise a l’origine du produit. Pour le paiement de type Europay Mastercard Visa (EMV), EMVCo fournit le document appel « Security Evaluation Process » a ses membres [9]. Il assure une base de securit robuste pour les cartes a puces et produits associes. Pour resumer, EMVCo fournit des documents a n de guider le test et l’evaluation de cartes a puces mais aussi une liste des laboratoires approuves par EMVCo [10].

Plus generalement, l’evaluation de plus haut niveau est permise par la certi ca-tion dite tierce partie, « qui permet a un client de s’assurer par l’intervention d’un professionnel independant, competent et contr^ole, appel organisme certi cateur, de la conformite d’un produit a un cahier des charges ou a une speci cation tech-nique. La certi cation tierce partie apporte au client la con rmation independante et impartiale qu’un produit repond a un cahier des charges ou a des speci cations techniques publiees » [11]. En France, la certi cation s’appuie sur des travaux e ectues par des centres d’Evaluation de la Securit des Technologies de l’Information (CESTI) acredites par le Comite Francais d’Acreditation (COFRAC) selon la norme ISO/IEC 17025 [12]. Les CESTI menent ces evaluations selon les speci cations de l’Agence Nationale de la Securit des Systemes d’Information (ANSSI) a n d’emettre des certi cats attestant que le produit certif est conforme a une speci cation technique appelee cible de securit .

L’evaluation selon les Criteres Communs [13] permet quant a elle de certi er, et ainsi delivrer un certi cat, un produit selon des niveaux d’assurance de securit Evaluation Assurance Level (EAL) tres varies, allant de EAL1 (niveau d’attaquant faible) a EAL7 (niveau d’attaquant eleve). Les certi cats emis par l’ANSSI et bases sur les Criteres Communs peuvent bene cier d’une reconnaissance internationale. On peut aussi citer le CCRA (Common Criteria Recognition Agreement) signe par 25 membres permettant la reconnaissance au niveau EAL2 (niveau d’attaquant basique) et l’accord europeen SOG-I5 [14] regroupant actuellement 10 membres dont les CESTI et permettant la reconnaissance des certi cats jusqu’a EAL4, voire pour certains domaines techniques particuliers jusqu’a EAL7.

Dans cette partie, nous presentons toutes les notions liees a la securit des appli-cations sur carte en decrivant les aspects materiels, les standards et les speci cations a n de positionner les travaux de cette these (illustration dans la gure 1.3).

Un element securis ou « Secure Element »(SE) est une plate-forme « inviolable » capable d’heberger une ou plusieurs applications en toute securit ainsi que leurs donnees con dentielles et cryptographiques (par exemple, gestion des cles). L’authen-ti cation, l’identi cation, la signature et la gestion du PIN sont au coeur du systeme. Le SE contr^ole les interactions entre les sources de con ance (un etablissement nancier), l’application de con ance (une application de paiement) stockee sur la SE et des tiers (un commercant). Le domaine securis protege les informations d’identi – cation de l’utilisateur et traite la transaction de paiement dans un environnement de con ance a n d’assurer la securit des donnees de l’utilisateur. La gure 1.4 fournit un zoom sur le SE de la carte a puce.

Il y a trois di erents types de SE :

{ le SE pour le mobile : Universal Integrated Circuit Card (UICC) { le SE embarqu

{ le SE sous forme de microSD

Chaque SE repond a des besoins di erents du marche. La puce a microcircuit qui reside dans les cartes de paiement a et adaptee pour repondre aux besoins du monde mobile. Avec de multiples applications actuellement stockees et leurs processus executes dans le m^eme dispositif, il est essentiel d’^etre en mesure d’accueillir des applications de con ance dans un environnement securis . Au niveau logiciel, les SEs de type embarqu sont souvent bases sur les systemes d’exploitation ouverts comme JavaCard[16] et MULTOS et repondent aux speci cations GlobalPlatform [17] pour le chargement securis des applications.

Dans cette partie, nous allons exposer les failles existantes sur l’usage de la carte `a puce. Malgr´e une s´ecurit´e importante et un audit s´ecurit´e, nous pouvons voir que des attaques sur ce syst`eme existent [32]. Certaines attaques sont sp´ecialis´ees pour une transaction avec ou sans contact physique. Nous pouvons aussi distinguer les attaques invasives (impliquant une destruction partielle ou compl`ete de la carte) et les attaques non invasives.

Attaques invasives ou semi-invasives :

Ce type d’attaque met en p´eril l’int´egrit´e physique de la puce `a micro-circuit. Les attaques pr´esent´ees ici sont pr´esent´ees dans [33].
Par injection de fautes :
Cette attaque est une attaque semi-invasive car elle n´ecessite un acc`es direct `a la carte `a puce. Il s’agit de perturber le fonctionnement d’une carte `a puce en modifiant une donn´ee pr´ecise. Par exemple, on peut faire varier la tension d’alimentation (power glitch), l’horloge ou encore la temp´erature. Une autre m´ethode consiste `a imposer `a la puce un laser, un faisceau d’ion, un rayon X, etc. Concr`etement, plusieurs techniques ([34] ou [35]) sont connues :
{ Application de lumi`ere laser sur le processeur introduit par [36]
{ Attaque de Bellcore sur le chiffrement RSA (nomm´e par les initiales de ses trois inventeurs) comme dans [35]
{ D´efaillance ´electronique (glitch) appliqu´e sur un calcul RSA, historiquement la premi`ere m´ethode [37] { Attaque de type « Differential fault analysis » (DFA) [37]
La r´ealisation de cette attaque est donc variable d’un syst`eme `a l’autre. Il faut effectuer de nombreux essais, de diff´erentes sortes, afin d’obtenir des r´esultats concluants.
Par conditions anormales Cette attaque varie de l’attaque pr´ec´edente par la dur´ee de la modification apport´ee [38]. Ici, on fait fonctionner la carte `a puce en dehors de ses conditions op´erationnelles. L’attaquant peut modifier la tension ou la fr´equence d’alimentation ainsi que la temp´erature facilement. Cependant, ces attaques ne semblent pas efficaces car des d´etecteurs de conditions anormales sont pr´esents dans la carte `a puce.
Par rayonnement : Afin de modifier l’ex´ecution des applications d’une carte `a puce, on peut aussi utiliser un rayonnement ´electromagn´etique. Cette attaque est semi-invasive car l’attaquant doit acc´eder `a la puce. On applique donc un rayonnement durant l’ex´ecution de l’application (ce qui diff`ere de l’injection de faute) [39].
Par les composants : Ces attaques [40] sont compl`etement invasives car n´ecessitent l’´etude d’un composant pr´ecis de la carte `a puce. On doit donc d´esassembler la carte `a puce et celle-ci ne sera plus utilisable par la suite. Cette premi`ere ´etape se d´eroule chimiquement ou physiquement. Il existe plusieurs outils possibles en vue de cette attaque [40] :
{ Focused Ion Beam (FIB). Cet outil permet d’´etudier un composant avec un microscope ainsi que de retirer de la mati`ere `a la carte `a puce.
{ Electron Beam Tester (EBT). Cet outil permet de lire la valeur du potentiel `a un endroit donn´e de la carte. { Microprobing : acc`es `a la puce.
L’attaquant cherche `a trouver les syst`emes de s´ecurit´e (impl´ementations, informations contenues dans la puce) pr´esents sur un composant en particulier. Par exemple, il est possible de lire les bits sur le bus m´emoire lorsqu’on sait qu’une donn´ee int´eressante y transite.

Attaques non invasives

Ce type d’attaque n’alt`ere pas la puce `a micro-circuit mais consiste `a observer le fonctionnement d’une application.
Par canaux cach´es :
Une attaque sur carte `a puce consiste `a ´etudier le fonctionnement du circuit ´electronique. Plusieurs donn´ees peuvent ^etre utilis´ees telles que la consommation du courant, les ´emissions ´electromagn´etiques ou encore le temps d’ex´ecution. Les attaques par canaux cach´es utilisent les failles mat´erielles de l’impl´ementation pour r´ecup´erer des informations sur le secret utilis´e [41]. On peut ainsi lister plusieurs techniques majeures :
{ consommation du courant : Simple Power Attack / Differential Power Attack / High Order Differential Power Analysis avec par exemple [42]
{ ´emissions ´electromagn´etiques : Simple Electromagnetic Attack / Differential
Electromagnetic Attack [43]
{ le temps d’ex´ecution dans [44]
Skimming : L’attaque dite de  » skimming  » [45] est une attaque simple `a mettre en place, d’o`u son utilisation importante. Il s’agit de r´ecup´erer des informations d’une carte `a puce en pla¸cant un ´el´ement entre le lecteur de carte `a puce et la carte `a puce (`a condition d’avoir la possibilit´e de cr´eer un ´el´ement d’´ecoute d’´epaisseur inf´erieure `a 0,1 mm). Cet ´el´ement a pour but de capturer les donn´ees tel que le num´ero de carte. Sur la figure 1.12, on voit cet ´el´ement sur la photo en haut `a droite. La seconde partie de l’attaque est l’utilisation d’une cam´era (voir la fl`eche noire visible sur la premi`ere image de la figure 1.12). On peut ainsi r´ecup´erer le code PIN (Personal Identification Number) du porteur et se faire passer pour le porteur de la carte, m^eme si g´en´eralement il s’agit uniquement de la lecture et la r´ecup´eration de la piste.

Afin de repr´esenter l’application et ses comportements th´eoriques et donner des informations par rapport aux raisons qui ont conduit `a un mauvais comportement de la part de l’application carte, nous avons d´efini un langage. 

Introduction

 

Contrairement aux m´ethodes formelles tels que la v´erification de mod`ele ou le th´eor`eme de preuve, nous v´erifions `a la vol´ee des s´equences d’´el´ements APDU par rapport `a un oracle, et ceci durant la transaction. En fait, dans les ´etudes [79] [66] [65] [68] or [78], la v´erification n´ecessite un mod`ele formel ou l’acc`es au code source. Avec notre language, nous pouvons d´efinir des comportements th´eoriques (locaux ou globaux) utilisant seulement les donn´ees transmises.

D´efinition

Le langage nous permet de d´efinir `a la fois des machines `a ´etats, permettant de suivre le comportement global d’une application, mais aussi de les partitionner, permettant de suivre le comportement local d’une application. Nous pr´esentons les ´el´ements de base, puis les ´el´ements nous permettant de d´efinir les machines `a ´etats e enfin les ´el´ements nous permettant de d´efinir des comportements locaux. Ce language est d´ecrit en langage de balisage extensible (XML) [135].

El´ements de base

Nous avons d´efini deux types d’´el´ements de base sans lesquels la repr´esentation des donn´ees n’est pas possible. Dans un premier temps, nous avons les ´el´ements repr´esentant la communication APDU :
{ Instruction : repr´esente les octets CLA et INS d’une commande APDU { Parameters : repr´esente les octets P1 et P2 d’une commande APDU { Status : repr´esente les octets SW1 et SW2 d’une commande APDU
Le second type permet de repr´esenter les relations entre plusieurs ´el´ements :
{ And : tous les ´el´ements sont vrais { Or : au moins un ´el´ement est vrai { Nor : tous les ´el´ements sont faux
Afin de compl´eter la repr´esentation des commandes et r´eponses, nous pouvons compl´eter les ´el´ements repr´esentant les instructions, les param`etres et les status words, ´el´ements obligatoires lors d’une communication unitaire commande et r´eponse APDU (un couple APDU). La repr´esentation d’une partie ou de la totalit´e des donn´ees transmises (i.e. les donn´ees contenues dans UDC et UDR). Avec des donn´ees de type TLV, nous pouvons aller plus loin et traiter une partie de la donn´ee compl`ete. De plus, l’appel `a des fonctions externes est possible et permet une utilisation sp´ecifique d’une partie des donn´ees ou d’une association de donn´ees (garder en m´emoire une partie, effectuer des op´erations sur des donn´ees transitant sur plusieurs couples APDU).
Le second type permet de repr´esenter les relations entre plusieurs ´el´ements :
{ Cdata : correspond `a l’UDR entier
{ Rdata : correspond `a l’UDC entier
{ Tag : correspond `a un ´el´ement de type Tag Longueur Valeur (TLV)
{ nom : nom du tag (exemple : 0x9F27) { valeur : valeur de l’´el´ement (exemple : 0x40)
{ mask : permet d’appliquer un masque sur un ´el´ement
{ call : permet l’appel `a une fonction de traitement de donn´ees suppl´ementaires