What is the project about?
Using term rewriting systems to model program semantics
Term rewriting systems are formal tools used for solving equational problems in automated deduction as well as for specification and verification in software engineering. In this last case, term rewriting systems are a convenient way to specify functions, parallel processes or (in)finite state systems where the rewriting relation represents respectively evaluation, progression and transition. One of the interest of using term rewriting system is that it leads to an executable formal model.Verifying term rewriting models using tree/term automata
For verification, in addition to classical proof tools of rewriting, it is possible to use approximations of reachable terms which is a method developed in IRISA. Starting from a set of initial terms (representing respectively all possible calls to a function, initial configuration for parallel processes, etc.) we can compute a regular super-set of all terms reachable by rewriting initial terms. This over-approximation, recognized by a tree automaton, represents a super-set of all possible evaluations (partial or completed) for functions or a super-set of all possible processes behaviors for parallel processes. Then, it is possible to check some properties related to reachability (in particular safety and security properties) on the modeled system using tree automata intersection algorithms.This method is automatic and can prove reachability properties on non-terminating term rewriting systems, i.e. on infinite models. Proving reachability properties on infinite models is hard with classical proof techniques of rewriting, but also with any automatic verification tool (like model-checking). The regular approximation technique has been implemented in the Timbuk tool and is currently used for the verification of security properties on industrial cryptographic protocols.
Putting into practice both techniques to verify Java bytecode
applications
These first experiments reveal that this technique can be used for the
proof of security properties in a more general setting than
cryptographic protocols. The first objective of this project is to
define and implement a verification tool, based on reachability, well
adapted to the proof of security properties on general purpose
rewriting models. The second objective is to demonstrate genericity of
the obtained tool by verifying security properties on some rewriting
models substantially different from those used for the cryptographic
protocol
case. Our case studies are multi-threaded Java byte code programs and
will be proposed by our industrial partner France Telecom R&D.
In order to tackle those goals and propose a general purpose verification technique, the approximation method has to be refined in two different ways. First, though the efficiency of the current prototype is sufficient for verifying some protocols, it is not the case for more complex software systems. In that direction, we aim at using some results obtained in rewriting compilation to bring the efficiency of our tool closer to what has been obtained in the model-checking domain. Second, automation of approximation has to be enhanced. At present, the approximation automaton construction is guided by a set of approximation rules very close to the tree automata formalism and given by the user of the tool. On the one hand, we plan to replace approximation rules, which are difficult to define by a human, by approximation equations which are more natural. Approximation equations define equivalence classes of terms equal modulo the approximation. On the other hand, we will automatically generate approximation equations from the property to be proved and also provide an automatic approximation refinement methodology adapted to the equational approximation framework.