Reachability analysis in rewriting has served as a verification technique in recent decades, despite the underlying issue being undecidable. Regular tree model-checking has found application in verifying security protocols, Java programs, and concurrent systems. The premise in these approaches is to represent the targeted system as a state system and encode its transitions using a term rewriting system or a tree transducer. The crucial aspect lies in calculating a fixed point that represents the set of configurations or states that can be reached. While this is generally uncomputable, it is sufficient to compute an overapproximation for the purpose of verifying safety properties. Let A, B, and ℛ represent, respectively, an initial set of terms, a set of forbidden (“bad”) terms, and a term rewriting system. The question is whether there exists a regular approximation A^⋆ of the set of reachable terms such that A^⋆⊇ℛ^*(A) and A^⋆∩ B = ∅ . Finding suitable approximations requires, in practice, the use of heuristics, steered towards an anticipated conclusive fixed point by the intervention of human domain experts. The parameters upon which they act may take the form of term equations, normalizing rules, predicate abstractions, etc., but in all cases boil down to carefully choosing states to merge during the fixpoint computation, forcing convergence while avoiding overshooting the approximation into B . We propose a practical, scalable automated method offloading that expert work to a SAT solver.

Performing formal verification of concurrent systems involves partial order logics (here MSO with partial orders) for the specification of properties or of the concurrent system itself. A common structure for the verification of concurrent systems is so-called pomset. A pomset is a multiset of partially ordered events. The partial order relation describes causal dependencies of events. We propose a new word based model, namely Pre-Post-Pomset, making the exploration of pomsets space possible. In this paper, our new model stands to be a general model in the sense that some classical models used in the specification of concurrent systems (Synchronized product of systems, Mazurkiewicz traces or parallel series) can be specified within. Besides its general aspect, our model offers decidability results on the verification problem according to an MSO formula on pomsets.

In this paper, we propose an extension of a technique transforming logic programs into a particular class of logic programs called CS-programs. Up to now, this technique is a semi-algorithm preserving the least Herbrand model. We integrate in this technique a process of generalization. Thanks to it, we are able to make the computation (the transformation) terminate and if we force the computation to terminate then we obtain a CS-program whose least Herbrand model contains the initial one. In this way, we can tackle successfully reachability problems that are out of the scope of techniques using regular approximations and also of the initial transformation technique (for which computations do not terminate).

Over-approximating the descendants (successors) of an initial set of terms under a rewrite system is used in reachability analysis. The success of such methods depends on the quality of the approximation. Regular approximations (i.e. those using finite tree automata) have been successfully applied to protocol verification and Java program analysis. In [2,10], non-regular approximations have been shown more precise than regular ones. In [3] ( fixed version of [2]), we have shown that sound over-approximations using synchronized tree languages can be computed for left-and-right-linear term rewriting systems (TRS). In this paper, we present two new contributions extending [3]. Firstly, we show how to compute at least all innermost descendants for any left-linear TRS. Secondly, a procedure is introduced for computing over-approximations independently of the applied rewrite strategy for any left-linear TRS.

To check a system, some verification techniques consider a set of terms I that represents the initial configurations of the system, and a rewrite system R that represents the system behavior. To check that no undesirable configuration is reached, they compute an over-approximation of the set of descendants (successors) issued from I by R, expressed by a tree language. Some techniques have been presented using regular tree languages, and more recently using non-regular languages to get better approximations: using context-free tree languages [1] on the one hand, using synchronized tree languages [2] on the other hand. In this paper, we merge these two approaches to get even better approximations: we compute an over-approximation of the descendants, using synchronized-context-free tree languages expressed by logic programs. We give several examples for which our procedure computes the descendants in an exact way, unlike former techniques.

Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes over-approximation of descendants, using synchronized tree-(tuple) languages expressed by logic programs.

Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time. This paper proposes a new CounterExample Guided Abstraction Refinement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in finite time. This set is represented by ℛ_/E -automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certified by Coq, which means that they are formally proved correct.

This paper proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called functional term rewriting systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Second, we present the implementation of our FTRS-based tool as well as optimisations based on local fixpoint computations. Our experiments show that for well-known protocols (e.g., tree arbiter, percolate, leader election protocol,...) our tool is more efficient than other rewriting tools such as Timbuk, Maude or Tom. Moreover, it can also be applied to check invariant properties which are a particular subclass of linear temporal logic (LTL) formula.

In [1], we have described a technique for computing non-regular approximations using synchronized tree languages. This technique can handle the reachability problem of [2]. These synchronized tree languages [4, 3] are recognized using CSprograms [5], i.e. a particular class of Horn clauses. From an initial CS-program Prog and a left-linear term rewrite system (TRS) R, another CS-program Prog′ is computed in such a way that its language represents an over-approximation of the set of terms (called descendants) reachable by rewriting using R, from the terms of the language of Prog. This algorithm is called completion. However, the assumptions of the result showing that all the descendants are obtained, i.e. Theorem 14 in [1], are not correct. Actually, preserving should be replaced by non-copying (a variable cannot occur several times in the head of a clause). However, the non-copying nature of a CS-program is not preserved by completion as soon as the given TRS is not right-linear. Consequently, the final result presented in [1] holds for completely linear TRS, and not for just left-linear TRS. In this paper, we propose a correction of [1], assuming that the initial CSprogram is non-copying, and the TRS is completely linear (see Section 3).

