Potentially Unsafe Buffer Overflow Not Detected with `scanf` User Input in Buffer Overflow Analysis

[ouatu-ro]

When analyzing the following code with IKOS, the analyzer reports the program as "SAFE" with no warnings, even though l is set by scanf without bounds checking. This unbounded input could lead to an out-of-bounds access on a[10], which should ideally be flagged by the buffer overflow analysis (boa):

#include <stdio.h>
int a[10];
int main(int argc, char *argv[]) {
    size_t i = 0;
    size_t l = 5;
    scanf("%zi", &l);
    printf("%zi\n", l);
    for (; i < l; i++) {
        a[i] = i;
    }
}

In this example, if the user enters a value for l greater than 10, the loop will write out of bounds of the array a[10], leading to undefined behavior.

Expected Behavior

The buffer overflow analysis (boa) or other relevant checks should flag this as a potential out-of-bounds access due to unbounded user input.

Actual Behavior

IKOS reports the program as "SAFE" with no warnings, potentially overlooking the risk of unbounded user input leading to out-of-bounds access.

Could you clarify if this is a known limitation or if there are additional configuration options to enable more robust detection of potential buffer overflows with unbounded inputs?

Thank you!

[Vivraan]

I think this is related to #136, #138, and #208 regarding a known limitation for bounds-checking arrays and loop-writing.