CASSIS Research team

Combination of approaches to the security of infinite states systems

Team presentation

The aim of the project-team is the design and the development of tools for checking the safety of systems with an infinite number of states. Our analysis of systems is based on a symbolic representation of the sets of states as formal languages or logical formulas. Safety is obtained by automated proofs, symbolic exploration of models, or tests generation. These validation methods are complementary. They are based, in our project, on accessibility problems and their reduction to constraints solving.
An originality of the project lies in its focusing on the infinite systems, parameterized or of large size, where each technique taken separately shows its limits. As examples of such systems we can mention protocols operating on topologies of arbitrary size (ring networks), systems handling datastructures with unspecified size (sets), or whose control is infinite (automata communicating by unlimited buffers).
The applications are embedded softwares on smart cards, for example, security protocols and distributed systems.

Research themes

Making of methods and tools for checking of critical software is our objective. To carry it out, we develop in a joint way deduction techniques for software safety, constraints solving techniques for tests generation, and methods for computing reachability for the verification of infinite systems.
  • Automated deduction:
    The goal is to prove the validity of assertions resulting from the analysis of the programs. We develop techniques and systems of automated deduction based on term rewriting and constraints solving. The verification of recursive data structures frequently calls upon induction, equational reasoning, and exploits properties of operators like associativity or commutativity.
  • Synthesis and resolution of set constraints:
    The objective of this task concerns the evaluation of formal specifications, based on logic and sets. Current work is based on the development of a set constraints solving system around the core system CLPS.
  • Analysis of reachability in infinite systems:
    The principal objective of this task is to determine if unsafe states can or cannot be reached by a system of large or infinite size. These reachability problems are obviously fundamental to guarantee the safety of critical systems.
The current application domains of the team are:
  • Verification of security protocols:
    Security protocols like SET, TLS, Kerberos are designed to establish confidence at the time of the electronic transactions. They rely on cryptographic primitives aiming at ensuring the integrity of data, authentication or anonymity of the participants, confidentiality of transactions, and so on.
    The experience shows that the design of these protocols is often erroneous, even when admitting that cryptography is perfect, i.e. when encrypted messages cannot be deciphered without the key. An adversary can intercept, analyze and modify the messages with small computing power and cause for example significant economic damages.
    The analysis of cryptographic protocols is complex because the set of configurations is huge or infinite: it is necessary to take into account any number of sessions, any size for the messages, the interleaving of sessions, the algebraic properties of cryptographic primitives or data structures.
    Our approach consists in automating as much as possible the protocol analysis, starting from their specifications. The system CASRUL that we develop compiles the specifications before submitting them to decisions procedures.
  • Generation of tests sequences from a formal model:
    An application of our set constraints solving system is the generation of test sequences. It relies on first extracting limit values for states variables from a specification, and second, on computing the sequences of operations that keep the system in these limit states. In the two phases, the technique uses the constraint solver.

International and industrial relations

Industrial partnerships:
  • Since 1997, a collaboration is ongoing with SchlumbergerSema, Test and Transaction division, on formal specifications and test generation from a formal model.
  • The ANVAR, within the frame of an innovation support procedure, supports the development of the BZ-Testing-Tool environment, for diffusion as free software for noncommercial use, over 2001-2003.
International relationships:
  • We participate to the European program: Information Society Technologies (IST), as members of the FET Open Project Avispa (IST-2001-39252) for 2002-5 with the ETH Zürich, the Università di Genova and Siemens Münich. The objective of this project is to to formalize and validate a representative corpus of Internet protocols selected in the drafts of the IETF, and to build a powerful analyzer for protocols described by complex specifications.
  • We collaborate with Ralf Kuesters from the university of Kiel, within the framework of the PAI Procope.
  • We collaborate with SUP'COM (High School of Communications of Tunis), within the framework of a STIC project with A. Bouhoula, on formal verification of telecommunication softwares.
  • We take part in a project on the extension of a logic (WSlogic) for checking properties of Haskell programs within the PROGRAMATICA project of the research center PACSOFT in Oregon Graduate Institute of the Oregon Health and Science University.
  • We have a partnership on test generation with the University of Waikato, Hamilton, in New Zealand, Professor Marc Utting (in six-month period invited to the LIFC, from July 2001 to January 2002), with a support of the program for scientific cooperation between France and New Zealand.
  • We are in the network CPCFQ, supporting research between France and Quebec, working on the security of cryptographic protocols.
We participate to an action Cryptology of the French Ministry of Research, concerning the verification of security protocols (VERNAM, 2001-2003), with the university of Provence (R. Amadio and D. Lugiez) and the ENS Cachan (H. Comon and J. Goubault-Larrecq).
We also collaborate with several universities, such as Dublin, Verona, EPFL Lausanne, Oran, OGE Oregon, SUNY Albany, Stanford, Grenoble, Orleans.

Keywords: Verification Security Automated proof Test Infinite systems

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social