|
Verification tool are used to check some important property of
critical applications. However, when a tool answers that the property
holds, the criticality has only been shifted from the the application
to the verification tool. We considered the general case of a fixpoint
computation for a transition system R. The fixpoint Phi
is computed by a tool that possibly contains bugs. Then, our goal is
to ensure the correctness of the result, independantly of the
correctness of the tool. Thus, we prove that Phi is a fixpoint of R:
forall s,s':States, Phi(s) /\ R(s,s') ==> Phi(s')
In order to guaranty that this property holds, it is far from being
possible to prove the correctness of the implementation of the
fixpoint computation. However, for a given fixpoint Phi and
transition system R, it is amenable to generate a correctness
proof for a proof-checker like COQ or PVS. Then, the correctness of
the answer no more depends on the verification tool but on the
proof-checker.
Assuming that the proof trees use inference rules of a mathematical
inference system that has been proved correct, the confidence only
depends on the implementation of the proof-checker. Its task -- the
utlimate verification -- consists in cehcking that the applications of
the rules respects the syntactical constraints of well-formedness of
the tree.
Most of the automatic verification tool compute a fixpoint, based on
which it concludes that the property is satisfied or not.
By instrumenting the verification tool, it is possible to
automatically provide a proof that the stable point reached is
actually a fixpoint.
We run one more time the fixpoint computation starting with the
current fixpoint and we generate the proof that the states reached by
R already appear in the fixpoint.
This approach has been successfully used in the case of HERMES, a
verification tool for secrecy properties in cryptographic protocols
|