[Dailydave] [fuzzing] Coverage and a recent paper by L. Suto

[Nicolas RUFF]

> Anyone of you has experience with binary-level static analyzer
> or model checkers ?

Most static analysis tools (apart from the upcoming Evarista maybe) are
working on source code. FYI, we have our very own project hosted here:
http://penjili.org/

Static analysis and model checking with the help of source code is still
in early stage of industrialization. During compilation, most type
information is lost, thus rendering the analysis even more complex. I
guess that's why there is no binary-level analyzer I am aware of.

Let's consider this seemingly simple sample:
------------------------------------
int main() {
char string[16];
char rnd[100];
int i;
int j=0;

  for (i=0; i<100; i++)
    rnd[i] = 0;		// this is the key

  for (i=0; i<32; i++) {
    string[j] = 'A';
    if (rnd[i])
      j++;
  }

  return 0;
}
------------------------------------

Depending on rnd[] values (true or false), this program could overflow.

Using the free Fortify SCA 4 software that comes with "static analysis"
book, a buffer overflow condition is always detected (whatever rnd[] value).

Using Microsoft Visual Studio 2005 (Microsoft provided VHD) with
"/analyze", no buffer overflow is detected (whatever rnd[] value).

Just to give you an idea of the existing state of the art...

Regards,
- Nicolas RUFF