Patent ID: 7720939

Claim:
A method of verifying a program fragment downloaded onto a reprogrammable embedded system, equipped with a rewritable memory, a microprocessor and a virtual machine equipped with an execution stack and with operand registers, said program fragment consisting of an object code and including at least one subprogram consisting of a series of instructions manipulating said operand registers, said microprocessor and virtual machine configured to interpret said object code, said embedded system being interconnected to a reader, wherein subsequent to a detection of a downloading command and a storage of said object code in said rewritable memory, said method, for each subprogram, comprises: initializing a type stack and a table of register types through data representing a state of said virtual machine on initialization of an execution of said temporarily stored object code; carrying out a verification process of said temporarily stored object code instruction by instruction, by discerning an existence, for each current instruction, of a target, a branching-instruction target, a target of an exception-handler call or a target of a subroutine call, and, said current instruction being a target of a branching instruction, said verification process including verifying that said type stack is empty and rejecting said program fragment otherwise; verifying and updating an effect of said current instruction on the data types of said type stack and of said table of register types including: verifying that said type stack includes at least as many entries as said current instruction includes operands; unstacking and verifying that types of entries at the top of said stack are subtypes of the types of said operands of said current instruction; and stacking data types which are assigned to said results on said stack; said verification process being successful when said table of register types is not modified in the course of a verification of all said instructions, and said verification process being carried out instruction by instruction until said table of register types is stable, with no modification having taken place, said verification process being interrupted and said program fragment being rejected, otherwise.