Method for verifying code transformers for an incorporated system, in particular in a chip card
First Claim
1. A method for verifying transformation of a source code into a transformed code designed for an embedded system, said source and transformed codes being associated with virtual machines comprising:
- determining, for each of said source and transformed codes, a first common subset, constituting a single virtual machine that factors in the behavior of said source and transformed codes;
determining, for each of said source and transformed codes, a second subset constituted by a plurality of auxiliary functions used by said single virtual machine, said auxiliary functions representing residual differences between said source and transformed codes and parameterizing the single virtual machine;
associating said auxiliary functions in pairs, a first auxiliary function of each pair belonging to said second subset associated with said source code and a second auxiliary function of each pair belonging to said second subset associated with said transformed code;
verifying a given correspondence property between said auxiliary functions of all of said pairs; and
verifying that said transformation of the source code into a transformed code satisfies said given correspondence property.
3 Assignments
0 Petitions
Accused Products
Abstract
The invention relates to a method for verifying transformation (2) of a source code (1) into a transformed code (3) designed for an embedded system (7) such as in a smart card or other portable or mobile device including data processing resources. The method comprises at least the following steps: determining a single virtual machine that factors in the behavior of both of these codes (1, 3), determining for each source code (1) and transformed code (3) a plurality of auxiliary functions representing the residual differences between said source code (1) and transformed code (3), and a step for verifying a correspondence property between the auxiliary functions, the verification of the code transformation (2) being obtained from this last step.
-
Citations
11 Claims
-
1. A method for verifying transformation of a source code into a transformed code designed for an embedded system, said source and transformed codes being associated with virtual machines comprising:
-
determining, for each of said source and transformed codes, a first common subset, constituting a single virtual machine that factors in the behavior of said source and transformed codes; determining, for each of said source and transformed codes, a second subset constituted by a plurality of auxiliary functions used by said single virtual machine, said auxiliary functions representing residual differences between said source and transformed codes and parameterizing the single virtual machine; associating said auxiliary functions in pairs, a first auxiliary function of each pair belonging to said second subset associated with said source code and a second auxiliary function of each pair belonging to said second subset associated with said transformed code; verifying a given correspondence property between said auxiliary functions of all of said pairs; and verifying that said transformation of the source code into a transformed code satisfies said given correspondence property. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
-
Specification
-
- Resources
-
Current AssigneeCP8 Technologies (Thales SA)
-
Original AssigneeCP8 Technologies (Thales SA)
-
InventorsGoire, Christian, Jensen, Thomas, Le Metayer, Daniel, Fradet, Pascal, Denney, Ewen
-
Primary Examiner(s)Dam, Tuan
-
Assistant Examiner(s)RAMPURIA, SATISH
-
Application NumberUS09/786,114Time in Patent Office2,099 DaysField of Search717/109, 717139-148, 717/149, 717/137, 717/167, 717/154, 717/177, 717/153, 235/380, 235/492, 713/187, 713/193, 713/172, 713/200, 710/15, 702/189, 711/156, 711/154, 340/5.74, 707/103.RUS Class Current717/143CPC Class CodesG06F 8/52 Binary to binaryG06F 9/44589 Program code verification, ...
