METHOD FOR VERIFYING CODE TRANSFORMERS FOR AN INCORPORATED SYSTEM, IN PARTICULAR IN A CHIP CARD

摘要

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.