[cfe-dev] Checking Model Used by 'ArrayBoundV2'

[Benjamin Schulz]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> On the other hand, I suspect there could be checks mentioned in the
> paper that the ArrayBoundV2 checker does not have.
>
> I only briefly looked at the paper. Do you have other suggestions?

Momentarily putting aside the issue of interprocedural analysis, I might
suggest that something similar to Jones and Kelly's method could be used
to warn of out-of-bounds pointer dereferences whenever the originating
pointer is declared within the scope of the function and the array in
question is declared as a predefined constant or literal.

E.g. I would expect that even in the purely intraprocedural case it
could catch something like this:

int *foo, *bar;
int baz = something;

foo = (int*) malloc(CONSTANT * sizeof(int));
bar = (foo + CONSTANT + 1);
*bar = baz;

, which the present implementation of 'ArrayBoundV2' does not catch.

> There are ways to solve these issues by implementing interprocedural
> analysis (inlining or summary based) or/and adding annotations on
> function arguments. However, none have been implemented yet.
>
> On the other hand, I suspect there could be checks mentioned in the
> paper that the ArrayBoundV2 checker does not have.

Is anyone actively working on this problem, or would I otherwise be
stepping on anyone's toes if I tinkered with 'ArrayBoundV2' to explore
the possibility of improving its false negative rate along these lines?
 I'd like to see if it's possible to do so using the current
implementation of the symbolic execution engine.  If not, I could come
back with a concrete proposal on how the engine might be extended.
Otherwise, I can continue to try to dream up test cases.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iQEcBAEBAgAGBQJO2u9hAAoJECT8Sbi31ptpXu0H/1wZ5X2xAy/0nkYmRmFYbH/S
wCT/RokGBJaNSVi6575/hH5cTcOGZxx1Sbhdb2k4N5N13wAD5KzwhV9sPvf4DaJi
3M//glALBtzvnbp4GWLYnCz0NCppxKt8ZH6oloZzkWizpISw/rQiuC9glCONwlSw
TNvfbRo4L5EqV1p0x7j8KCoW4qIKNQXwx9yDqYlNDRDCgUm4FmvxZeH7HRtY/8bS
I7I0o5/Q5p6r/v922EAk947DVB9H4ChVhA7oGG124UnXi7XbAYhiMhaX6HnLIB4S
IHTNZmzhONV5ucKKStPTp0xKxAsK9iGDoctOLrEdaY+9yDdvf9HWPlGjVErmOW4=
=vKXA
-----END PGP SIGNATURE-----