RAVAJ

In the field of computer security, formal methods are more and more successful and spread in the industry. Industrial use of formal methods for security yields some new needs on specification and verification methodologies : more automation and more flexibility. Those two new requirements are due to the fact that, nowadays, security has to be ensured on a large number of different general audience devices/softwares, all of them rapidly updated. Hence, the formal model should be easy to design and easy to modify. Similarly, for verification, proofs should be as automatic as possible and easy to adapt to the formal model evolutions. Among all the formal methods used in security, term rewriting systems are a simple and flexible formalism that is now commonly used for the specification of programs or systems. As an example, several versions of the Java virtual machine have been specified using rewriting as well as several models for cryptographic protocols. However, using classical rewriting tools to achieve verification over those models is hard. Indeed, most of those rewriting models have an infinite behavior (due to the possibly infinite set of input data or due to the infinite set of execution pathes) which cannot be handled with most of automatic proof tools on rewriting. On the other hand, abstract interpretation and static analysis can prove security properties on programs with an infinite behavior. Abstract interpretation helps to represent finitely an infinite number of input data or an infinite number of execution pathes. However, validity of proofs by abstract interpretation rely on an other proof step, so-called safety of abstraction, which is generally done by hand. Furthermore, each change in the abstraction or in the model to verify results into a new proof of safety to be written. The first goal of this project is to define a method to automatically produce certified static analysis for security properties over rewriting models of programs or systems. For this purpose, we plan to use regular approximations of reachable terms which are specific abstractions whose safety is guaranteed by construction. The second objective consists in improving efficiency and flexibility of this technique so as to verify security properties on real, multi-threaded, Java programs for cell phones.