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

[Anna Zaks]

On Dec 3, 2011, at 7:56 PM, Benjamin Schulz wrote:

>> 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.

This example is not handled because the checker does not reason about malloc. Note, the analyzer CAN find the bug in the following example:

void m() {
    int foo[3];
    int *bar;
    bar = (foo + 3 + 1);
    *bar = 3;
}

> 
>> 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?

If you see opportunities to improve the checker you are more than welcome to submit patches. We are definitely interested in having a better buffer overflow solution (which requires improvements in different parts of the analyzer.)

> 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.