Research activities

    • Verification of cryptographic protocols, the Hermes tool
      with Liana Bozga, Yassine Lakhnech             

    • Certification of security applications for smart cards
      Eden project with M.Bozga, Y.Roux, L.Bozga, M.Garnacho             

    • Certification of the verdict of a verification tool
      • Certification of Cryptographic Protocols by Abstract Model-Checking and Proof Concretization
        with R.Janvier and Y.Lakhnech, ITCES'2006, San Jose.
        slides [pdf], paper [pdf]
      with Romain Janvier, Yassine Lakhnech             
      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