Enhance detection of buffer overflows by introducing variable for length of array/blob

[FungOliver]

This draft PR enhances the detection of buffer overflows by introducing a variable for the length of array/blob as suggested by @michael-schwarz in #620.

Arrays:
Upon creation of a VLA vdecl creates a new ghost variable in the domain, which tracks the symbolic relationships between program variables and the length of the array. Using the query system, the arraydomain can check for out-of-bounds accesses.

Malloc:
This works similarly to the VLA case. When upon calling malloc/alloc/calloc the special transfer function creates a new ghost variable, which tracks the length of blob size. MemOutOfBounds can then use the query system to ask the relational domain if an OOB access occurred. In addition, I implemented pointer tracking as we would not be able to know the symbolic relationship of the pointer offset otherwise. (see the following example).

   int main() {
     int  EXP_OF_ARRAY_LENGTH = rand();
     EXP_OF_ARRAY_LENGTH %= 4;
     int * arr;
     arr = malloc( sizeof(int)*   EXP_OF_ARRAY_LENGTH );
     for (int  i = 0 ; i < EXP_OF_ARRAY_LENGTH  ; i++) {
       char * t = arr + i ;
       *t = 2;
     }   
   }

CHANGES/BUG fixes:
- [x] The relational domain wasn't able to parse sizeOf expression. This is now fixed. One such case would be the new test case 36 100. 
- [x] Rewrite the logic of memOutOfBounds. Previously, the analysis gave no warnings for negative indices and was therefore unsound. One such example is in the new test case 74 33
 In addition to that, due to the fact that the struct Offset and pointer Offset are analyzed separately, the analysis was unsound in certain cases. (see the newly added test 74 32 and 74 34)
 Finally, the memOutOfBounds analysis should now be more precise and give less false warnings for structs see 74 13
