[eros-arch] Static checking
Tue, 02 Mar 2004 10:40:14 +0100
Valerio Bellizzomi wrote:
>I just found this program
Well, I started my PhD (and never finished it :-) on an attempt in
writing something like this. I wanted to chase buffer overflows and
incorrect lock management in the Linux kernel, using abstract
interpretation techniques - http://www.di.ens.fr/~cousot/aiintro.shtml -
but this has been done numerous times since then, with various,
C-Breeze looks like a cool starting point for anyone who wants to
statically analyze C code (assuming this person does not mind coding in
C++ :-), however it mostly does just the easy part (parsing and AST
modeling), not the all-important analyses (data-flow, range checks,
assert eliminations etc.) which are much harder. And it does not parse C++.
If I were to restart that job, I would personnally prefer any other
language to C++ for AST-frobbing - OCaml would probably be my choice.
And I would consider engineering an invariance-conservation framework
that helps guaranteeing that the transformations applied by "changers"
do not alter the semantics of the program (this is lacking in C-Breeze).
BTW, what are the envisioned benefits of static analysis in Eros? Is it
for checking the TCB?
Dominique QUATRAVAUX Ingénieur senior
01 44 42 00 08 IDEALX