Algebraic Formal Methods for Invariant Generation.

• Grant number: 11/08947-1
• Support type: Scholarships in Brazil - Post-Doctorate
• Effective date (Start): September 01, 2011
• Effective date (End): January 31, 2015
• Field of knowledge: Physical Sciences and Mathematics - Computer Science - Theory of Computation
• Principal researcher: Arnaldo Vieira Moura
• Grantee: Rachid Rebiha
• Home Institution: Instituto de Computação (IC). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil
• Associated scholarship(s): 13/04734-9 - Algebraic formal methods for program verification, BE.EP.PD

Abstract

An invariant is an assertion that hold true at a specific location on every possible run of the system. It is well-known 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. 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. We propose to reduce the problems of invariant generation for programs and hybrid systems to linear algebraic problems in order to address various deficiencies of other state-of-the-art invariant generation methods, including the efficient treatment of complicated programs and non linear hybrid systems. Such linear algebraic methods will have much lower complexities than the mathematical foundations of the previous approaches. Using these new methods, we could provide novel and efficient techniques that will form the core of new algorithms for the automation of deductive processes, and new algorithms for the verification of complex models. In particular, we will investigate and develop pioneers methods that automatically generate bases of invariants expressed by multivariate formal power series and transcendental functions. The contribution could be significant as it propose the rst automatic verification methods capable of dealing with models present in most critical hybrid, embedded systems. Our rst investigations along these lines is very promising and we were able to deal automatically with such complex systems that was intractable so far and beyond current research limits. On the other hand, we propose to extend the domain of applications for any invariant generation methods to the area of security. More precisely, we would like to provide an extensible invariant-based platform for malware analysis and show how we could detect the most virulent intrusions attacks using these pre-computed invariants. We propose to automatically generate invariants directly from the specified malware code in order to use them as semantic aware signatures, that we call "malware-invariant" that would remain unchanged by most obfuscated techniques.

Scientific publications

(References retrieved automatically from Web of Science and SciELO through information on FAPESP grants and their corresponding numbers as mentioned in the publications by the authors)

REBIHA, RACHID; MOURA, ARNALDO VIEIRA; MATRINGE, NADIR. Generating invariants for non-linear loops by linear algebraic methods. FORMAL ASPECTS OF COMPUTING, v. 27, n. 5-6, p. 805-829, NOV 2015. (11/08947-1, 13/04734-9)

REBIHA, RACHID; MOURA, ARNALDO V.; MATRINGE, NADIR. Generating invariants for non-linear hybrid systems. THEORETICAL COMPUTER SCIENCE, v. 594, p. 180-200, AUG 23 2015. (11/08947-1, 13/04734-9)