As you probably know, I'm a huge fan of Formal Methods: use appropriate Mathematics and tools to ensure a program is correct in all possible situations. In other words, bug free software... well, sort of. :-)
The interesting side of this is that tools to apply Formal Methods have improved a lot and most of them are now Free Software. I'm maintaining a list of Free Software tools for Formal Methods (it is a wiki, you can update it!).
I would like to make an experiment with Frama-C and its plugins, especially Jessie. Frama-C is a framework for static analysis of C programs developed at CEA. Combined with the Why and Alt-Ergo tools, you can prove some properties on real C code (absence of integer underflow or overflow, absence of out-of-bound accesses, absence of NULL pointer de-referencing, program's specific properties, etc.). All those tools are Free Software and are developed in OCaml. And they now are available in Debian and Ubuntu!
I made a simple experiment last year but I would like to make a more elaborated one.
Therefore, I'm looking for a piece of C code with following criteria:
- Free Software: I'm interested in improving software for the whole humankind; ;-)
- Pure C code, no C++. If there is some assembly, I could work around for example by re-writting corresponding C function;
- Code of moderate size, a few thousands line at most. It could be a sub-module or subset of a bigger code;
- Code using mostly integers and pointers, few strings (aka
char *)[1]; - Verifying some properties on this code would be "interesting". Several possible reasons: for security or safety reasons, because the code is used in an embedded platform on which modifications are difficult once in production or simply because this code is used a lot.
If you know some software that fills those criteria, let me know through a comment or at dmentre@linux-france.org!
Notes
[1] Frama-C is a bit slow to handle strings and it can become cumbersome.
Comments
Fri 19 Mar 2010
What about image decoding libraries, such as libjpeg or libpng, they often have security issues. Or compression/decompression libraries ?
See for example http://www.libpng.org/pub/png/libpn... for a big number of security issues, due to out-of-bound reads, buffer overflows, uninitialized data, and so forth.
Fri 19 Mar 2010
«Verifying some properties on this code would be "interesting".» Of course, but that means that interesting properties are already known (i.e. 'a priori'). Thus, the software should be (well) documented or may be related to a reference documentation (such that norm, RFC ...)
By the way, would be interesting to setup a kind of forge to share this kind of experiments (beginning with the one mentionned on frama-C list ;) / and saving lot of time for people who intend to learn this kind of technologies/
Tue 23 Mar 2010
@Thomas: Good idea! I'll take a look at libpng.
@GMR: I would made a difference between "system" properties (like we have in safety critical system in railway) and "micro"-properties like checking that arguments to a function are in the correct range. Security issues in libraries like libpng are of the second kind.
Regarding the setup of a Forge, a simple wiki like dokuwiki should be enough as a starting point.