Tree Regular model checking is the name of a family of techniques for analyzing infinite- state systems in which states are represented by trees and sets of states by tree automata. From the verification point of view, the central problem is to compute the set of reachable states providing a given transition relation. A main obstacle is that this set is in general not computable in a finite time. In this paper, we propose a new CounterExample Guided Abstraction Refinement technique that can be used to check whether a set of state can be reached from the initial set. Contrary to existing techniques, our approach relies on equational abstraction to ease the definition of approximations and on a specific model of tree automata to avoid heavy backward refinement steps.

This paper proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures. Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round Robin Mutex protocols,...) our tool is not only better than other rewriting tools such as Timbuk or Maude, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).

This paper extends a rewriting approximations-based theoretical framework in which the security problem - secrecy preservation against an active intruder - may be semi-decided through a reachability analysis. In a recent paper, we have shown how to semi-decide whether a security protocol using algebraic properties of cryptographic primitives is safe. In this paper, we investigate the dual - insecurity - problem: we explain how to semi-decide whether a protocol using cryptographic primitive algebraic properties is unsafe. This improvement offers us to draw automatically a complete diagnostic of a security protocol with an unbounded number of sessions. Furthermore, our approach is supported by the tool TA4SP successfully applied for analysing the NSPK-xor protocol and the Diffie-Hellman protocol.

This paper is dedicated to candidate abstractions to capture relevant aspects of the integer weighted automata. The expected effect of applying these abstractions is studied to build the deterministic reachability graphs allowing us to semi-decide the positivity problem on these automata. Moreover, the papers reports on the implementations and experimental results, and discusses other encodings.

This paper addresses the following general problem of tree regular model-checking: decide whether R∗(L)∩Lp=∅ where R∗ is the reflexive and transitive closure of a successor relation induced by a term rewriting system R, and L and Lp are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are left-quadratic. The most common practical case is handled this way.

Term Rewriting Systems (TRSs) are now commonly used as a modeling language for applications. In those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. Using a tree automata completion technique, it has been shown that the non reachability of a term tcan be verified by computing an over-approximation of the set of reachable terms and proving that tis not in the over-approximation. Since the verification of real programs gives rise to rewrite models of significant size, efficient implementations of completion are essential. We present in this paper a TRS transformation preserving the reachability analysis by tree automata completion. This transformation makes the completion implementation based on rewriting techniques possible. Thus, the reduction of a term to a state by a tree automaton is fully handled by rewriting. This approach has been prototyped in Tom, a language extension which adds rewriting primitives to Java. The first experiments are very promising relative to the state-of-the-art tool Timbuk.

This paper addresses the following general problem of tree regular model-checking: decide whether R * ( L ) ∩ L p = θ where R * is the reflexive and transitive closure of a successor relation induced by a term rewriting system R , and L and L p are both regular tree languages. We develop an automatic approximation-based technique to handle this - undecidable in general - problem in most practical cases, extending a recent work by Feuillade, Genet and Viet Triem Tong. We also make this approach fully automatic for practical validation of security protocols.

Term rewriting systems are now commonly used as a modeling language for programs or systems. On those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth-Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term tcan be shown by computing an over-approximation of the set of reachable terms and prove that tis not in the over-approximation. However, when the term tis in the approximation, nothing can be said.In this paper, we improve this approach as follows: given a term t, we try to compute an over-approximation which does not contain tby using an approximation refinement that we propose. If the approximation refinement fails then tis a reachable term. This semi-algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the interest of such an approach w.r.t. verification on rewriting models.

La demarche qualite/fiabilite n'est pas aussi exigeante en informatique que dans des domaines comme la mecanique. Toutefois dans des domaines tels que l’aerospatiale ou la securite de l’information, la qualite, la fiabilite et la securite priment dans tous les projets informatiques. Le projet europeen AVISPA est dedie au developpement de techniques de validation de protocoles de securite afin de les rendre disponibles simplement aux ingenieurs developpant ces protocoles. Le double enjeu etait d'etre a la fois performant dans cette validation et de mettre ces performances a la portee de non-specialistes.

The verification of cryptographic protocols has greatly improved these last years. Automated tools such as AVISPA provide real help in finding and characterizing attacks. The counterpart is the formal specification of the protocol, using an appropriate language such as HLPSL. Since HLPSL is a very expressive language, this stage is complicated and error-prone before a correct specification is eventually obtained. The verification tools of AVISPA are not designed to detect such specification errors. Unfortunately, as long as it contains typo-like errors, the verification of a HLPSL specification is pointless. In this paper, we propose an animation tool called SPAN †. It turns a formal protocol specification into an execution diagram, according to user choices. We show how the visualization eases the formal specification stage in many ways: drawing of typical execution diagrams, visualization of protocol termination, understanding of interleaved sessions, detection of unwanted side effects, etc. We also show how visualization and simulation of an intruder helps in finding attacks that are not automatically detected by tools.