| 摘要 |
A method for securing a first program, the first program comprising a finite number of program points and evolution rules associated to program points and defining the passage of a program point to another, comprising: • a definition of a plurality of exit cases and, when a second program is used in the definition of the first program, for each exit case, definition of a branching toward a specific program point of the first program or a declaration of branching impossibility; and • a definition of a set of properties to be proven, each associated with one of the constitutive elements of the first program, said set of properties comprising the branching impossibility as a particular property; • establishment of the formal proof of the set of properties. |
