Method for securing a program

摘要

A method for securing a first program with a second program, a third program and a fourth program, each program comprising constitutive elements having a finite number of program points and evolution rules associated with the program points and defining the passage from one program point to another program point, and each program comprising a definition of a set of properties each property being associated with one or more of the constitutive elements of the program. The fourth program constructed by defining at least one relation between at least one constitutive element of the second program and at least one constitutive element of the third program, said relation being named a correspondence relation, and at least one property of the third program being proven, propagate the proof of said property to at least one property of the first program by exploitation of the correspondence relation.

主权项

1. A method for securing a first program, referenced hereinafter as a target program with a second program, referenced hereinafter as a target representative program, a third program, referenced hereinafter as a lemma program, and a fourth program, referenced hereinafter as a composition program, each program comprising constitutive elements, said constitutive elements comprising a finite number of program points and evolution rules associated with the program points and defining the passage from one program point to another program point, and each program comprising a definition of a set of properties each property being associated with one or more of the constitutive elements of the program, said method comprising:
constructing the composition program by defining at least one relation between at least one constitutive element of the target representative program and at least one constitutive element of the lemma program, said relation being named a correspondence relation; and exploiting the correspondence relation for establishing a relation between one property of the first program and at least one property of the lemma or composition program, said relation being named a “sufficiency relation” and being such that it creates an oriented relationship between one local property of a program, and one or more local properties of the same or another program such that the proof of the latter properties proves the first local property, or propagate the proof of said property to at least one property of the target program.