- [x]  Fix computation of the no_overflow flag. Previously, the no_overflow flag was computed using a comparison of top. This was incorrect in the case of comparisons. When evaluating comparisons, we get the interval [0,1], if we have an overflow. However, this does not correspond to Top. Additionally, this flag was not used in further computations. This leads to the RD being unable to compare unsigned and signed integers, which is essential for this analysis. To fix this, I added an overflow flag in the intdomain to determine if an overflow occurred in an expression. This is a nonfunctional solution; however, after initially trying to rewrite the logic to incorporate the overflow information, I concluded that this would lead to too much refactoring.
```C
int main() {
    unsigned  int EXP_OF_ARRAY_LENGTH =   (rand()%32) +2;
    for (  int i = 0 ;i < EXP_OF_ARRAY_LENGTH -33; i++) 
        assert( i< EXP_OF_ARRAY_LENGTH); // UNKNOWN
    return 0;

}

TODO:

• Option for toggling pointer tracking
• Rewrite memOutOfBounds query logic
• Fix removal of ghost variables after function return
• Clean-up

[jerhard]

Thank you for your pull request! Supporting relational information about array lengths and allocated blocks will be very neat!

I left some first round of remarks that you may have a look at.

[jerhard]

Did you find an example where the old no overflow handling in the relational domain caused an unsoundness in the analysis results?

[FungOliver]

The old no overflow handling didn't cause any unsoundness in the analysis results because the flag was ignored (see comment). However this overflow handling is not sufficient for the analysis, due to apron giving up when there is a cast from signed integer to unsigned integer and vice versa even when enabling --set sem.int.signed_overflow assume_none. This may work for relational vla length analysis if there are just integers, but for malloc cil cast the expression to unsigned long.

[FungOliver]

If we decide to not ignore the old overflow handling, we do get unsoundness in the analysis as one can see in 6b797ad.

// PARAM: --enable ana.int.interval --set ana.activated[+] apron
#include <stdlib.h>
#include <goblint.h>

int main()
{
    unsigned int len = rand();
    len = len % 10;

    for (int i = 0; i -1 < len ; i++)
    {
        int tmp = i;
    }
}

This results in

[Error][Analyzer][Unsound] both branches over condition '(unsigned int )(i - 1) < len' are dead (tests/regression/100-limitation/01-crash.c:9:9-9:37)
[Error][Analyzer][Unsound] Both branches dead

[FungOliver]

I, unfortunately, found out that the current overflow handling in this PR also suffers from this problem. The queries for EvalInt are cached, which results in the local_no_overflow not being set correctly.

One idea to solve this problem, which don't involve rewriting the whole evalint function would be to disable the cache lookup with another global flag.

[FungOliver]

I, unfortunately, found out that the current overflow handling in this PR also suffers from this problem. The queries for EvalInt are cached, which results in the local_no_overflow not being set correctly.

One idea to solve this problem, which don't involve rewriting the whole evalint function would be to disable the cache lookup with another global flag.

Disabling the cache with a global flag seems to work. However, I agree that this solution may not be the prettiest. After having a look at the overflow handling in Linear two var equality #1297 and testing a bit, it seems like their overflow handling may also work with my analysis.

[michael-schwarz]

Great to see there's progress here! I left some first comments, but I have not had the time to go into details yet (especially the changes inside the relational domain and the oob analysis).

Here's two questions I already have though:

• One's conceptual: Have you considered what happens for multi-threaded programs? Initially we thought about having an analysis such as this to demonstrate the usefulness of our analyses of global variables. Do you think this it within reach?
• The other one is perhaps more down to earth: What do you do when you encounter a malloc only in one branch? Will you not have issues with the apron environments not matching up after the join?

[michael-schwarz]

Also why ID above and VDQ.ProdID here? The meaning of the tuple should ideally be obvious from the name.

[FungOliver]

For the relational VLA oob check, I don't check if the index can be negative because if the relational domain knows that the index is not negative, the bounds for the array index would be improved anyway in the Valuedomain.

However, this does not work for pointer arithmetic. The relational domain doesn't track the relationship between pointers (yet). Therefore the analysis can't give boundaries for the memory access. In the (newly) added test case 85 14 memOutOfBounds would raise a warning that we may access the array before the allocated memory. With the new pointer_tracking enabled, which tracks relational relationships between pointers, we know that this cannot be the case. We, therefore, return a tuple of ID FlatBool to know if we might access before or after the allocated memory.

[michael-schwarz]

Why does this cache need to be disabled?

[FungOliver]

This is for the new no overflow computation in the relational domain, as the old one was unsound and unused. I added a local_no_overflow flag in the intdomain and checked this flag after an EvalInt query. This is a kind of dirty hack, as I first tried to rewrite the Evalint to include the overflow information, but after adapting the intdomain and trying to adopt the base.ml to include the overflow information. I noticed that this would involve nearly a few thousand lines of code and deemed this not reasonable for this PR.

This works in most cases except for loops, where it seems like the EvalInt query is cached, which results in the EvalInt query not being newly evaluated and the flag not being set correctly. See also: #1330 (comment)

[sim642]

This is very suspicious. We assume that queries are pure, so caching or not caching cannot make an observable difference. If it can, then something is wrong.

We don't recompute until query results stabilize, so in the presence of such impure queries we have no soundness guarantees anymore.

[FungOliver]

This is, because for the no_overflow query uses side effects to evaluate if we have an overflow. It queries the EvalInt query and checks the side effect for an overflow. However, this does not work if the query is cached.

[FungOliver]

Greta to see there's progress here! I left some first comments, but I have not had the time to go into details yet (especially the changes inside the relational domain and the oob analysis).

Here's two questions I already have though:

* One's conceptual: Have you considered what happens for multi-threaded programs? Initially we thought about having an analysis such as this to demonstrate the usefulness of our analyses of global variables. Do you think this it within reach?

* The other one is perhaps more down to earth: What do you do when you encounter a `malloc` only in one branch? Will you not have issues with the apron environments not matching up after the join?

• The problem with global variables in Multithreading right now is that we need the relational information of the ghost variable with the initialization expression together in one domain. However, in the case of multithreading, the global variables get removed and are tracked separately. Therefore, we lose the relational relationship between the ghost variable and the initialization expression. Additionally, in the case of escaped variables, the relationship remains in the domain. Nonetheless, this is still useless due to the fact that new variables are introduced for the escaped variables. So, we still know nothing in this case. I got this to work with global invariants after setting the ghost variable to Global type.

• Yes, this is indeed a problem. However, I am also not quite sure how to solve this problem...

Unfortunately, I don't think solving later issues is within reach. Investigating and fixing bugs in the relational domain and unsoundness issues in memOutOfBounds took quite some time.

[jerhard]

Before merging this, one should verify whether the handling of non-unique mallocs is sound here, e.g. for a program segment:

int n = 1 + (rand() % 5);
for(int i = 0; i < n; i++){
   int* a = malloc(i * sizeof(int));
   if(i == 0){ b = a;}
}
*b = 4; // Should warn, as size of block pointed to by b is zero.

[jerhard]

How does this ensure that the relational analysis never leaks the introduced dummy variables to other analysis, e.g. by making queries? Note that the relational information for other variables then may also be expressed via the dummy variables.

[FungOliver]

The ghost variables are added into the environment with RD.add_vars like in body and in return

analyzer/src/analyses/apron/relationAnalysis.apron.ml

Line 361 in d86fe48

let rel' = RD.add_vars st.rel [RV.return] in

The ghost variables are needed to evaluate any relational relationship between for example arrays and should be part of the relational domain. I am not quite sure what you mean by leak here. However, I think that the ghost variables should behave similarly to the other variables in the relational domain?