[eros-arch] Static checking

[Dominique Quatravaux]

Valerio Bellizzomi wrote:

>I just found this program
>
>C-Breeze
>http://www.cs.utexas.edu/users/c-breeze/
>
>opinions ?
>  
>
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, 
unrelated techniques.

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