Regression: KLEE may miss use-after-free in call to libc function (detected correctly in 1.4)

[moyix]

In the following program (reduced from Juliet test case CWE416_Use_After_Free/CWE416_Use_After_Free__return_freed_ptr_01.c) KLEE misses a use-after-free (UAF) when a pointer is passed to a library function like puts:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

char * dothing() {
    char *t = "B";
    char *s = malloc(2);
    if (s != NULL) {
        s[1] = '\0';
        for (int i = 0; i < 1; i++)
            s[i] = t[i];
        free(s);
        return s;
    }
    else {
        return NULL;
    }
}

int main(int argc, char **argv) {
    char *s = dothing();
    puts(s);
    return 0;
}

Test case reduction notes:

• If puts(s) is directly after the free(s), then KLEE will catch the bug.
• If the for loop is removed, or replaced by s[0] = t[0], then KLEE will catch the bug.
• If the if/else is removed (so there is no check on the return value of malloc), then KLEE will catch the bug.
• Using printf("%s\n", s) instead of puts(s) will also cause KLEE to miss the bug, even if uclibc was built with -DKLEE_SYM_PRINTF

We went back to check KLEE 1.4, and it successfully detects the UAF.

Output from the most recent version of KLEE:

$ klee --version
KLEE 2.3-pre (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: TRUE)
  Build revision: 5ee3a54001fe4291a0a5c3ce3beb33f856836cbb

LLVM (http://llvm.org/):
  LLVM version 9.0.1
  Optimized build with assertions.
  Default target: x86_64-unknown-linux-gnu
  Host CPU: znver2

$ klee --posix-runtime --libc=uclibc test.bc
KLEE: NOTE: Using POSIX model: /tmp/klee_build90stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build90stp_z3/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: Using STP solver backend
warning: Linking two modules of different target triples: test.bc' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'

KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94446342609136) at klee_src/runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
xU

KLEE: done: total instructions = 13975
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 1

The version of KLEE that catches the UAF:

$ klee --version
KLEE 1.4.0.0 (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: TRUE)
  Build revision: unknown

LLVM (http://llvm.org/):
  LLVM version 3.4
  
  Optimized build.
  Built Mar  5 2014 (17:05:10).
  Default target: x86_64-pc-linux-gnu
  Host CPU: x86-64
$ klee --posix-runtime --libc=uclibc test.bc 
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 42752912) at /home/klee/klee_src/runtime/POSIX/fd.c:1044
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /home/klee/klee_build/klee-uclibc/libc/string/strlen.c:22: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 5156
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

[251]

I can't reproduce it neither on my machine nor on Docker's klee/klee:latest. Could you please attach the assembly.ll file?

[moyix]

Hmm, we tested it in klee/klee:latest as well as building the dockerfile for the head commit. Here's the
assembly.ll.

The compile command for the test case was:

clang -c -g -emit-llvm test.c -o test.bc

[251]

I couldn't observe it as I have an alias that uses the recommended compilation flags: -g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__. With -O1 it finds the bug...

[ccadar]

I also tried this quickly with KLEE and it finds the bug, even w/o -O1.
@251 can you reproduce it w/o -O1?

[251]

@ccadar Yes, same KLEE version as above¹ against LLVM 11.1.0.

¹ also ran some slightly older versions - same result

[moyix]

Yep, can confirm that with -O1 KLEE detects the UAF correctly:

klee@a29f498923ce:~$ clang -O1 -c -g -emit-llvm test.c -o test.bc
klee@a29f498923ce:~$ klee --posix-runtime --libc=uclibc test.bc
KLEE: NOTE: Using POSIX model: /tmp/klee_build90stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build90stp_z3/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/klee-out-13"
KLEE: Using STP solver backend
warning: Linking two modules of different target triples: test.bc' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'

KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94482344996992) at klee_src/runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: ERROR: libc/string/strlen.c:22: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 13146
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

Edit: Although presumably -O1 is just hiding some underlying KLEE bug? Is there a fundamental reason why this can't be detected in unoptimized code?

[251]

My quick guess after dumping the addresses:

allocation at ...
free: 0x55a776531130
puts: 0x55a776531130
allocation at ...
allocation at 0x55a776531130 <- re-allocated

