salle A. Turing CE4
12 avril 2013 - 14h00
Verifying C-Programs memory faults freedom by mean of Abstract Interpretation and a-posteriori model verification
par Florent Garnier de VERIMAG
Abstract: This work presents an original technique that
allow to guarantee that a given ANSI C program is free from certain
memory faults. The faults we consider are pervasive in such
programs and all C program developers as well as program users
have been concerned with such issues.
In this work, we are tracking a subset of the memory faults,
such as: A memory access through
a dangling pointer, calling free() upon a pointer that does not
refer to an allocated memory cell, memory leakages, access outside
an allocated memory zone or using a non-aligned pointer address
to perform a memory access.
Verifying those properties is not trivial as the source of
errors can either be due to the shape of the memory --access
to a non allocated memory cell, or be due to some arithmetic
constraints on the address of pointers --access to an
allocated memory cell, but outside its bounds.
To track those errors, we combine a static analysis by abstract
interpretation approach using an abstract domain defined thanks
to a weaker version of the separation logic, followed by a verification
step performed by verification tools upon the aforementioned abstract
system.
Basically :
_ During a first phase, we do extract a counter automaton based
model of the input program, using static analysis and abstract
interpretation techniques.
_ In a second phase, we compile this model into the Numerical Transition
Language, which is a common format used to describe numerical transition systems, a.k.a. Hierarchical counter automata systems.
Once this model is compiled, we query various verification tools for
the reachability of the states that abstract a memory fault in the
original program.
When the verification tools answers that no error states are reachable
then we can guarantee that never such an error will occur.
In the other case, the counter example trace need to be analyzed
to check whether it corresponds or not to a false alarm.
This verification technique has been prototyped as a FRAMA-C plugin, used
as a front-end for Numerical Transitions Systems reachability analysis
verifiers. Those techniques as well as the front-end are the fruit of
a collaboration between Radu Iosif and Florent Garnier.
