Algebraic Formal Methods for Invariant Generation

You are cordially invited to attend the PhD Dissertation Defense of Rachid REBIHA on Friday, January 28th 2011 at 14h00 in room SI-008 (Informatics building)

Abstract:

It is well-know that the automation and effectiveness of "formal verification" of softwares, embedded systems or hybrid systems depends to the ease with which precise invariants can be automatically generated. Actually the verification problem of safety properties can be reduced to the problem of invariant generation.

Also, invariants are essential to establish liveness properties such as progress or termination. Automated discovery of invariants allow also the construction of automated "static analysis" and coverage "test-case generation". The static analysis and verification of programs, hybrid systems or embedded systems has been one of the main challenges for the formal verification community over several decades.

Despite tremendous progress over the years, the problem of "invariant generation" remains very challenging for both "non-linear discrete programs", as well as for "non-linear hybrid systems".

In this thesis, we first present new computational methods that can automate the discovery and strengthening of non-linear interrelationships among the variables of a program that contains non-linear loops, that is, programs that display multivariate polynomial and fractional manipulations. Moreover, most of safety-critical systems such as aircraft, automobiles, chemicals, power plants and biological systems, ... operate semantically as non-linear hybrid systems.

We demonstrate powerful computational methods that can generate basis for non-linear invariant ideals of non-linear hybrid systems.

We also show that the preconditions for discrete transitions and the Lie-derivatives for continuous evolution can be viewed as morphisms and can be suitably represented by matrices. The new relaxed consecution requirements, extended to fractional scaling, are also encoded as morphisms represented by matrices with terms that can be used to approximate the consecution conditions.

By reducing the problems of non-trivial non-linear invariant generation for programs and hybrid systems to related linear algebraic problems we are able to address various deficiencies of other state-of-the-art invariant generation methods, including the efficient treatment of complicated non-linear loop programs and non-linear hybrid systems. Such linear algebraic methods have lower complexities than the mathematical foundations of the previous approaches such as Grobner basis computation, quantifier elimination and cylindrical algebraic decomposition.

Secondly, we present the first verification methods that automatically generate basis for invariants expressed by "multivariate formal power series" and "transcendental functions". We also discuss their convergence over hybrid systems that exhibit non linear models. The formal power series invariants generated are often composed by the expansion of some well-known transcendental functions e.g. "log" and "exp". They also have an analysable closed-form which facilitates the use of the invariants when verifying safety properties. For each invariant generation problem, we establish very general sufficient conditions that guarantee the existence and allow for the computation of invariant ideals for situations that can not be treated in the present invariant generation approaches.

Finally, we extend the domain of applications for invariant generation methods to the area of security. More precisely, we provide an extensible invariant-based platform for malware analysis and show how we can detect the most virulent intrusions attacks using these invariants.

Dissertation Committee:

• Prof. Fernando Pedone, Università della Svizzera italiana, Switzerland (Research Advisor)
• Prof. Mauro Pezzè, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Evanthia Papadopoulou, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Hassen Saidi, Stanford Research Institute, California, USA (External Member)