Use-After-Free (UAF) Analysis First Iteration

[mrstanb]

To sum up the PR infos:

• Added a UAF analysis to Goblint
• For this, I also had to add free as a supported library function (similar to malloc)
• Added a simple C regression test file with a UAF bug

Note: Currently the analysis doesn't seem to be really working properly, hence it's only a first iteration. I'm debugging my way through it to try and find out what's going on and what's wrong.

@michael-schwarz feel free to do a review round

[michael-schwarz]

Something we should also write tests for: Developers like to have custom wrappers around calls to memory-related functions such as free or malloc to potentially plugin-in a custom allocator. I think we will be precise in presence of such usages, as we are context-sensitive in the pointer argument that is passed to free, but it might still be worth having tests for this.

[mrstanb]

There are two ways how to fix this: We immediately go for a solution to this problem in the multi-threaded context, or we add a simple heuristics to basically make the analysis warn whenever something is accessed in multi-threaded mode, and improve precision in a separate PR.

I think I'd go for the second option and add proper multi-threaded support in a separate PR, if we'd prefer to keep this PR rather lean and not too big. What do you think?

[mrstanb]

Something we should also write tests for: Developers like to have custom wrappers around calls to memory-related functions such as free or malloc to potentially plugin-in a custom allocator. I think we will be precise in presence of such usages, as we are context-sensitive in the pointer argument that is passed to free, but it might still be worth having tests for this.

Should be now covered by 9e5cd7a

[mrstanb]

Thank you for the PR, and sorry I am only now getting around to reviewing it in detail.

Here's a first issue: As expected, this does not soundly account for UAF in the concurrent setting yet:

//PARAM: --set ana.activated[+] useAfterFree
#include <stdlib.h>
#include <stdio.h>
#include <pthread.h>

int* gptr;

// Mutex to ensure we don't get race warnings, but the UAF warnings we actually care about
pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER;

void *t_other(void* p) {
    pthread_mutex_lock(&mtx);
    free(gptr); //WARN
    pthread_mutex_unlock(&mtx);
}

int main() {
    gptr = malloc(sizeof(int));
    *gptr = 42;

    pthread_t thread;
    pthread_create(&thread, NULL, t_other, NULL);

    pthread_mutex_lock(&mtx);
    *gptr = 43; //WARN
    free(gptr); //WARN
    pthread_mutex_unlock(&mtx);

    return 0;
}

There are two ways how to fix this: We immediately go for a solution to this problem in the multi-threaded context, or we add a simple heuristics to basically make the analysis warn whenever something is accessed in multi-threaded mode, and improve precision in a separate PR.

As a idea: We might want to record the thread ids of threads (and potentially which threads have already been joined at that point) that free the memory in a global invariant. Then, upon a potentially multi-threaded access, I need to warn if the thread ids do indicate that the free must have happen only after the current function.

I now added this example C program as a regression test for UAF in a multi-threaded context (cf. a00814f)

I also added a simple heuristic that warns for a potential UAF occuring whenver the program is definitely not single-threaded (cf. 9545618)

As already discussed, the proper multi-threaded solution for UAF detection will be implemented in a follow-up PR