The memory is freed but an allocation afterwards gets the same address, hence it's "valid". With a different allocator (--allocate-determ) that relies on incrementing addresses in an mmap it doesn't happen (also when you change the size from 2 to something less common, e.g. 42).

[ccadar]

Edit: Although presumably -O1 is just hiding some underlying KLEE bug? Is there a fundamental reason why this can't be detected in unoptimized code?

@moyix Yes, this is a more fundamental issue, which is incidentally triggered here by the optimization level. Note that KLEE was not designed to reliably catch UAF bugs in its default configuration. If you want to reliably catch them, you should use --allocate-determ (but this is really bad in terms of memory consumption). We are actually working in the group on a better solution, and I hope to see it integrated into KLEE 2.3, or at least 2.4.

[ccadar]

@251 looks like our messages crossed, or at least I only noticed yours after submitting mine.
Now we only need to integrate the solution I mentioned into the mainline ;)

[moyix]

Got it :) I guess another workaround might be to use some kind of dangling pointer sanitizer in conjunction with KLEE? (I don't know exactly how those would interact with KLEE though.)

[ccadar]

Indeed, one would have to be careful with the integration, as UAF detection techniques are likely to directly interfere with KLEE's memory model.

[Hanseltu]

Hi,

Following the above comments, may I add one more case that makes KLEE miss the UAF detection? The problem is why KLEE treats differently on char and wchar_t data types when encountering UAF. Please check the following code for more detail.

char-test.c (reduced from CWE416_Use_After_Free__malloc_free_char_01.c)

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
int main(){
    char * data = NULL;
    data = (char *)malloc(100*sizeof(char));
    if (data == NULL) {exit(-1);}
    memset(data, 'A', 100-1);
    data[100-1] = '\0';
    free(data);
    printf("%s\n", data);
}

wchar-test.c (reduced from CWE416_Use_After_Free__malloc_free_wchar_t_01.c)

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <wchar.h>
int main(){
    wchar_t * data = NULL;
    data = (wchar_t *)malloc(100*sizeof(wchar_t));
    if (data == NULL) {exit(-1);}
    wmemset(data, L'A', 100-1);
    data[100-1] = L'\0';
    free(data);
    wprintf(L"%ls\n", data);
}

I guess the only difference between them comes from the different definitions of data variable types, but why does KLEE miss the detection of the UAF in char-test.c?

$klee/examples/uaf$ clang -emit-llvm -c char-test.c 
$klee/examples/uaf$ klee --libc=uclibc --posix-runtime char-test.bc 
KLEE: output directory is "/home/haoxin/disk-smu/research/klee-env/klee/examples/uaf/klee-out-8"
KLEE: Using STP solver backend
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 93825035161248) at runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(93825034506464, 93825006275520) at [no debug info]
�NhWUU

KLEE: done: total instructions = 14906
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 1

$klee/examples/uaf$ clang -emit-llvm -c wchar-test.c 
$klee/examples/uaf$ klee --libc=uclibc --posix-runtime wchar-test.bc 
KLEE: output directory is "/home/haoxin/disk-smu/research/klee-env/klee/examples/uaf/klee-out-9"
KLEE: Using STP solver backend
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 93825035767408) at runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: ERROR: libc/string/strnlen.c:30: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 21114
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

Please kindly note that when adding the option -O1 to compile char-test.c, then KLEE can detect this error. Adding --allocate-determ when executing KLEE on the unoptimized bc file still can not detect it. (which is different from the previous comment in the earlier reported case). I tested them in KLEE-2.3 and KLEE-2.1 (all built with LLVM-9.0), and they behave the same.

So, I am so confused about why KLEE can not detect the UAF in char-test.c. Is this the same fundamental issue mentioned [before] (#1434 (comment)) (I guess not as the --allocate-determ can not add any help)? Or are there any other issues hidden in KLEE?

Thanks for your help!
Haoxin

[251]

IIRC KLEE does not check the arguments to external calls (printf). In the case of wchar-test.c the compiler actually inserts a call to wprintf, which is an internal call. While executing it, KLEE reaches a strlen and reports an error.

Edit: check the last section in https://github.com/klee/klee-uclibc/