WO2003100607A2 - Procédé de vérification de codes pour microcircuits à ressources limitées - Google Patents

Procédé de vérification de codes pour microcircuits à ressources limitées Download PDF

Info

Publication number
WO2003100607A2
WO2003100607A2 PCT/EP2003/050193 EP0350193W WO03100607A2 WO 2003100607 A2 WO2003100607 A2 WO 2003100607A2 EP 0350193 W EP0350193 W EP 0350193W WO 03100607 A2 WO03100607 A2 WO 03100607A2
Authority
WO
WIPO (PCT)
Prior art keywords
reallocation
code
intermediate code
microcircuit
type
Prior art date
Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
Ceased
Application number
PCT/EP2003/050193
Other languages
English (en)
Other versions
WO2003100607A3 (fr
Inventor
Jean-François GREZES
Alexandre Benoit
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Gemplus SA
Original Assignee
Gemplus Card International SA
Gemplus SA
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Gemplus Card International SA, Gemplus SA filed Critical Gemplus Card International SA
Priority to US10/515,375 priority Critical patent/US20050252977A1/en
Priority to AU2003238085A priority patent/AU2003238085A1/en
Priority to EP03735717A priority patent/EP1512071B1/fr
Priority to DE60317324T priority patent/DE60317324D1/de
Publication of WO2003100607A2 publication Critical patent/WO2003100607A2/fr
Publication of WO2003100607A3 publication Critical patent/WO2003100607A3/fr
Anticipated expiration legal-status Critical
Ceased legal-status Critical Current

Links

Classifications

    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformation of program code
    • G06F8/41—Compilation
    • G06F8/44—Encoding
    • G06F8/441—Register allocation; Assignment of physical memory space to logical memory space
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for program control, e.g. control units
    • G06F9/06—Arrangements for program control, e.g. control units using stored programs, i.e. using an internal store of processing equipment to receive or retain programs
    • G06F9/44—Arrangements for executing specific programs
    • G06F9/445—Program loading or initiating
    • G06F9/44589—Program code verification, e.g. Java bytecode verification, proof-carrying code

Definitions

  • the present invention relates to a method for verifying codes used with microcircuits with limited resources, such as used in smart cards, in particular for verifying the integrity and ensuring the safety of the code.
  • Electronic microcircuit cards are used as mobile IT support for very diverse applications and requiring for most of them a high level of security, in particular banking, secure payments, access to buildings or secure areas and telecommunications.
  • the widespread use of smart cards and the diversity of their applications currently tend to the use of open platforms, such as the platform known as "Java”, which allows loading, in the memory of a processing machine.
  • electronic data applications compatible with the platform.
  • a platform such as Java has two advantages, the standardization of the intermediate code, called "bytecode”, and its independence from the machine. Any Java program can therefore be compiled into a series of bytecode instructions universally understood by any machine based on such a platform.
  • a Java type intermediate code verification program is described in US Patent 5,740,441.
  • the verification process described in this patent is suitable for computer systems such as PC computers whose computing power of their processor and the capacity of their random access memory (Random Access Memory) are clearly greater than those of a smart card.
  • the power of a processor and the capacity of the random access memory or of the ROM (Read Only Memory) depend on the surface of silicon inserted. Chip cards must on the one hand respect mechanical constraints, in particular torsion and bending, and on the other hand guarantee a reasonable lifetime, their silicon surface generally does not exceed 25 mm 2 .
  • the memory of a smart card typically has a capacity of about 8 kilobytes, therefore much less than the RAM capacity available to the least efficient PC computer currently on the market.
  • One of these approaches consists in adding to the code the result of a pre-calculation algorithm which will then be taken up by the verifier of the bytecode. It can be, for example, the PCC (Proof Carrying Code) method or a variant of the latter which allows the embedded verifier to use simpler algorithms.
  • a program, such as any Java applet, does not include the additional PCC code, therefore cannot be checked by the microcircuit. The sphere use of microcircuits using these methods is therefore limited.
  • Another approach consists in modifying the intermediate code of the program to be verified outside the device so that the verification process is easier without however resulting in a decrease in reliability, as described in the international patent application WO 0114958 A2.
  • a method of verifying a Java type program is described in which the intermediate code is modified by a so-called "normalization" method in an external data processing system before transferring this modified code into a embedded system.
  • the real type register is reallocated to a virtual register, each box of this register defining only one type, that is to say that the virtual register is monomorphic. This modification therefore makes it possible to greatly reduce the memory consumption necessary for storing the different types of a polymorphic register during the verification process.
  • one of the objectives of the invention is to provide an intermediate code verification method intended to be executed in a microcircuit object with limited resources, reliable and economical in terms of occupation of the resources of microcircuit memory, in particular volatile memory or other memories accessible for writing and reading the microcircuit.
  • a method of verifying intermediate codes executable by a limited-resource microcircuit connected to an external data processing system comprises a step of modifying the intermediate code comprising the reallocation of real registers of types to virtual registers of monomorphic types, and construction of a reallocated code whose instructions refer to the virtual registers, and a step of verifying the reallocated code in the microcircuit with limited resources, characterized in that, in the event of success of the verification of the reallocated code in the microcircuit, the original intermediate code is installed in the microcircuit with limited resources for execution.
  • the modification of the original intermediate code can be carried out in an external data processing system before it is loaded into the microcircuit with limited resources, the modification comprising the generation of a reallocation component including an array of reallocation defining the reallocation of data of the type of a real register to data of the type of a monomorphic virtual register.
  • the verification method includes verification of the reallocation component and, if successful, verification of the reallocated code, the reallocated code being constructed either during the verification process of the reallocation component, or after verification of the reallocation component. If the verification of the reallocated code finishes successfully, the original bytecode is installed for execution, the original bytecode being either stored in a persistent memory accessible in read and write of the microcircuit, or loaded from the external system.
  • the steps of calculating the reallocation and of the construction of the reallocated code can be carried out in the microcircuit with limited resources, the original intermediate code being loaded in the microcircuit before the execution of the verification process and stored in a memory of the microcircuit, for example in a persistent memory accessible in read and write, of the type EEPROM (Electrical Erasable Programmable Read Only Memory).
  • EEPROM Electrical Erasable Programmable Read Only Memory
  • the generation of a reallocated code for verification makes it possible to generate a register of the monomorphic type reducing the consumption of the volatile memory of the microcircuit during the verification of the intermediate code.
  • the installation of the original intermediate code for execution, after the verification process makes it possible to avoid possible problems linked to the execution of a modified intermediate code and also allows the use of optimized calculation techniques.
  • Fig. 1 shows a flowchart illustrating the sequence of steps of a method for verifying an intermediate code according to a first embodiment of the invention
  • Fig. 2 is a simplified representation of instructions of the intermediate code (bytecode) and of a reallocation table associated with the instructions of the intermediate code
  • Fig. 3 is a simplified representation of an example of intermediate code with its reallocation table according to an embodiment of the invention
  • Fig. 4 shows a flowchart illustrating the sequence of steps during the process of verifying the reallocation table
  • Fig. 1 shows a flowchart illustrating the sequence of steps of a method for verifying an intermediate code according to a first embodiment of the invention
  • Fig. 2 is a simplified representation of instructions of the intermediate code (bytecode) and of a reallocation table associated with the instructions of the intermediate code
  • Fig. 3 is a simplified representation of an example of intermediate code with its reallocation table according to an embodiment of the invention
  • Fig. 4 shows a flowchart illustrating the sequence of steps during the process of verifying
  • FIG. 5 is a simplified representation of the assignment and of the updating of the current reallocation table for an instruction of the intermediate code and of the "def r" type, which is an instruction defining a value in the real register associated with the instruction ;
  • Fig. 6 is a simplified representation of the allocation and updating of the current reallocation table for an instruction of the "use r” type, which is an instruction using a value r in a register associated with the current instruction;
  • Fig. 7 is a simplified representation of the assignment and of the updating of the current reallocation table for an instruction of the intermediate code of the type "jbrc-h", which is an instruction for connection to at least two instructions;
  • Fig. 8 is a simplified representation of the assignment and updating of the current reallocation for an instruction of the "nop" type, which is an instruction which does not include any operation on the register associated with the current instruction;
  • Fig. 9 is a simplified representation of the assignment and updating of the current reallocation table for an instruction of the "return”type;
  • Fig. 10 shows a flowchart illustrating the sequence of steps in an intermediate code verification method according to a second embodiment of the invention.
  • FIG. 1 the steps of a method for verifying an intermediate code, such as a Java or Javacard bytecode, according to a first embodiment of the invention, are shown.
  • a microcircuit with limited resources in particular for an embedded system such as a smart card, is connected to an external data processing system (hereinafter "external system") for loading and executing a program such as 'a Java applet, or Javacard, in the microcircuit.
  • the external system compiles and converts the Java program to a file. cap, that is to say the intermediate code (bytecode) executable by the microcircuit.
  • a reallocation component comprising a reallocation table T, as shown in Figures 2 and 3.
  • This reallocation component is generated by the external system by a method of known reallocation calculation, such as the "graph coloring" method.
  • the reallocation calculation by graph coloring is well known as such and is used for example in the verification method described in international application WO 0114958 A2.
  • the original intermediate code is modified by a process called "normalization".
  • the instructions of the intermediate code and the register are modified, so that the register is monomorphic, it that is to say that each register does not receive data representing a single type and, on the other hand, at each connection instruction, the stack is empty.
  • This transformation makes the verification process linear and avoids the high consumption of volatile memory (RAM) required by the storage of registers that can accept data representing different types, that is to say the polymorphic registers.
  • the Java bytecode thus modified is used for the execution of the program after verification.
  • the execution of the modified code can on the one hand have consequences on the reliability of the execution, on the other hand it limits the possibilities of using the known optimization techniques of Java bytecode, used for example to reduce the time execution time or the communication time with the external system.
  • the original intermediate code (bytecode) as well as the reallocation component is loaded into the microcircuit with limited resources.
  • the original intermediate code is stored in the memory of the microcircuit, for example in a persistent memory accessible for writing and reading of EEPROM type and the reallocation component is loaded into a volatile memory (RAM) of the microcircuit. After loading, the reallocation component is checked
  • step 110 and, if successful, the reallocated code is constructed (step 112) and finally a step of verifying the reallocated code (step 114) before the installation of the original intermediate code stored in the persistent memory (step 116) for execution. If the verification process of the reallocation component or the verification process of the reallocated code fails, the intermediate code is rejected and is not installed for execution. It should be noted that the construction of the reallocated code can be carried out during the verification process of the reallocation component, that is to say that the steps 110 and 112 can be confused.
  • FIG. 2 shows, in a simplified manner, a series of instructions PC of the intermediate code as well as a reallocation component T of the real type data register.
  • the instructions of the intermediate code can be classified among the following five classes of instructions according to their effect on the reallocation of the corresponding type data register.
  • the reallocation component T comprises a sub-array D containing the reallocation for each instruction which defines the type of a variable x in the register r x , that is to say a instruction of class "def x", and a reallocation table F having the same number of columns k as real registers and the same number of lines S as instructions PC.
  • Array F is an array resulting from the reallocation of real registers of data of type r x to virtual registers v y .
  • Each register r x of the same type is reallocated to a single virtual register v y corresponding to this type.
  • the real registers whose type can change that is to say the polymorphic registers, are reallocated to different virtual registers corresponding to the different types of these registers.
  • the virtual registers are monomorphic, that is to say the variables for which there is a type remain valid throughout the verification process of the intermediate code.
  • the verification algorithm is much simpler in the case of monomorphic variables, since it is simply necessary to find for each variable the type of the variable which will be valid throughout the verification procedure. It is actually a fixed point calculation where the type of variables is specialized until it remains unchanged. Such an algorithm fails if it is presented with polymorphic variables as being monomorphic variables.
  • the method of verifying the reallocation component uses a current table F '(see Fig.
  • the current table F' can therefore be represented by a single line and a number of columns equal to the number k of real registers.
  • the data of the current reallocation table are mitialized (step 402 of FIG. 4) with the type "null", as shown in the Fig. 3, which is the smallest element of the lattice of types, instead of the type "top” which brings together all the types, that is to say the largest element of the lattice of types.
  • the first instruction is then read (step 404 of FIG. 4) and according to the instruction class of the intermediate code, a verification is carried out followed by an update of the current reallocation table F 'or simply a update of the current reallocation table.
  • the verification algorithm simply updates the reallocation table (steps 412 respectively 414 of FIG. 4), as shown in Figures 8 respectively 9.
  • the update consists simply in a transfer of the data of type (f' ⁇ , i) in the current reallocation table, that is that is, the type data is kept unchanged for the next PC + ⁇ instruction.
  • updating consists in assigning the type data (f '+ ⁇ , ⁇ ) of the reallocation sub-table F of the following instruction PC + ⁇ in the current reallocation table F', as shown in FIG. 9.
  • the verification algorithm simply checks whether the value of the corresponding register (column x) of the current reallocation table F 'is not equal to the value "null", which is the smallest value of the types lattice.
  • the update for this instruction is simply the conservation of data of type (f, A from the current reallocation table F ', as shown in Fig. 6.
  • the verification consists in comparing the data of type (f, 2 ) in the table in the current reallocation table F 'corresponding to the current instruction PC ⁇ with the data of type (f r ⁇ ) of the reallocation table F to the target instructions PC ⁇ and PC ⁇ and, in the event of an inequality, the verification procedure ends with a failure.
  • the current reallocation table F ' is then updated by assigning the type data of the reallocation table F to the next instruction PC ⁇ + ⁇ to the current reallocation table F'.
  • the next step (416) is to check if there are still instructions to read and, if so, to increment the pointer of the current instruction (step 418) and to repeat the instruction read loop (step 414) and checking and updating the current reallocation until there are no more instructions to read.
  • the verification program then proceeds to the step of constructing the reallocated code (step 112) and to verifying the reallocated code (step 114). Verification of the reallocated code follows known verification methods. It should however be noted that the reallocated code can be constructed during the verification of the reallocation component (step 110) by changing the variable on which the instruction acts to its reallocated value. For example, if a definition instruction "def '(see Fig. 3) acts on the register r! Which is reallocated to the virtual register v lr then the instruction of the reallocated code becomes" def v', so that it acts on the virtual type data register instead of the original type data real register.
  • the program starts over at the beginning until the type of each variable remains unchanged.
  • the verification algorithm fails when presented with a code with non-monomorphic variables, because it checks on the definition instructions "def" that the type data in sub-array D specialize the type already present in the reallocation array current F '.
  • a code that passes the monomorphic verification and initializes the type data of its variables must be correctly typed, since each virtual register (v) can contain only one type.
  • the type interpreter checks that all the possible uses of a variable conform to its type and this is therefore ensured by the fact that the operations of the PC instructions on the reallocation table F pass a monomorphic verification.
  • any "use x" usage instruction uses the same reallocation as all of the "def x" definition instructions that may have defined it. That is to say that in the code generated for the verification, if a "use x" instruction is transformed into “use y", then the "def x” instruction is transformed into “def y".
  • the intermediate code verification process we store in volatile memory (RAM) the types of variables for each connection target as well as a current table and a work list. Arrays are initialized with the type "top", the largest element of the lattice of types. The current array is also initialized with the "top” type for each non-parameterized variable and with the types of the signature for the parameterized variables.
  • the verification algorithm begins with the instruction associated with the entry point of the method in the worklist. The first instruction is removed from the work list. We calculate the new current table after the execution of this instruction from the type interpreter and we unify it with all the tables which correspond to the instructions which can succeed. The instructions whose tables have changed are added to the work table. The intermediate code is successfully verified if we end up with an empty worklist.
  • the verification process rejects an algorithm if a type unification is impossible or if the type interpreter encounters an instruction incompatible with the type data in the register table.
  • PC 1 def ri as integer: reallocation j ⁇ v ⁇
  • PC 2 def r ⁇ as reference: reallocation r 7 ⁇ v 2 If the two "def" instructions are protected by the same exception handler and the variable rt is not used in the handling of the exception , therefore the typing is respected, but the algorithm for verifying the reallocation table fails because the variable r! can only have one reallocation at the start of the processing of the exception.
  • the solution is to create a dummy register (let's call the Top) which prohibits the use of the real register reallocated in Top. In the example, it suffices to reallocate to Top the register r 2 in the reallocation table for processing the exception.
  • a reallocation to Top is transmitted by the connections and can appear in a reallocation table that corresponds to the start of the processing of an exception.
  • step 1010 the calculation of the reallocation and of the realloue code (step 1010) is carried out entirely in the microcircuit with limited resources, followed by a step 1012 of verification of the realloué code in the microcircuit and, if successful, installing the original intermediate code for execution (step 1016).
  • the calculation of the reallocation and of the code reallocated in the microcircuit can be carried out according to known methods, however without the need to optimize the reallocated code because it is not used for execution, but only for verifying the integrity and safety of the intermediate code.
  • the intermediate code can either be stored in persistent memory accessible in writing and in reading, for example of the EEPROM type, during the first loading from the external system, either to be reinstalled after verification, by applying a hash function on the first loading, by storing the result in a memory of the microcircuit and by comparing it with the calculated hash value from the intermediate code loaded after verification.

Landscapes

  • Engineering & Computer Science (AREA)
  • Software Systems (AREA)
  • Theoretical Computer Science (AREA)
  • General Engineering & Computer Science (AREA)
  • Physics & Mathematics (AREA)
  • General Physics & Mathematics (AREA)
  • Devices For Executing Special Programs (AREA)
  • Debugging And Monitoring (AREA)
  • Design And Manufacture Of Integrated Circuits (AREA)
  • Slot Machines And Peripheral Devices (AREA)
  • Structure Of Printed Boards (AREA)
  • Test And Diagnosis Of Digital Computers (AREA)
  • Microscoopes, Condenser (AREA)

Abstract

L'invention concerne un procédé de vérification de code intermédiaire exécutable par un microcircuit à ressources limitées connecté à un système de traitement de données externe, comportant une étape de modification du code intermédiaire comprenant la réallocation des registres réels de type r à des registres virtuels v de type monomorphe, et de construction d'un code réalloué dont les instructions PC font référence aux registres virtuels v, et une étape de vérification du code réalloué dans le microcircuit à ressources limitées, caractérisé en ce que, en cas de succès de la vérification du code réalloué dans le microcircuit, l'on installe le code intermédiaire original dans le microcircuit à ressources limitées pour exécution.

Description

Procédé de vérification de codes pour microcircuits à ressources limitées
La présente invention concerne un procédé de vérification de codes utilisés avec des microcircuits à ressources limitées, tels que utilisés dans des cartes à puce, notamment pour vérifier l'intégrité et assurer l'innocuité du code.
Les cartes à microcircuit électronique, dites cartes à puce, sont utilisées comme support informatique mobile pour des applications très diverses et exigeant pour la plupart d'entre elles un haut niveau de sécurité, notamment les opérations bancaires, les paiements sécurisés, l'accès aux bâtiments ou à des zones sécurisées et les télécommunications. L'utilisation répandue des cartes à puce et la diversité de leurs applications tendent actuellement à l'utilisation de plateformes ouvertes, telle la plateforme connue sous le nom de "Java", qui permet le chargement, dans la mémoire d'une machine de traitement de données électroniques, d'applications compatibles avec la plateforme. Une plateforme tel que Java présente deux avantages, la standardisation du code intermédiaire, dit "bytecode", et son indépendance par rapport à la machine. Tout programme Java peut donc être compilé en une série d'instructions bytecode universellement comprises par toute machine basée sur une telle plateforme.
Etant donné que les cartes à puce ou d'autres systèmes embarqués sont mobiles et qu'elles sont utilisées en relation avec des systèmes informatiques étrangers, ou qu'elles exécutent un bytecode d'origine soit inconnue, soit non-sécurisée, il est nécessaire de vérifier l'intégrité et l'innocuité du programme utilisé avec la carte ou avec d' autres systèmes embarqués.
Un programme de vérification de code intermédiaire de type Java est décrit dans le brevet US 5,740,441. Le procédé de vérification décrit dans ce brevet est adapté aux systèmes informatiques tels que des ordinateurs PC dont la puissance de calcul de leur processeur et la capacité de leur mémoire vive RAM (Random Access Memory) sont nettement supérieures à celles d'une carte à puce. La puissance d'un processeur et la capacité de la mémoire vive ou de la mémoire persistante ROM (Read Only Memory) sont fonction de la surface de silicium encarté. Les cartes à puce devant d'une part respecter des contraintes mécaniques, en particulier la torsion et la flexion, et d'autre part garantir une durée de vie raisonnable, leur surface de silicium ne dépasse généralement pas 25 mm2. La mémoire d'une carte à puce a typiquement une capacité d'environ 8 kilo-octets, par conséquent bien inférieure à la capacité de RAM dont dispose l'ordinateur PC le moins performant proposé actuellement sur le marché.
Il existe plusieurs solutions permettant de vérifier le bytecode dans des dispositifs dont la capacité de mémoire est très limitée.
L'une de ces approches consiste à ajouter au code le résultat d'un algorithme de pré-calcul qui sera ensuite repris par le vérifieur du bytecode. Il peut s'agir par exemple de la méthode PCC (Proof Carrying Code) ou d'une variante de cette dernière qui permet au vérifieur encarté d'utiliser des algorithmes plus simples. Un programme, tel qu'un applet Java quelconque, ne comprennent pas le code supplémentaire PCC, ne pourra donc pas être vérifié par le microcircuit. La sphère d'utilisation des microcircuits utilisant ces méthodes est donc limitée.
Une autre approche consiste à modifier le code intermédiaire du programme à vérifier à l'extérieur du dispositif de telle sorte que le procédé de vérification soit plus aisé sans entraîner pour autant une diminution de fiabilité, telle que décrite dans la demande de brevet internationale WO 0114958 A2. Dans cette demande, on décrit un procédé de vérification d'un programme de type Java dans lequel l'on modifie le code intermédiaire par un procédé dit "de normalisation" dans un système de traitement de données externe avant de transférer ce code modifié dans un système embarqué. Lors de cette normalisation, le registre réel des types est réalloué à un registre virtuel, chaque case de ce registre ne définissant qu'un type, c'est-à-dire que le registre virtuel est monomorphe. Cette modification permet donc de réduire fortement la consommation en mémoire nécessaire pour stocker les différents types d'un registre polymorphe lors du procédé de vérification. Si le procédé de vérification de ce code modifié se termine avec succès, le code modifié est ensuite exécuté par le système embarqué. L'un des désavantages de ce procédé est que l'on ne peut pas être absolument sûr que le code modifié dans le système externe correspond au code original et sera exécuté correctement par le système embarqué. D'autre part, le fait d'exécuter un code modifié selon le procédé décrit dans la demande de brevet précitée, limite l'utilisation de certaines techniques d'optimisation de calcul du programme.
De manière générale, les procédés conventionnels de vérification du code intermédiaire (bytecode) Java destinés à être utilisés dans des microcircuits à ressources limitées peuvent également avoir les inconvénients d'augmenter la quantité d'informations à transmettre au microcircuit, de nécessiter 1' implémentation et l'exécution d'un logiciel relativement complexe dans le système informatique externe en communication avec la carte à puce, ou de limiter l'utilisation de certaines techniques d'optimisation de calcul du programme.
Tenant compte de ce qui précède, l'un des objectifs de l'invention est de fournir un procédé de vérification de code intermédiaire destiné à être exécuté dans un objet à microcircuit à ressources limitées, fiable et économe en termes d'occupation des ressources de mémoire du microcircuit, notamment la mémoire volatile ou d'autres mémoires accessibles en écriture et lecture du microcircuit .
Il est avantageux de fournir un procédé de vérification destiné à être exécuté dans un objet à microcircuit à ressources limitées qui ne compromet pas l'exécution du code intermédiaire et qui ne limite pas l'utilisation des techniques d'optimisation de calcul du code intermédiaire.
Il est avantageux de fournir un procédé de vérification destiné à être exécuté dans un objet à microcircuit à ressources limitées, ayant un large spectre d'utilisation pour une plateforme donné, tel que le Java ou des variantes telles que le Javacard.
Il est en outre avantageux de réduire l'utilisation des ressources de calculs du microcircuit de l'objet. II est également avantageux de réduire le temps nécessaire pour effectuer la vérification d'un programme à vérifier. Des buts de l'invention sont réalisés par un procède selon la revendication 1.
Dans la présente invention, un procédé de vérification de codes intermédiaires exécutable par un microcircuit à ressources limitées connecté à un système de traitement de données externe, comporte une étape de modification du code intermédiaire comprenant la réallocation de registres réels de types a des registres virtuels de types monomorphes, et de construction d'un code réalloué dont les instructions font référence aux registres virtuels, et une étape de vérification du code réalloué dans le microcircuit a ressources limitées, caractérisée en ce que, en cas de succès de la vérification du code réalloue dans le microcircuit, l'on installe le code intermédiaire original dans le microcircuit à ressources limitées pour exécution.
Dans une première forme d'exécution, la modification du code intermédiaire original peut être effectuée dans un système de traitement de données externe avant son chargement dans le microcircuit à ressources limitées, la modification comprenant la génération d'un composant de réallocation incluant un tableau de réallocation définissant la réallocation des données du type d'un registre réel à des données du type d'un registre virtuel monomorphe. Dans cette forme d'exécution, le procédé de vérification comprend la vérification du composant de réallocation et, en cas de succès, la vérification du code réalloué, le code réalloué étant construit soit lors du procédé de vérification du composant de réallocation, soit après vérification du composant de réallocation. Si la vérification du code réalloué se termine avec succès, le bytecode original est installé pour exécution, le bytecode original étant soit stocké dans une mémoire persistante accessible en lecture et en écriture du microcircuit, soit chargé depuis le système externe. Dans ce dernier cas, afin d'assurer que le bytecode original installé depuis le système externe correspond au code original qui a été vérifié lors du premier chargement du bytecode original, un calcul de hachage du code intermédiaire original est effectué et comparé avec le résultat du calcul de hachage du code intermédiaire original à réinstaller après le procédé de vérification.
Dans une autre forme d'exécution, les étapes de calcul de la réallocation et de la construction du code réalloué peuvent être effectuées dans le microcircuit à ressources limitées, le code intermédiaire original étant chargé dans le microcircuit avant l'exécution du procédé de vérification et stocké dans une mémoire du microcircuit, par exemple dans une mémoire persistante accessible en lecture et en écriture, du type EEPROM (Electrical Erasable Programmable Read Only Memory) .
Avantageusement, la génération d'un code réalloué pour vérification permet de générer un registre du type monomorphe réduisant la consommation de la mémoire volatile du microcircuit lors de la vérification du code intermédiaire. L'installation du code intermédiaire original pour exécution, après le procédé de vérification, permet toutefois d'éviter des problèmes éventuels liés à l'exécution d'un code intermédiaire modifié et permet également l'utilisation de techniques de calcul optimisées.
D'autres caractéristiques avantageuses de l'invention ressortiront des revendications, de la description détaillée de formes d'exécution de l'invention donnée ci-après et des dessins annexés, dans lesquels : la Fig. 1 montre un organigramme illustrant l'enchaînement des étapes d'un procédé de vérification d'un code intermédiaire selon une première forme d'exécution de l'invention; la Fig. 2 est une représentation simplifiée d'instructions du code intermédiaire (bytecode) et d'un tableau de réallocation associé aux instructions du code intermédiaire ; la Fig. 3 est une représentation simplifiée d'un exemple de code intermédiaire avec son tableau de réallocation selon une forme d'exécution de l'invention; la Fig. 4 montre un organigramme illustrant l'enchaînement des étapes pendant le procédé de vérification du tableau de réallocation; la Fig. 5 est une représentation simplifiée de l'affectation et de la mise à jour du tableau de réallocation courante pour une instruction du code intermédiaire et du type " def r", qui est une instruction définissant une valeur dans le registre réel associé à l'instruction; la Fig. 6 est une représentation simplifiée de l'affectation et de la mise à jour du tableau de réallocation courante pour une instruction du type " use r ", qui est une instruction utilisant une valeur r dans un registre associé à l'instruction courante; la Fig. 7 est une représentation simplifiée de l'affectation et de la mise a jour du tableau de réallocation courante pour une instruction du code intermédiaire du type "jbrc-h", qui est une instruction de branchement à au moins deux instructions; la Fig. 8 est une représentation simplifiée de l'affectation et de la mise à jour du tableau de réallocation courante pour une instruction du type " nop" , qui est une instruction qui ne comporte pas d'opération sur le registre associé à l'instruction courante; la Fig. 9 est une représentation simplifiée de l'affectation et de la mise à jour du tableau de réallocation courante pour une instruction du type " return" ; la Fig. 10 montre un organigramme illustrant l'enchaînement des étapes dans un procédé de vérification de code intermédiaire selon une deuxième forme d'exécution de l'invention.
Faisant référence à la Fig. 1, les étapes d'un procédé de vérification d'un code intermédiaire, tel qu'un bytecode Java ou Javacard, selon une première forme d'exécution de l'invention, sont montrées. Un microcircuit à ressources limitées notamment pour un système embarqué tel qu'une carte à puce, est connecté à un système de traitement de données externe (ci-après "système externe") pour le chargement et l'exécution d'un programme tel qu'un applet Java, ou Javacard, dans le microcircuit. Le système externe effectue la compilation et la conversion du programme Java en un fichier . cap, c'est-à-dire le code intermédiaire (bytecode) exécutable par le microcircuit. Dans cette première forme d'exécution, l'on ajoute au code intermédiaire original un composant de réallocation comprenant un tableau de réallocation T, tel que montré dans les Figures 2 et 3. Ce composant de réallocation est généré par le système externe par une méthode du calcul de réallocation connue, telle que la méthode de "coloration de graph".
Le calcul de réallocation par coloration de graph est bien connu en tant que tel et est utilisé par exemple dans le procédé de vérification décrit dans la demande internationale WO 0114958 A2. Toutefois, dans la demande précitée, le code intermédiaire original est modifié par un procédé dit de "normalisation", Ainsi, d'une part, les instructions du code intermédiaire et le registre sont modifiés, de sorte que le registre est monomorphe, c'est- à-dire que chaque registre ne reçoit des données représentant un seul type et, d'autre part, à chaque instruction de branchement, la pile est vide. Cette transformation permet de rendre le procédé de vérification linéaire et d'éviter la forte consommation en mémoire volatile (RAM) que nécessite le stockage de registres pouvant accepter des données représentant différents types, c'est-à-dire les registres polymorphes. Dans la méthode connue précitée, le bytecode Java ainsi modifié est utilisé pour l'exécution du programme après vérification. L'exécution du code modifié peut d'une part avoir des conséquences sur la fiabilité de l'exécution, d'autre part elle limite les possibilités d'utiliser les techniques d'optimisation connues du bytecode Java, utilisées par exemple pour réduire le temps d'exécution ou le temps de communication avec le système externe.
Dans la présente invention, le code intermédiaire (bytecode) original ainsi que le composant de réallocation est chargé dans le microcircuit à ressources limitées. Le code intermédiaire original est stocké en mémoire du microcircuit, par exemple dans une mémoire persistante accessible en écriture et en lecture de type EEPROM et le composant de réallocation est chargé dans une mémoire volatile (RAM) du microcircuit. Après chargement, le composant de réallocation est vérifié
(étape 110) et, en cas de succès, l'on procède à la construction du code réalloué (étape 112) et finalement à une étape de vérification du code réalloué (étape 114) avant l'installation du code intermédiaire original stocké dans la mémoire persistante (étape 116) pour exécution. En cas d'échec du procédé de vérification du composant de réallocation ou du procédé de vérification du code réalloué, le code intermédiaire est rejeté et n'est pas installé pour exécution. Il est à remarquer que la construction du code réalloué peut être effectuée lors du procédé de vérification du composant de réallocation, c'est-à-dire que les étapes 110 et 112 peuvent être confondues .
La procédure de vérification du composant de réallocation sera décrite plus en détail ci-après, en faisant référence aux Figures 2 à 9: La Fig. 2 montre, de manière simplifiée, une série d'instructions PC du code intermédiaire ainsi qu'un composant de réallocation T du registre réel de données de type. Les instructions du code intermédiaire peuvent être classées parmi les cinq classes d'instructions suivantes en fonction de leur effet sur la réallocation du registre de données de type correspondant.
" def x" : On définit la valeur de la variable x dans le registre (par exemple les instructions " ss tore" , " astore" ) " use x" : On utilise la variable x dans le registre (par exemple les instructions " sload" , " aload" )
"nop" : On n'effectue aucune opération sur les valeurs du registre (par exemple les instructions " sxor" , " iadd" ) " return" : On sort de la méthode (par exemple les instructions " areturn" , " sreturn" ) "brch x y : On branche à des instructions cibles x ou y (par exemple les instructions " î feq" , " if- scmpeq" )
Faisant référence plus particulièrement aux Figures 2 et 3, le composant de réallocation T comprend un sous- tableau D contenant la réallocation pour chaque instruction qui définit le type d'une variable x dans le registre rx, c'est-à-dire une instruction de la classe " def x", et un tableau de réallocation F ayant le même nombre de colonnes k que de registres réels et le même nombre de lignes S que d'instructions PC. Le tableau F est un tableau résultant de la réallocation des registres réels de données de type rx à des registres virtuels vy . Chaque registre rx de même type est réalloué à un seul registre virtuel vy correspondant à ce type. Les registres réels dont le type peut changer, c'est-à-dire les registres polymorphes, sont réalloués à différents registres virtuels correspondants aux différents types de ces registres. Comme chaque registre virtuel ne définit qu'un seul type, les registres virtuels sont monomorphes, c'est-à-dire les variables pour lesquelles il existe un type restent valables tout au long du procédé de vérification du code intermédiaire. L'algorithme de vérification 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 procédure de vérification. Il s'agit en fait d'un calcul de point fixe où le type des variables est spécialisé jusqu'à ce qu'il reste inchangé. Un tel algorithme échoue si on lui présente des variables polymorphes comme étant des variables monomorphes. Le procédé de vérification du composant de réallocation 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 à l'évolution de la réallocation courante lors de la vérification du composant de réallocation T. Le tableau courant F' peut donc être représenté par une seule ligne et un nombre de colonnes égal au nombre k de registres réels. Au début du procédé de vérification, c'est-à-dire à l'instruction PCi, les données du tableau de réallocation courante sont mitialisées (étape 402 de la Fig. 4) avec le type "nul", telles que montrées dans la Fig. 3, qui est le plus petit élément du treillis des types, au lieu du type " top " qui réunit tous les types, c'est-à-dire le plus grand élément du treillis des types. On lit ensuite la première instruction (étape 404 de la Fig. 4) et en fonction de la classe d'instruction du code intermédiaire, l'on effectue une vérification suivie par une mise à jour du tableau de réallocation courante F' ou simplement une mise à jour du tableau de réallocation courante .
Pour les instructions sans opération sur le registre "nop" et de retour " ret urn " , l'algorithme de vérification effectue simplement une mise à jour du tableau de réallocation (étapes 412 respectivement 414 de la Fig. 4), telle que montrée dans les Figures 8 respectivement 9. Dans le cas d'une instruction de type " nop" , la mise à jour consiste simplement en un report des données de type (f'α, i) dans le tableau de réallocation courante, c'est- à-dire que les données de type sont conservées sans changement pour la prochaine instruction PC +ι . Dans le cas d'une instruction de classe "return", la mise à our consiste en l'affectation des données de type (f' +ι,ι) du sous-tableau de réallocation F de l'instruction suivante PC +ι dans le tableau de réallocation courante F', telle que montrée dans la Fig. 9. Dans le cas d'une instruction de définition " def" , l'on affecte les données de type (dα) dans le sous- tableau D contenant la réallocation pour l'instruction ( PC ) en question, au registre correspondant du tableau de réallocation courante F', c'est-à-dire si l'instruction courante PC définit la valeur d'un registre ( f ,x) la réallocation (dα=vy) définie dans le tableau D est affectée et met à jour le registre ( f , x) du tableau de réallocation courante F'. Lors de cette mise à jour, les autres valeurs ( f , λ à -f' , λ-ι et f , x+1 à f , k) du tableau de réallocation courante sont conservées, telles que montrées dans la Fig. 5.
Si l'instruction est de classe " use rx", l'algorithme de vérification vérifie simplement si la valeur du registre correspondant (la colonne x) du tableau de réallocation courante F' n'est pas égale à la valeur " nul " , qui est la plus petite valeur du treillis des types. La mise à jour pour cette instruction est simplement la conservation des données de type ( f , A du tableau de réallocation courante F', telle que montrée à la Fig. 6.
Dans le cas d'une instruction de branchement, la vérification consiste à comparer les données de type ( f , 2 ) dans le tableau dans le tableau de réallocation courante F' correspondant à l'instruction courante PCα avec les données de type ( f r ι ) du tableau de réallocation F aux instructions cibles PCβ et PCγ et, en cas d'inégalité, la procédure de vérification se termine avec un échec. Le tableau de réallocation courante F' est ensuite mis à jour en affectant les données de type du tableau de réallocation F à 1 ' instruction suivante PCα+ι au tableau de réallocation courante F'. La prochaine étape (416) consiste à vérifier s'il reste encore des instructions à lire et, dans l'affirmative, d' incrémenter le pointeur de l'instruction courante (étape 418) et de répéter la boucle de lecture de l'instruction (étape 414) et de vérification et de mise à jour de la réallocation courante jusqu'à ce qu'il n'y ait plus d'instructions à lire. Le programme de vérification passe ensuite à l'étape de construction du code réalloué (étape 112) et à la vérification du code réalloué (étape 114). La vérification du code réalloué suit les procédés de vérification connus. Il est toutefois à remarquer que le code réalloué peut être construit lors de la vérification du composant de réallocation (étape 110) en chanqeant la variable sur laquelle agit l'instruction à sa valeur réallouée. Par exemple, si une instruction de définition " def ' (voir Fig. 3) agit sur le registre r! qui est réalloué au registre virtuel vl r alors l'instruction du code réalloué devient " def v ', de sorte qu'elle agit sur le registre virtuel de données de type au lieu du registre réel de données de type original.
On constate donc que les instructions sont lues linéairement de la première à la dernière instruction, chaque instruction étant exécutée par l'interpréteur de type . Pour les instructions d'utilisation d'une variable ( " use" ) , sans opération sur les registres ( " nop" ) ou de retour ("return"), le comportement de l'algorithme de vérification est similaire à celui d'un vérifieur conventionnel .
Cependant on doit garantir lors d'une instruction d'utilisation " use x" que la variable "x" sur laquelle agit cette instruction a été bien définie auparavant, alors que la variable peut avoir été initialisée dans une autre branche du programme avant cette instruction. Ce problème est résolu en vérifiant que la valeur stockée dans le sous-tableau D pour une instruction de définition " def x" spécialise le type précédent de la variable x dans le tableau de réallocation courante F'. Pour cette raison il est important qu'au début du programme, les variables du tableau F' sont initialisées à "n ul " pour leur permettre d'être spécialisées. On remarque que sur une instruction de branchement "brch" , l'algorithme de vérification n'effectue aucun changement au tableau de réallocation courante F' et avance d'une instruction.
Une fois arrivé à la fin du code intermédiaire, le programme recommence au début jusqu'à ce que le type de chaque variable reste inchangé. L'algorithme de vérification échoue quand on lui présente un code avec des variables non monomorphes, car il vérifie sur les instructions de définition " def" que les données de type dans le sous-tableau D spécialisent le type déjà présent dans le tableau de réallocation courante F'. Un code qui passe la vérification monomorphe et initialise les données de type de ses variables doit être correctement typé, puisque chaque registre virtuel ( v ) ne peut contenir qu'un seul type. En d'autres mots,
1 ' interpréteur de types vérifie que toutes les utilisations possibles d'une variable sont conformes avec son type et ceci est donc assuré par le fait que les opérations des instructions PC sur le tableau de réallocation F passent une vérification monomorphe.
Une réallocation est valide si dans le code intermédiaire original, toute instruction d'utilisation " use x" utilise la même réallocation que toutes les instructions de définition " def x" qui ont pu la définir. C'est à dire que dans le code généré pour la vérification, si une instruction " use x" s'est transformée en " use y", alors l'instruction " def x" s'est transformée en " def y".
La validité de la proposition précédente peut être démontrée par un raisonnement par l'absurde. Soit une réallocation non valide pour laquelle l'algorithme se termine sur la fin du code. Si la réallocation n'est pas valide, il existe alors une instruction " use x" dans le champ d'une instruction " def x" pour laquelle la réallocation de la variable x est la variable z, alors que la réallocation de la variable x pour l'instruction " def x" est la variable y, où la variable y est différente de la variable z. Il existe une séquence d'instructions du code intermédiaire original " def x", "i-i", " i -2" , ...," i -k" , " use x" qui conduit de l'instruction " def x" à " use x" par un flot d'exécutions correctes. Il n'y a pas d'autre instruction " def x" à l'intérieur de la séquence, sinon ce serait elle qui définit l'instruction "use x" . Toutes les autres instructions préservent la réallocation courante du registre x lors du déroulement de l'algorithme. En effet, les instructions "nop" , " return " et "use" ne changent pas la réallocation courante et 1 ' instruction de branchement "brch" s'assure que la réallocation après le branchement est la même que celle avant. La séquence d'instructions précitée est donc en contradiction avec la proposition par l'absurde, ce qui démontre la validité de la proposition initiale, objet de la démonstration. On peut également démontrer par le raisonnement suivant que si un code intermédiaire, généré à partir d'un code intermédiaire original et de son tableau de réallocation valide, passe un procédé de vérification, alors le code intermédiaire original passe aussi le procédé de vérification. Supposons que dans le procédé de vérification du code intermédiaire on stocke en mémoire volatile (RAM) les types des variables pour chaque cible de branchement ainsi qu'un tableau courant et une liste de travail. Les tableaux sont initialisés avec le type " top" , le plus grand élément du treillis des types. Le tableau courant est également initialisé avec le type " top" pour chaque variable non paramétrée et avec les types de la signature pour les variables paramétrées . L'algorithme de vérification commence avec l'instruction associée au point d'entrée de la méthode dans la liste de travail. On enlève la première instruction de la liste de travail. On calcule le nouveau tableau courant après l'exécution de cette instruction à partir de l'interpréteur de type et on l'unifie à tous les tableaux qui correspondent aux instructions qui peuvent succéder. On rajoute à la table de travail les instructions dont les tableaux ont changé. Le code intermédiaire est vérifié avec succès si l'on aboutit à une liste de travail vide. Le procédé de vérification rejet un algorithme si une unification de types est impossible ou si l'interpréteur de types rencontre une instruction incompatible avec les données de type dans le tableau des registres . En prenant une étape quelconque de la vérification du code intermédiaire original, l'on a comme hypothèse que la vérification s'est bien déroulée jusqu'à présent, en on a à disposition le tableau courant et le contenu des registres. On part aussi de l'hypothèse que l'étape correspondante de la vérification du code intermédiaire avec réallocation se déroule bien et on sait que la réallocation est valide. Pour terminer cette démonstration, on distingue plusieurs cas selon l'instruction en cours :
"nop" : L'instruction ne concerne pas les variables, on avance à l'instruction suivante sans rien modifier. Le procédé de vérification ne peut pas échouer sur une instruction " nop" . " def x" : Mise à jour du tableau courant avec le nouveau type. Le procédé de vérification ne peut pas échouer sur un " def" car il prend un argument dans la pile, mais on n'est pas concerné par les types dans la pile. "return" : La vérification se poursuit normalement. Le procédé de vérification ne peut pas échouer ici .
" use x" : Le procédé de vérification peut échouer si l'interpréteur de type décide que le type de la variable x n'est pas compatible avec son utilisation. La validité de la réallocation nous assure que la réallocation de la variable x n'a pas changé entre cette instruction "use" et les instructions "def" qui lui correspondent. Comme la vérification du code réalloué a réussi jusqu'ici, le type de la variable x est compatible avec son utilisation. Donc, le procédé de vérification passe avec succès sur l'instruction.
"brch x y" : Le procédé de vérification peut échouer dans l'unification du tableau courant avec celui correspondant au registre x ou avec celui correspondant au registre y. Or, la validité de la réallocation nous assure que la réallocation courante au moment de l'instruction de branchement "brch" est la même que celle en x et en y. De plus, la vérification du code réalloué réussit pour cette instruction, la vérification réussit donc aussi pour le code intermédiaire non réalloué . En ce qui concerne le traitement des exceptions dans le code intermédiaire, si l'on se trouve sur une partie de code protégée par un "handler" d'exception, chaque instruction doit être considérée comme un branchement potentiel vers la portion de code intermédiaire qui traite l'exception, c'est à dire que la réallocation courante doit être la même que celle donnée dans le tableau de réallocation de l'exception. Si ce traitement des exceptions permet d'assurer la correction du typage, il est par contre trop restrictif dans le sens où il ne permet pas de changer la réallocation d'une variable à l'intérieur d'un bloc protégé par un même handler d'exception. Exemple :
PC 1 : def ri comme entier: réallocation j→ vι
PC 2 : def rλ comme référence: réallocation r7→ v2 Si les deux instructions " def" sont protégées par le même "handler" d'exception et que la variable rt n'est pas utilisée dans le traitement de l'exception, alors le typage est respecte, mais l'algorithme de vérification du tableau de réallocation échoue car la variable r! ne peut avoir qu'une seule réallocation à l'entrée du traitement de l'exception. La solution est de créer un registre factice (appelons le Top) qui interdit l'utilisation du registre réel réalloué en Top. Dans l'exemple, il suffit de reallouer à Top le registre r2 dans le tableau de réallocation du traitement de l'exception. Une réallocation a Top se transmet par les branchements et peut apparaître dans un tableau de réallocation qu correspond au début du traitement d'une exception.
En ce qui concerne les appels de sous-routines, on doit tenir compte du fait qu'elles font perdre le lien entre les instructions " use" et les instructions " def" des variables. Pour rendre compatible les réallocations avec les appels de sous-routines JSR/RET, il faut ajouter un système de contexte de réallocation.
En faisant référence à la Fig. 10, dans une deuxième forme d'exécution de l'invention, le calcul de la réallocation et du code realloue (étape 1010) est effectue entièrement dans le microcircuit a ressources limitées, suivi d'une étape 1012 de vérification du code realloué dans le microcircuit et, en cas de succès, l'installation du code intermédiaire original pour exécution (étape 1016) . Le calcul de la réallocation et du code réalloué dans le microcircuit peut être effectué selon les méthodes connues, toutefois sans qu'il soit nécessaire d'effectuer une optimisation du code réalloué du fait qu'il n'est pas utilisé pour l'exécution, mais uniquement pour la vérification de l'intégrité et de l'innocuité du code intermédiaire.
Le code intermédiaire peut soit être stocké en mémoire persistante accessible en écriture et en lecture, par exemple de type EEPROM, lors du premier chargement depuis le système externe, soit être réinstallé après vérification, en appliquant une fonction de hachage au premier chargement, en stockant le résultant dans une mémoire du microcircuit et en le comparant avec la valeur de hachage calculée à partir du code intermédiaire chargé après vérification.

Claims

Revendications
1. Procédé de vérification de code intermédiaire exécutable par un microcircuit à ressources limitées connecté à un système de traitement de données externe, comportant une étape de modification du code intermédiaire comprenant la réallocation des registres réels de type r à des registres virtuels v de type monomorphe, et de construction d'un code réalloué dont les instructions PC font référence aux registres virtuels v, et une étape de vérification du code réalloué dans le microcircuit à ressources limitées, caractérisé en ce que, en cas de succès de la vérification du code réalloué dans le microcircuit, l'on installe le code intermédiaire original dans le microcircuit à ressources limitées pour exécution .
2. Procédé selon la revendication 1, caractérisé en ce que l'étape de la construction du code réalloué est effectuée dans le microcircuit à ressources limitées.
3. Procédé selon l'une des revendications précédentes, caractérisé en ce que le code intermédiaire original est chargé dans le microcircuit à ressources limitées avant l'exécution du procédé de vérification et stocké dans une mémoire du microcircuit.
4. Procédé selon l'une des revendications précédentes, caractérisé en ce que, dans l'étape de modification du code intermédiaire, l'on crée un composant de réallocation T définissant la réallocation des registres réels de type aux registres virtuels monomorphes.
5. Procédé selon la revendication précédente, caractérisé en ce que le composant de réallocation T contient un sous-tableau de réallocation D contenant la réallocation pour chaque instruction de définition " def" du code intermédiaire définissant le type d'une variable dans un des registres réels, et un tableau de réallocation F contenant la réallocation des registres réels de type aux registres virtuels monomorphes.
6. Procédé selon la revendication précédente, caractérisé en ce que, lors du procédé de vérification du composant de réallocation T, l'on vérifie si le sous- tableau de réallocation D pour les instructions de définition " def" comporte une valeur de réallocation et, s'il ne comporte pas de valeur de réallocation, le code intermédiaire est rejeté.
7. Procédé selon l'une des revendications précédentes, caractérisé en ce que, lors du procédé de vérification du tableau de réallocation F, pour une instruction du code intermédiaire qui utilise une variable, l'on vérifie si la variable utilisée dans le tableau de réallocation courante n'est pas "n ul " et, si elle est " nul " , le code intermédiaire est rejeté.
8. Procédé selon l'une des revendications précédentes, caractérisé en ce que, lors du procédé de vérification du tableau de réallocation dans le cadre d'une instruction de branchement "brch" à des instructions cibles, l'on vérifie l'identité du tableau de réallocation courante F' avec les lignes du tableau de réallocation F correspondant aux instructions cibles et, en cas de différences, le code intermédiaire est rejeté.
9. Procédé selon l'une des revendications 1 à 3, caractérisé en ce que l'étape de modification du code intermédiaire est effectuée dans le microcircuit à ressources limitées.
PCT/EP2003/050193 2002-05-27 2003-05-23 Procédé de vérification de codes pour microcircuits à ressources limitées Ceased WO2003100607A2 (fr)

Priority Applications (4)

Application Number Priority Date Filing Date Title
US10/515,375 US20050252977A1 (en) 2002-05-27 2003-05-23 Code verification method for limited resource microcircuits
AU2003238085A AU2003238085A1 (en) 2002-05-27 2003-05-23 Code verification method for limited resource microcircuits
EP03735717A EP1512071B1 (fr) 2002-05-27 2003-05-23 Procede de verification de codes pour microcircuits a ressources limitees
DE60317324T DE60317324D1 (de) 2002-05-27 2003-05-23 Verfahren zum prüfen von codes für mikroschaltungen mit eingeschränkten ressourcen

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
FR0206445A FR2840084A1 (fr) 2002-05-27 2002-05-27 Procede de verification de codes pour microcircuits a ressources limitees
FR02/06445 2002-05-27

Publications (2)

Publication Number Publication Date
WO2003100607A2 true WO2003100607A2 (fr) 2003-12-04
WO2003100607A3 WO2003100607A3 (fr) 2004-02-19

Family

ID=29415115

Family Applications (1)

Application Number Title Priority Date Filing Date
PCT/EP2003/050193 Ceased WO2003100607A2 (fr) 2002-05-27 2003-05-23 Procédé de vérification de codes pour microcircuits à ressources limitées

Country Status (8)

Country Link
US (1) US20050252977A1 (fr)
EP (1) EP1512071B1 (fr)
CN (1) CN1672130A (fr)
AT (1) ATE377791T1 (fr)
AU (1) AU2003238085A1 (fr)
DE (1) DE60317324D1 (fr)
FR (1) FR2840084A1 (fr)
WO (1) WO2003100607A2 (fr)

Families Citing this family (6)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
FR2884994A1 (fr) 2005-04-22 2006-10-27 Gemplus Sa Procede de verification de pseudo-code charge dans un systeme embarque, notamment une carte a puce
US8200983B1 (en) * 2006-09-09 2012-06-12 9Rays.Net, Inc. System and method for tamper-proofing executable binary assemblies
JP2013138409A (ja) * 2011-11-30 2013-07-11 Canon Inc 情報処理装置およびその方法
EP2782006B1 (fr) * 2013-03-19 2018-06-13 Nxp B.V. Procédé et système permettant de vérifier un programme informatique sur une carte à puce
US10261764B2 (en) * 2014-05-13 2019-04-16 Oracle International Corporation Handling value types
US11416273B2 (en) 2020-01-16 2022-08-16 Red Hat, Inc. Adaptive and secure bitecode injection based on comparison with previously stored bytecode

Family Cites Families (10)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US5748964A (en) * 1994-12-20 1998-05-05 Sun Microsystems, Inc. Bytecode program interpreter apparatus and method with pre-verification of data type restrictions
ES2184066T3 (es) * 1996-10-25 2003-04-01 Schlumberger Systems & Service Uso de un lenguaje de programacion de alto nivel con microcontrolador.
US6092147A (en) * 1997-04-15 2000-07-18 Sun Microsystems, Inc. Virtual machine with securely distributed bytecode verification
FR2795835B1 (fr) * 1999-07-01 2001-10-05 Bull Cp8 Procede de verification de transformateurs de codes pour un systeme embarque, notamment sur une carte a puce
FR2797963B1 (fr) * 1999-08-23 2002-11-29 Trusted Logic Protocole de gestion, procede de verification et de transformation d'un fragment de programme telecharge et systemes correspondants
US6560774B1 (en) * 1999-09-01 2003-05-06 Microsoft Corporation Verifier to check intermediate language
US6763463B1 (en) * 1999-11-05 2004-07-13 Microsoft Corporation Integrated circuit card with data modifying capabilities and related methods
US6981245B1 (en) * 2000-09-14 2005-12-27 Sun Microsystems, Inc. Populating binary compatible resource-constrained devices with content verified using API definitions
US7506175B2 (en) * 2000-11-06 2009-03-17 International Business Machines Corporation File language verification
EP1207454A1 (fr) * 2000-11-15 2002-05-22 International Business Machines Corporation Système de temps d'exécution pour Java avec identificateurs de liaison modifiés

Also Published As

Publication number Publication date
FR2840084A1 (fr) 2003-11-28
DE60317324D1 (de) 2007-12-20
CN1672130A (zh) 2005-09-21
EP1512071A2 (fr) 2005-03-09
AU2003238085A1 (en) 2003-12-12
ATE377791T1 (de) 2007-11-15
EP1512071B1 (fr) 2007-11-07
WO2003100607A3 (fr) 2004-02-19
US20050252977A1 (en) 2005-11-17

Similar Documents

Publication Publication Date Title
EP1212678B1 (fr) Protocole de gestion, procede de verification et de transformation d'un fragment de programme telecharge et systemes correspondants
US7191288B2 (en) Method and apparatus for providing an application on a smart card
FR2790844A1 (fr) Procede et dispositif de surveillance du deroulement d'un programme, dispositif programme permettant la surveillance de son programme
EP2453356B1 (fr) Procédé, programme d'ordinateur et dispositif de sécurisation de code intermédiaire de programmation pour son exécution par une machine virtuelle
EP2565810A1 (fr) Microprocesseur protégé contre le vidage de mémoire
WO2003010666A1 (fr) Procede pour la compression d'un code interprete par analyse semantique
EP1512071B1 (fr) Procede de verification de codes pour microcircuits a ressources limitees
WO2015091511A1 (fr) Authentification de code binaire
EP1782191B1 (fr) Procede de chargement d'un logiciel en langage intermediaire oriente objet dans un appareil portatif
EP1700218A2 (fr) Procede de determination de caracteristiques operationnelles d'un programme
FR2833374A1 (fr) Procede et dispositif de controle d'acces dans un systeme embarque
EP1960934B1 (fr) Procede pour securiser l'execution d'un code logiciel en langage intermediaire dans un appareil portatif
EP1344137A1 (fr) Procede et dispositif de securisation d'un traitement de donnees
FR2795835A1 (fr) Procede de verification de transformateurs de codes pour un systeme embarque, notamment sur une carte a puce
WO2003027851A1 (fr) Procede et dispositif de verifieur de code optimise
FR2867929A1 (fr) Procede d'authentification dynamique de programmes par un objet portable electronique
FR2814557A1 (fr) Protection contre l'exploitation abusive d'une instruction dans une memoire
CN116091056A (zh) 基于u盾的交易方法、装置、计算机存储介质及电子设备
WO2008125479A1 (fr) Procédé d'exécution sécurisée d'une application
EP2252978B1 (fr) Carte a circuit integre ayant un programme d'exploitation modifiable et procede de modification correspondant
EP3514749B1 (fr) Procede de controle de regles de dependances d'objets mis a jour dans un microcircuit, et dispositif correspondant
FR2854261A1 (fr) Procede d'execution d'une application logicielle par l'intermediaire d'un programme d'amorce logicielle et architecture informatique pour la mise en oeuvre du procede
FR2829847A1 (fr) Procede de controle d'acces a des ressources partagees dans un systeme embarque et systeme embarque pour la mise en oeuvre d'un tel procede
EP3203405B1 (fr) Procede d'execution d'instructions d'applications orientees objet par un interpreteur
FR2832821A1 (fr) Procede de verification de codes pour microcircuits a ressources limitees

Legal Events

Date Code Title Description
AK Designated states

Kind code of ref document: A2

Designated state(s): AE AG AL AM AT AU AZ BA BB BG BR BY BZ CA CH CN CO CR CU CZ DE DK DM DZ EC EE ES FI GB GD GE GH GM HR HU ID IL IN IS JP KE KG KP KR KZ LC LK LR LS LT LU LV MA MD MG MK MN MW MX MZ NI NO NZ OM PH PL PT RO RU SC SD SE SG SK SL TJ TM TN TR TT TZ UA UG US UZ VC VN YU ZA ZM ZW

AL Designated countries for regional patents

Kind code of ref document: A2

Designated state(s): GH GM KE LS MW MZ SD SL SZ TZ UG ZM ZW AM AZ BY KG KZ MD RU TJ TM AT BE BG CH CY CZ DE DK EE ES FI FR GB GR HU IE IT LU MC NL PT RO SE SI SK TR BF BJ CF CG CI CM GA GN GQ GW ML MR NE SN TD TG

121 Ep: the epo has been informed by wipo that ep was designated in this application
DFPE Request for preliminary examination filed prior to expiration of 19th month from priority date (pct application filed before 20040101)
WWE Wipo information: entry into national phase

Ref document number: 2003735717

Country of ref document: EP

WWE Wipo information: entry into national phase

Ref document number: 20038179695

Country of ref document: CN

WWP Wipo information: published in national office

Ref document number: 2003735717

Country of ref document: EP

WWE Wipo information: entry into national phase

Ref document number: 10515375

Country of ref document: US

NENP Non-entry into the national phase

Ref country code: JP

WWW Wipo information: withdrawn in national office

Country of ref document: JP

WWG Wipo information: grant in national office

Ref document number: 2003735717

Country of ref document: EP