Hi, this pr contains some improvements and fixes to buffer overrun analysis. The two fixes were originally inspired due to the two false positives/negatives we found during using it.
The buffer overrun checker ignores checking the case when the index may be +oo while the array size is less than +oo. It may cause a false negative. For example,
int a[1];
for(int i=0; a[i]; i++) {}
There will be a buffer overrun issue within the condition judgment of the for statement since i will finally be equal to 1 and the statement will check whether a[1] is nonzero.
The buffer overrun checker makes a rough estimation when adding two upper bounds, i.e., when i1 <= max {1, i1}, i2 <= i2, BO only let i1 + i2 <= 1 + i2, while the true upper bound should be max{1 + i2, i1 + i2}. Hence it will cause a false positive when checking the codes below:
Before executing the fourth if statement, BO will regard the value of seedlen as max{16, entropy_len}. However, when executing the fourth if statement, by adding the two variables seedlen and nonce_len, BO makes a rough estimation as above description, and will regard the upper bound of seedlen as 16 + nonce_len. Hence, it will cause a false positive when executing the call to the memcpy function.
For the two issues above, I have made the following improvements.
Within the checking function of array access, I let BO report a L3-level error when the upper bound of index is +oo and the upper bound of the array size is limited.
I have implemented a more precise plus of bounds. It handles the case when one operator is c1 + max{x1, d1} and another is c2 + d2.
Hi, this pr contains some improvements and fixes to buffer overrun analysis. The two fixes were originally inspired due to the two false positives/negatives we found during using it.
There will be a buffer overrun issue within the condition judgment of the
for
statement sincei
will finally be equal to 1 and the statement will check whethera[1]
is nonzero.Before executing the fourth
if
statement, BO will regard the value ofseedlen
as max{16, entropy_len}. However, when executing the fourthif
statement, by adding the two variablesseedlen
andnonce_len
, BO makes a rough estimation as above description, and will regard the upper bound ofseedlen
as 16 + nonce_len. Hence, it will cause a false positive when executing the call to thememcpy
function.For the two issues above, I have made the following improvements.
L3
-level error when the upper bound of index is +oo and the upper bound of the array size is limited.