Brevet FR2840084A1 — publié le 20031128

rithme. 1 2840084 Procede de verification de codes pour microcircuits a ressources limitees La presente invention concerne un procede de verification de codes utilises avec des microcircuits a ressources limitees, tels que utilises dans des cartes a puce, notamment pour verifier l'integrite et assurer l'innocuite du code. Les cartes a microcircuit electronique, cites cartes a puce, vent utilisees comme support informatique mobile pour des applications tres diverges et exigeant pour la plupart d'entre elles un haut niveau de securite, notamment les operations bancaires, les paiements securises, l'acces aux batiments ou a des zones securisees et les telecommunications. L'utilisation repandue des cartes a puce et la diversite de leurs applications tendent actuellement a l'utilisation de plateformes ouvertes, telle la plateforme connue sous le nom de "Java", qui permet le chargement, dans la memoire d'une machine de traitement de donnees electroniques, d' applications compatibles avec la plateforme. Une plateforme tel que Java presente deux avantages, la standardisation du code intermediaire, dit "bytecode", et son independence par rapport a la machine. Tout programme Java peut done etre compile en une serie d' instructions bytecode universellement comprises par toute machine basee sur une telle plateforme. Etant donne que les cartes a puce ou d'autres systemes embarques vent mobiles et qu'elles vent ut ili sees en relation avec de s systeme s informat iques etrangers, ou qutelles executent un bytecode d'origine soit inconnue, soit non-securisee, il est necessaire de 2 2840084 verifier l' integrite et l' innocuite du programme utilise avec la carte ou avec d' autres systemes embarques. Un programme de verification de code intermediaire de type Java est decrit dans le brevet US 5,740,441. Le S procede de verification decrit dans ce brevet est adapte aux systemes informatiques tels que des ordinateurs PC dont la puissance de calcul de leur processeur et la capacite de leur memoire vive RAM (Random Access Memory) vent nettement superieures a celles d'une carte a puce. La puissance d'un processeur et la capacite de la memoire vive ou de la memoire persistante ROM (Read Only Memory) vent fonction de la surface de silicium encarte. Les cartes a puce devant d'une part respecter des contraintes mecaniques, en particulier la torsion et la flexion, et d'autre part garantir une duree de vie raisonnable, leur surface de silicium ne depasse generalement pas 25 mm2. La memoire d'une carte a puce a typiquement une capacite d' environ 8 kilo-octets, par consequent bien inferieure a la capacite de RAM dont dispose l'ordinateur PC le moins performant propose actuellement sur le marche. Il existe plusieurs solutions permettant de verifier le bytecode dans des dispositifs dont la capacite de memoire est tres limitee. L'une de ces approches consiste a ajouter au code le resultat d'un algorithme de pre-calcul qui sera ensuite repris par le verifieur du bytecode. Il peut s'agir par exemple de la methode PCC (Proof Carrying Code) ou d'une variante de cette derriere qui permet au verifieur encarte d'utiliser des algorithmes plus simples. Un programme, tel qu'un apples Java quelconque, ne comprennent pas le code supplementaire PCC, ne pourra done pas etre verifie par le microcircuit. La sphere 3 2840084 d'utilisation des microcircuits utilisant ces methodes est done limitee. Une autre approche consiste a modifier le code intermediaire du programme a verifier a l'exterieur du dispositif de telle sorte que le procede de verification soit plus aise sans entralner pour autant une diminution de fiabilite, telle que decrite dans la demande de brevet internationale WO 0114958 A2. Dans cette demande, on decrit un procede de verification d'un programme de type Java dans loquel l'on modifie le code intermediaire par un procede dit '' de normal i sat ion" dans un systeme de traitement de donnees externe avant de transferer ce code modifie dans un systeme embarque. Lors de cette normalisation, le registre reel des types est realloue a un registre virtue!, chaque case de ce registre ne definissant qu'un type, c'est-a-dire que le registre virtuel est monomorphe. Cette modification permet done de reduire fortement la consommation en memoire necessaire pour stocker les differents types d'un registre polymorphe lors du procede de verification. Si le procede de verification de ce code modifie se termine avec succes, le code modifie est ensuite execute par le systeme embarque. L'un des desavantages de ce procede est que l'on ne peut pas etre absolument sur que le code modifie dans le systeme externe correspond au code original et sera execute correctement par le systeme embarque. D'autre part, le fait d' executer un code modifie selon le procede decrit dans la demande de brevet precitee, limite l'utilisation de certaines techniques d'optimisation de calcul du programme. De maniere generale, les procedes conventionnels de verification du code intermediaire (bytecode) Java destines a etre utilises dans des microcircuits a 4 2840084 ressources limitees peuvent egalement avoir les inconvenients d' augmenter la quantite d'informations a transmettre au microcircuit, de necessiter ['implementation et l' execution d'un logiciel relativement complexe dans le systeme informatique externe en communication avec la carte a puce, ou de limiter l'utilisation de certaines techniques d'optimisation de calcul du programme. Tenant compte de ce qui precede, l'un des objectifs de l' invention est de fournir un procede de verification de code intermediaire destine a etre execute dans un objet a microcircuit a ressources limitees, gable et econome en termes d' occupation des ressources de memoire du microcircuit, notamment la memoire volatile ou d'autres memoires accessibles en ecriture et lecture du microcircuit. Il est avantageux de fournir un procede de verification destine a etre execute dans un objet a microcircuit a ressources limitees qui ne compromet pas l' execution du code intermediaire et qui ne limite pas l'utilisation des techniques d'optimisation de calcul du code intermediaire. Il est avantageux de fournir un procede de verification destine a etre execute dans un objet a microcircuit a ressources limitees, ayant un large spectre d'utilisation pour une plateforme donne, tel que le Java ou des variantes telles que le Javacard. Il est en outre avantageux de reduire l'utilisation des ressources de calculs du microcircuit de ['objet. Il est egalement avantageux de reduire le temps necessaire pour effectuer la verification d'un programme a verifier. 2840084 Des buts de l' invention vent realises par un procede selon la revendication 1. Dans la presente invention, un procede de verification de codes intermediaires executable par un microcircuit a ressources limitees connecte a un systeme de traitement de donnees externe, comporte une etape de modification du code intermediaire comprenant la reallocation de registres reels de types a des registres virtuels de types monomorphes, et de construction d'un code realloue dont les instructions font reference aux registres virtuels, et une etape de verification du code realloue dans le microcircuit a ressources limitees, caracterisee en ce que, en cas de succes de la verification du code realloue dans le microcircuit, l'on installe le code intermediaire original dans le microcircuit a ressources limitees pour execution. Dans une premiere forme d' execution, la modification du code intermediaire original peut etre effectuee dans un systeme de traitement de donnees externe avant son chargement dans le microcircuit a ressources limitees, la modification comprenant la generation d'un composant de reallocation incluant un tableau de reallocation definissant la reallocation des donnees du type d'un registre reel a des donnees du type d'un registre virtuel monomorphe. Dans cette forme d' execution, le procede de verification comprend la verification du composant de reallocation et, en cas de succes, la verification du code realloue, le code realloue etant construit soit lors du procede de verification du composant de reallocation, soit apres verification du composant de reallocation. Si la verification du code realloue se termine avec succes, le bytecode original est installe pour execution, le bytecode original etant soit stocke dans une memoire 6 2840084 persistante accessible en lecture et en ecriture du microcircuit, soit charge depuis le systeme externe. Dans ce dernier cas, afin d'assurer que le bytecode original installe depuis le systeme externe correspond au code original qui a ete verifie lors du premier chargement du bytecode original, un calcul de hachage du code intermediaire original est effectue et compare avec le resultat du calcul de hachage du code intermediaire original a reinstaller apres le procede de verification. Dans une autre forme d'execution, les etapes de calcul de la reallocation et de la construction du code realloue peuvent etre effectuees dans le microcircuit a ressources limitees, le code intermediaire original etant charge dans le microcircuit avant lt execution du procede 1S de verification et stocke dans une memoire du microcircuit, par exemple dans une memoire persistante accessible en lecture et en ecriture, du type EEPROM (Electrical Erasable Programmable Read Only Memory). Avantageusement, la generation d'un code realloue pour verification permet de generer un registre du type monomorphe reduisant la consommation de la memoire volatile du microcircuit lors de la verification du code intermediaire. L' installation du code intermediaire original pour execution, apres le procede de verification, permet toutefois d'eviter des problemes eventuels lies a l' execution d'un code intermediaire modifie et permet egalement l'utilisation de techniques de calcul optimisees. D'autres caracteristiques avantageuses de l' invention ressortiront des revendications, de la description detaillee de formes d' execution de l' invention donnee ci-apres et des dessins annexes, dans lesquels: 7 2840084 la Fig. 1 montre un organigramme illustrant l'enchalnement des etapes d'un precede de verification d'un code intermediaire selon une premiere forme d' execution de l' invention; la Fig. 2 est une representation simplifies d' instructions du code intermediaire (bytecode) et d'un tableau de reallocation associe aux instructions du code intermediaire; la Fig. 3 est une representation simplifies d'un exemple de code intermediaire avec son tableau de reallocation selon une forme d' execution de l' invention; la Fig. 4 montre un organigramme illustrant l'enchalnement des etapes pendant le precede de verification du tableau de reallocation; la Fig. 5 est une representation simplified de l' affectation et de la mise a j our du tableau de reallocation courante pour une instruction du code intermediaire et du type "clef r", qui est une instruction definissant une valeur dans le registre reel associe a l' instruction; la Fig. 6 est une representation simplifies de l' affectation et de la mise a j our du tableau de reallocation courante pour une instruction du type " use r", qui est une instruction utilisant une valeur r dans un registre associe a l' instruction courante; la Fig. 7 est une representation simplifies de l' affectation et de la mise a j our du tableau de reallocation courante pour une instruction du code intermediaire du type "arch", qui est une instruction de branchement a au mains deux instructions; la Fig. 8 est une representation simplifies de l' affectation et de la mise a j our du tableau de 8 2840084 reallocation courante pour une instruction du type "nop", qui est une instruction qui ne comporte pas d' operation sur le registre associe a l' instruction courante; la Fig. 9 est une representation simplifiee de s l' affectation et de la mise a j our du tableau de reallocation courante pour une instruction du type "return") la Fig. 10 montre un organigramme illustrant l'enchalnement des etapes dans un procede de verification de code intermediaire selon une deuxieme forme d' execution de l' invention. Faisant reference a la Fig. 1, les etapes d'un procede de verification d'un code intermediaire, tel qu'un bytecode Java ou Javacard, selon une premiere forme d' execution de l' invention, vent montrees. Un microcircuit a ressources limitees notamment pour un systeme embarque tel qu'une carte a puce, est connecte a un systeme de traitement de donnees externe (ci-apres "systeme externe") pour le chargement et l' execution d'un programme tel qutun apples Java, ou Javacard, dans le microcircuit. Le systeme externe effectue la compilation et la conversion du programme Java en un fichier. cap, c'est-a-dire le code intermediaire (bytecode) executable par le microcircuit. 2s Dans cette premiere forme d'execution, l'on ajoute au code intermediaire original un composant de reallocation comprenant un tableau de reallocation T. tel que montre dans les Figures 2 et 3. Ce composant de reallocation est genere par le systeme externe par une methode du calcul de reallocation connue, telle que la methode de "coloration de graph". Le calcul de reallocation par coloration de graph est bien connu en tent que tel et est utilise par exemple 9 2840084 dans le procede de verification decrit dans la demande internationale WO 0114958 A2. Toutefois, dans la demande precitee, le code intermediaire original est modifie par un procede dit de "normalisation", Ainsi, d'une part, les instructions du code intermediaire et le registre vent modifies, de sorte que le registre est monomorphe, ctest- a-dire que chaque registre ne recoit des donnees representant un seul type et, d'autre part, a chaque instruction de branchement, la pile est vice. Cette transformation permet de rendre le procede de verification lineaire et d'eviter la forte consommation en memoire volatile (RAM) que necessite le stockage de registres pouvant accepter des donnees representant differents types, c'est-a-dire les registres polymorphes. IS Dans la methode connue precitee, le bytecode Java ainsi modifie est utilise pour l' execution du programme apres verification. L' execution du code modifie peut d'une part avoir des consequences sur la fiabilite de l' execution, d'autre part elle limite les possibilites d'utiliser les techniques d'optimisation connues du bytecode Java, utilisees par exemple pour reduire le temps d' execution ou le temps de communication avec le systeme externe. Dans la presente invention, le code intermediaire 2s (bytecode) original ainsi que le composant de reallocation est charge dans le microcircuit a ressources limitees. Le code intermediaire original est stocke en memoire du microcircuit, par exemple dans une memoire persistante accessible en ecriture et en lecture de type EEPROM et le composant de reallocation est charge dans une memoire volatile (RAM) du microcircuit. Apres chargement, le composant de reallocation est verifie (etape 110) et, en cas de succes, l'on procede a la io 2840084 construction du code realloue (etape 112) et finalement a une etape de verification du code realloue (etape 114) avant l' installation du code intermediaire original stocke dans la memoire persistante (etape 116) pour execution. En cas d'echec du procede de verification du composant de reallocation ou du procede de verification du code realloue, le code intermediaire est rejete et n'est pas installe pour execution. Il est a remarquer que la construction du code realloue peut etre effectuee lors du procede de verification du composant de reallocation, c'est-a-dire que les etapes 110 et 112 peuvent etre confondues. La procedure de verification du composant de reallocation sera decrite plus en detail ci-apres, en faisant reference aux Figures 2 a 9: La Fig. 2 montre, de maniere simplifiee, une serie d/instructions PC du code intermediaire ainsi qu'un composant de reallocation T du registre reel de donnees de type. Les instructions du code intermediaire peuvent etre classees parmi les cinq classes d' instructions suivantes en fonction de leur effet sur la reallocation du registre de donnees de type correspondent. "clef x": On definit la valeur de la variable x dans le registre (par exemple les instructions "sstore", "astore") "use x": On utilise la variable x dans le registre (par exemple les instructions "sload", "aload") "nop": On n'effectue aucune operation sur les valeurs du registre (par exemple les instructions "sxor", "iadd") "return": On sort de la methode (par exemple les instructions "areturn", "sreturn") 1 1 2840084 "brch x y: On branche a des instructions cibles x ou y (par exemple les instructions "ifeq", "if- sampoq") Faisant reference plus particuTierement aux Figures 2 et 3, le composant de reallocation T comprend un sous- tableau D contenant la reallocation pour chaque instruction qui definit le type d'une variable x dans le registre rx, ctest-a-dire une instruction de la classe "clef x", et un tableau de reallocation F ayant le meme nombre de colonnes k que de registres reels et le meme nombre de lignes S que d' instructions PC. Le tableau F est un tableau resultant de la reallocation des registres reels de donnees de type rx a des registres virtuels vy. Chaque registre rx de meme type est realloue a un seul registre virtuel vy correspondent a ce type. Les registres reels dont le type peut changer, c'est-a-dire les registres polymorphes, vent realloues a differents registres virtuels correspondents aux differents types de ces registres. Comme chaque registre virtuel ne definit qu'un seul type, les registres virtuels vent monomorphes, c'est-a-dire les variables pour lesquelles il existe un type restent valables tout au long du procede de verification du code intermediaire. L'algorithme de verification est beaucoup plus simple dans le cas des variables monomorphes, du fait qu'il convient simplement de trouver pour chaque variable le type de la variable qui sera valable tout au long de la procedure de verification. I1 s'agit en fait d'un calcul de point fixe ou le type des variables est specialise jusquta ce qu'il reste inchange. Un tel algorithme echoue si on lui presente des variables polymorphes comme etant des variables monomorphes. 12 2840084 Le procede de verification du composant de reallocation utilise un tableau courant F' (voir Fig. 3) contenant le type de chaque variable pour l' instruction (PC) courante, de sorte que les types contenus dans ce tableau courant F' correspondent a l' evolution de la reallocation courante lors de la verification du composant de reallocation T. Le tableau courant F' peut done etre represente par une seule ligne et un nombre de colonnes egal au nombre k de registres reels. I0 Au debut du procede de verification, c'est-a-dire a l' instruction PC1, les donnees du tableau de reallocation courante vent initialisees (etape 402 de la Fig. 4) avec le type "nul ", telles que montrees dans la Fig. 3, qui est le plus petit element du treillis des types, au lieu IS du type " top" qui reunit tous les types, c'est-a-dire le plus grand element du treillis des types. On lit ensuite la premiere instruction (etape 404 de la Fig. 4) et en fonction de la classe d' instruction du code intermediaire, l'on effectue une verification suivie par une mise a j our du tableau de reallocation courante F' ou simplement une mise a j our du tableau de reallocation courante. Pour les instructions sans operation sur le registre "nop" et de retour "return", l'algorithme de verification effectue simplement une mise a j our du tableau de reallocation (etapes 412 respectivement 414 de la Fig. 4), telle que montree dans les Figures 8 respectivement 9. Dans le cas d'une instruction de type "nop", la mise a j our consiste simplement en un report des donnees de type (f' i) dans le tableau de reallocation courante, c'est- a-dire que les donnees de type vent conservees sans changement pour la prochaine instruction PC:+1. Dans le cas d'une instruction de classe "return", la mise a j our 13 2840084 consiste en l' affectation des donnees de type (f'+l,i) du soul-tableau de reallocation F de l' instruction suivante PCc+1 dans le tableau de reallocation courante F', telle que montree dans la Fig. 9. Dans le cas d'une instruction de definition "def", l'on affecte les donnees de type (da) dans le sous tableau D contenant la reallocation pour l' instruction (PCO) en question, au registre correspondent du tableau de reallocation courante F', c'est-a-dire si l' instruction courante PCO definit la valeur d'un registre (f,x) la reallocation (o;=vy) definie dans le tableau D est affectee et met a j our le registre ( f O, x) du tableau de reallocation courante F'. Lors de cette mise a jour, les autres valeurs ( f 'O. i a f tO, X-l et f ':, x+ IS a f ',-, k) du tableau de reallocation courante vent conservees, telles que montrees dans la Fig. 5. Si l' instruction est de classe "use rx'', l'algorithme de verification verifie simplement si la valeur du registre correspondent (la colonne x) du tableau de reallocation courante F' n'est pas egale a la valeur "nul", qui est la plus petite valeur du treillis des types. La mise a j our pour cette instruction est simplement la conservation des donnees de type (f', i) du tableau de reallocation courante F', telle que montree a la Fig. 6. Dans le cas d'une instruction de branchement, la verification consiste a comparer les donnees de type (f 72, i) dans le tableau dans le tableau de reallocation courante F' correspondent a l' instruction courante PC avec les donnees de type (f 'n,i) du tableau de reallocation F aux instructions cibles PCp et PCy et, en cas d'inegalite, la procedure de verification se termine 14 2840084 avec un echec. Le tableau de reallocation courante F' est ensuite mis a j our en affectant les donnees de type du tableau de reallocation F a l' instruction suivante PCa+ au tableau de reallocation courante F'. La prochaine etape (416) consiste a verifier s'il reste encore des instructions a fire et, dans ['affirmative, d'incrementer le pointeur de l' instruction courante (etape 418) et de repeter la boucle de lecture de l' instruction (etape 414) et de verification et de mise a j our de la reallocation courante jusqu'a ce qutil n'y ait plus d' instructions a fire. Le programme de verification passe ensuite a l'etape de construction du code realloue (etape 112) et a la verification du code realloue (etape 114). La verification du code realloue suit les procedes de verification connus. Il est toutefois a remarquer que le code realloue peut etre construit lors de la verification du composant de reallocation (etape 110) en changeant la variable sur laquelle agit l' instruction a sa valeur reallouee. Par exemple, si une instruction de definition "clef r1'' (voir Fig. 3) agit sur le registre r1 qui est realloue au registre virtuel v1, alors l' instruction du code realloue devient "clef vl'', de sorte qu'elle agit sur le registre virtuel de donnees de type au lieu du registre reel de donnees de type original. On constate done que les instructions vent lues lineairement de la premiere a la derriere instruction, chaque instruction etant executee par l'interpreteur de type. Pour les instructions d'utilisation d'une variable ( " use"), sans operation sur les registres ( "nop") ou de retour ( " return"), le comportement de l'algorithme de 2840084 verification est similaire a celui d'un verifieur conventionnel. Cependant on doit garantir lors d'une instruction d'utilisation " use x" que la variable "x" sur laquelle agit cette instruction a ete bien definie auparavant, alors que la variable peut avoir ete initialisee dans une autre branche du programme avant cette instruction. Ce probleme est resolu en verifiant que la valeur stockee dans le soul-tableau D pour une instruction de definition "clef x" specialise le type precedent de la variable x dans le tableau de reallocation courante F'. Pour cette raison il est important qu'au debut du programme, les variables du tableau F' vent initialisees a "nul " pour leur permettre d'etre specialisees. On remarque que sur une instruction de branchement "brch", l'algorithme de verification n'effectue aucun changement au tableau de reallocation courante F' et avance d'une instruction. Une fois arrive a la fin du code intermediaire, le programme recommence au debut jusqu'a ce que le type de chaque variable reste inchange. L'algorithme de verification echoue quand on lui presente un code avec des variables non monomorphes, car il verifie sur les instructions de definition "clef" que les donnees de type dans le soul-tableau D specialisent le type deja present dans le tableau de reallocation courante F'. Un code qui passe la verification monomorphe et initialise les donnees de type de ses variables doit etre correctement type, puisque chaque registre virtuel (vi) ne peut contenir qu'un seul type. En d'autres moss, l'interpreteur de types verifie que toutes les utilisations possibles d'une variable vent conformes avec son type et ceci est done assure par le fait que les operations des instructions PC sur le tableau de reallocation F passent une verification monomorphe. Une reallocation est valide si dans le code intermediaire original, toute instruction d'utilisation "use x" utilise la meme reallocation que toutes les instructions de definition "clef x" qui ont pu la defining C'est a dire que dans le code genere pour la verification, si une instruction " use x" s ' est transformee en "use y", alors l' instruction "clef x" s'est transformee en "clef y". La validite de la proposition precedente peut etre demontree par un raisonnement par l'absurde. Soit une reallocation non valide pour laquelle l'algorithme se termine sur la fin du code. Si la reallocation ntest pas valide, il existe alors une instruction "use x" dans le champ d'une instruction "clef x" pour laquelle la reallocation de la variable x est la variable z, alors que la reallocation de la variable x pour l' instruction "clef x" est la variable y, ou la variable y est differente de la variable z. Il existe une sequence d'instructions du code intermediaire original "clef x", "i-l", "i-2"'... '" i-k", "use x" qui conduit de l' instruction "clef x" a "use x" par un flot d'executions correctes. Il n'y a pas d'autre instruction "clef x" a l'interieur de la sequence, sinon ce serait elle qui definit l' instruction "use x". Toutes les autres instructions preservent la reallocation courante du registre x lors du deroulement de l'algorithme. En effet, les instructions "nop", "return" et "use" ne changent pas la reallocation courante et l' instruction de branchement "brch" s' assure que la reallocation apres le branchement est la meme que celle avant. 17 2840084 La sequence d' instructions precitee est done en contradiction avec la proposition par l'absurde, ce qui demontre la validity de la proposition initiate, objet de la demonstration. On pent egalement demontrer par le raisonnement suivant que si un code intermediaire, genere a partir d'un code intermediaire original et de son tableau de reallocation valide, passe un precede de verification, alors le code intermediaire original passe aussi le precede de verification. Supposons que dans le precede de verification du code intermediaire on stacks en memoire volatile (RAM) les types des variables pour chaque cible de branchement ainsi qu'un tableau courant et une liste de travail. Les tableaux vent initializes avec le type " top", le plus grand element du treillis des types. Le tableau courant est egalement initialise avec le type " top" pour chaque variable non parametree et avec les types de la signature pour les variables parametrees. L'algorithme de verification commence avec l' instruction associee au point d' entree de la methode dans la liste de travail. On enleve la premiere instruction de la liste de travail. On calcule le nouveau tableaucourant apres l' execution de cette instruction a partir de l'interpreteur de type et on l'unifie a tous les tableaux qui correspondent aux instructions qui peuvent succeder. On rajoute a la table de travail les instructions dont les tableaux ont change. Le code intermediaire est verifie avec succes si l'on aboutit a une liste de travail vice. Le precede de verification rejet un algorithms si une unification de types est impossible ou si l'interpreteur de types rencontre une instruction incompatible avec les donnees de type dans le tableau des registres. 18 2840084 En prenant une etape quelconque de la verification du code intermediaire original, l'on a comme hypothese que la verification s'est bien deroulee jusqu'a present, en on a a disposition le tableau courant et le contenu des registres. On part aussi de l'hypothese que l'etape correspondante de la verification du code intermediaire avec reallocation se deroule bien et on salt que la reallocation est valide. Pour terminer cette demonstration, on distingue plusieurs cas selon l' instruction en cours: "nop": L' instruction ne concerne pas les variables, on avance a l' instruction suivante sans rien modifier. Le procede de verification ne peut pas echouer sur une instruction "nop". "clef x": Mise a j our du tableau courant avec le nouveau type. Le procede de verification ne peut pas echouer sur un "clef" car il prend un argument dans la pile, mais on n'est pas concerne par les types dans la pile. "return": La verification se pour-quit normalement. Le procede de verification ne peut pas echouer ici. " use x": Le procede de verification peut echouer si l'interpreteur de type decide que le type de la variable x n'est pas compatible avec son utilisation. La validite de la reallocation nous assure que la reallocation de la variable x n'a pas change entre cette instruction "use" et les instructions "clef" qui lui correspondent. Comme la verification du code realloue a reussi jusqu'ici, le type de la variable x est compatible avec son 19 2840084 utilisation. Donc, le procede de verification passe avec succes sur l' instruction. "brch x y": Le procede de verification peut echouer dans l' unification du tableau courant avec s celui correspondent au registre x ou avec celui correspondent au registre y. Or, la validite de la reallocation nous assure que la reallocation courante au moment de l' instruction de branchement "brch" est la meme que celle en x et en y. De plus, la verification du code realloue reussit pour cette instruction, la verification reussit done aussi pour le code intermediaire non realloue. En ce qui concerne le traitement des exceptions dans le code intermediaire, si l'on se trouve sur une partie de code protegee par un "handler" d'exception, chaque instruction doit etre consideree comme un branchement potentiel vers la portion de code intermediaire qui traite l' exception, c'est a dire que la reallocation courante doit etre la meme que celle donnee dans le tableau de reallocation de ltexception. Si ce traitement des exceptions permet d'assurer la correction du typage, il est par contre trop restrictif dans le sens ou il ne 2s permet pas de changer la reallocation d'une variable a l'interieur d'un bloc protege par un meme handler d'exception. Exemple: PC 1: def r1 comme entier: reallocation rl-> v1 PC 2: def r1 comme reference: reallocation rl-, V2 Si les deux instructions "clef" vent protegees par le meme "handler" d' exception et que la variable r1 n'est pas utilisee dans le traitement de l' exception, alors le 2840084 typage est respecte, mais l'algorithme de verification du tableau de reallocation echoue car la variable r1 ne peut avoir qu'une seule reallocation a l' entree du traitement de l' exception. La solution est de creer un registre factice (appelons le Top) qui interdit l'utilisation du registre reel realloue en Top. Dans l'exemple, il suffit de reallouer a Top le registre r1 dans le tableau de reallocation du traitement de l' exception. Une reallocation a Top se transmet par les branchements et peut apparaitre dans un tableau de reallocation qui correspond au debut du traitement d'une exception. En ce qui concerne les appels de soul-routines, on doit tenir compte du fait qu'elles font perdre le lien entre les instructions " use" et les instructions "clef" des variables. Pour rendre compatible les reallocations avec les appels de soul-routines JSR/RET, il faut ajouter un systeme de contexte de reallocation. En faisant reference a la Fig. 10, dans une deuxieme forme d'execution de l' invention, le calcul de la reallocation et du code realloue (etape 1010) est effectue entierement dans le microcircuit a ressources limitees, suivi d'une etape 1012 de verification du code realloue dans le microcircuit et, en cas de succes, l' installation du code intermediaire original pour execution (etape 1016). Le calcul de la reallocation et du code realloue dans le microcircuit peut etre effectue selon les methodes connues, toutefois sans qutil soit necessaire d'effectuer une optimisation du code realloue du fait qu'il n'est pas utilise pour lt execution, mais uniquement pour la verification de l'integrite et de l'innocuite du code intermediaire. Le code intermediaire peut soit etre stocke en memoire persistante accessible en ecriture et en lecture, 21 2840084 par exemple de type EEPROM, lors du premier chargement depuis le systeme externe, soit etre reinstalls apres verification, en appliquant une fonction de hachage au premier chargement, en stockant le resultant dans une memoire du microcircuit et en le comparant avec la valeur de hachage calculee a partir du code intermediaire charge apres verification. 22 2840084 Revendications 1. Procede de verification de code intermediaire executable par un microcircuit a ressources limitees connecte a un systeme de traitement de donnees externe, comportant une etape de modification du code intermediaire comprenant la reallocation des registres reels de type r a des registres virtuels v de type monomorphe, et de construction d'un code realloue dont les instructions PC font reference aux registres virtuels v, et une etape de verification du code realloue dans le microcircuit a ressources limitees, caracterise en ce que, en cas de succes de la verification du code realloue dans le microcircuit, l'on installe le code intermediaire original dans le microcircuit a ressources limitees pour execution. 2. Procede selon la revendication 1, caracterise en ce que ltetape de la construction du code realloue est effectuee dans le microcircuit a ressources limitees. 3. Procede selon l'une des revendications precedentes, caracterise en ce que le code intermediaire original est charge dans le microcircuit a ressources limitees avant l' execution du procede de verification et stocke dans une memoire du microcircuit. 4. Procede selon l'une des revendications precedentes, caracterise en ce que, dans l'etape de modification du code intermediaire, l'on cree un composant de reallocation T definissant la reallocation des registres reels de type aux registres virtuels monomorphes. 5. Procede selon la revendication precedente, caracterise en ce que le composant de reallocation T 23 2840084 contient un soul-tableau de reallocation D contenant la reallocation pour chaque instruction de definition "clef" du code intermediaire definissant le type d'une variable dans un des registres reels, et un tableau de reallocation F contenant la reallocation des registres reels de type aux registres virtuels monomorphes. 6. Procede selon la revendication precedente, caracterise en ce que, lors du procede de verification du composant de reallocation T. l'on verifie si le sous tableau de reallocation D pour les instructions de definition "clef" comporte une valeur de reallocation et, s'il ne comporte pas de valeur de reallocation, le code intermediaire est rejete. 7. Procede selon l'une des revendications precedentes, caracterise en ce que, lors du procede de verification du tableau de reallocation F. pour une instruct ion du code intermediaire qui uti l i se une variable, l'on verifie si la variable utilisee dans le tableau de reallocation courante n'est pas "nul " et, si elle est "nul", le code intermediaire est rejete. 8. Procede selon l'une des revendications precedentes, caracterise en ce que, lors du procede de verification du tableau de reallocation dans le cadre diune instruction de branchement "brch" a des instructions cibles, l'on verifie l'identite du tableau de reallocation courante F' avec les lignes du tableau de reallocation F correspondent aux instructions cibles et, en cas de differences, le code intermediaire est rejete. 9. Procede selon l'une des revendications 1 a 3, caracterise en ce que l'etape de modification du code intermediaire est effectuee dans le microcircuit a