| 摘要 |
<p>The invention concerns a method for verifying a transformer of source code into a transformed code designed for an incorporated system (7). The method comprises at least steps which consist in: determining a single virtual machine factoring the behaviour of said two codes (1, 3); determining for each of said source (1) and transformed (3) codes a plurality of functions called auxiliary functions representing residual differences between said source (1) and transformed (3) codes; and a step which consists in verifying a property of correspondence between the auxiliary functions, the code transformer (2) verification resulting from the latter step. The invention is particularly applicable to chip cards (7).</p> |
