Software Verification and Validation

Here you'll find the laboratories for the Software Verification and Validation Course.

Symbolic Execution with Klee and Angr

Today we will use two amazing tools from the world of symbolic execution: Klee and Angr.

Before starting to work on the lab we recommend going over the Klee paper - OSDI 2008.

KLEE Tutorial: Testing a Simple Function

Before starting, make sure you install Klee.

This tutorial walks you through the main steps needed to test a simple function with KLEE. Here is our simple function:

// get_sign.c
// Simple function we want to execute symbolically
int get_sign(int x) {
  if (x == 0)
     return 0;
  
  if (x < 0)
     return -1;
  else 
     return 1;
} 

int main() {
  int a;
  return get_sign(a);
}

Marking input as symbolic

In order to test this function with KLEE, we need to run it on symbolic input. To mark a variable as symbolic, we use the klee_make_symbolic() function (defined in klee/klee.h), which takes three arguments: the address of the variable (memory location) that we want to treat as symbolic, its size, and a name (which can be anything). Here is a simple main() function that marks a variable a as symbolic and uses it to call get_sign():

#include "klee/klee.h"

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

Compiling to LLVM bitcode

KLEE operates on LLVM bitcode. To run a program with KLEE, you first compile it to LLVM bitcode using clang -emit-llvm.

Want to find more about LLVM bitecode? Check out this resource.

# You can clone this repo https://github.com/klee/klee
# and include the path as -I klee/include
clang -I /path/to/klee.h -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

which should create a get_sign.bc file in LLVM bitcode format. The -I argument is used so that the compiler can find klee/klee.h, which contains definitions for the intrinsic functions used to interact with the KLEE virtual machine, such as klee_make_symbolic. It is useful to build with -g to add debug information to the bitcode file, which we use to generate source line level statistics information.

The bitcode passed to KLEE should not be optimised, because we hand-picked the correct optimisations for KLEE which can be enabled with KLEE's --optimize command line option. However, in newer LLVM versions (> 5.0) the -O0 zero flag should NOT be used when compiling for KLEE as it prevents KLEE from doing its own optimisations. -O0 -Xclang -disable-O0-optnone should be used instead.

If you do not wish to replay the test cases as described later and don't care about debug information and optimisation, you can delete the klee/klee.h include and then compile get_sign.c with:

$ clang -emit-llvm -c get_sign.c

However, we recommend using the longer command above.

Running KLEE

To run KLEE on the bitcode file simply execute:

$ klee get_sign.bc

You should see the following output:

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3

There are three paths through our simple function, one where a is 0, one where it is less than 0 and one where it is greater than 0. As expected, KLEE informs us that it explored three paths in the program and generated one test case for each path explored.

For larger programs, KLEE might not be able to explore each path to its end due to time or memory constraints. In that case, it also informs us about the number of interrupted (partially completed) paths.

The output of a KLEE execution is a directory (in our case klee-out-0) containing the test cases generated by KLEE. KLEE names the output directory klee-out-N where N is the lowest available number (so if we run KLEE again it will create a directory called klee-out-1), and also generates a symbolic link called klee-last to this directory for convenience:

$ ls klee-last/
assembly.ll      run.istats       test000002.ktest
info             run.stats        test000003.ktest
messages.txt     test000001.ktest warnings.txt

KLEE-generated test cases

Test cases generated by KLEE are written into files with .ktest extension. These are binary files which can be read with the ktest-tool utility. ktest-tool outputs different representations for the same object, for instance Python byte strings (data), integers (int) or ascii text (text). So let's examine each file:

$ ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

$ ktest-tool klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x01\x01\x01\x01'
object 0: hex : 0x01010101
object 0: int : 16843009
object 0: uint: 16843009
object 0: text: ....

$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

In each test file, KLEE reports the arguments with which the program was invoked (in our case no arguments other than the program name itself), the number of symbolic objects on that path (only one in our case), the name of our symbolic object ('a') and its size (4). The actual test itself is represented by the value of our input: 0 for the first test, 16843009 for the second and -2147483648 for the last one. As expected, KLEE generated value 0, one positive value (16843009), and one negative value (-2147483648). We can now run these values on a native version of our program to exercise all paths through the code!

Replaying a test case

While we can run the test cases generated by KLEE on our program by hand, (or with the help of an existing test infrastructure), KLEE provides a convenient replay library, which simply replaces the call to klee_make_symbolic with a call to a function that assigns to our input the value stored in the .ktest file. To use it, simply link your program with the libkleeRuntest library and set the KTEST_FILE environment variable to point to the name of the desired test case:

$ export LD_LIBRARY_PATH=path-to-klee-build-dir/lib/:$LD_LIBRARY_PATH
$ gcc -I ../../include -L path-to-klee-build-dir/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-last/test000001.ktest ./a.out
$ echo $?
0
$ KTEST_FILE=klee-last/test000002.ktest ./a.out
$ echo $?
1
$ KTEST_FILE=klee-last/test000003.ktest ./a.out
$ echo $?
255

As expected, our program returns 0 when running the first test case, 1 when running the second one, and 255 (-1 converted to a valid exit code value in the 0-255 range) when running the last one.

Acknowledgement. This tutorial is based on this Klee tutorial.

Testing a Regular Expression Matcher with KLEE

This is an example of using KLEE to test a simple regular expression matching function.

We start simple regular expression matching function, and the bare bones testing harness (in main()) needed to explore this code with KLEE.

// Regexp.c
#include "klee/klee.h"
static int matchhere(char*,char*);

static int matchstar(int c, char *re, char *text) {
  do {
    if (matchhere(re, text))
      return 1;
  } while (*text != '\0' && (*text++ == c || c== '.'));
  return 0;
}

static int matchhere(char *re, char *text) {
  if (re[0] == '\0')
     return 0;
  if (re[1] == '*')
    return matchstar(re[0], re+2, text);
  if (re[0] == '$' && re[1]=='\0')
    return *text == '\0';
  if (*text!='\0' && (re[0]=='.' || re[0]==*text))
    return matchhere(re+1, text+1);
  return 0;
}

int match(char *re, char *text) {
  if (re[0] == '^')
    return matchhere(re+1, text);
  do {
    if (matchhere(re, text))
      return 1;
  } while (*text++ != '\0');
  return 0;
}

// The size of the buffer to test with.
#define SIZE 7

int main() {
  // The input regular expression.
  char re[SIZE];
  
  // Make the input symbolic. 
  klee_make_symbolic(re, sizeof re, "re");

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

This example shows how to build and run the example using KLEE, as well as how to interpret the output, and some additional KLEE features that can be used when writing a test driver by hand.

We'll start by showing how to build and run the example, and then explain how the test harness works in more detail.

Building the example

The first step is to compile the source code using a compiler which can generate object files in LLVM bitcode format.

# Check the previous section.
$ clang -I /path/to/klee/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c

which should create a Regexp.bc file in LLVM bitcode format. The -I argument is used so that the compiler can find klee/klee.h, which contains definitions for the intrinsic functions used to interact with the KLEE virtual machine. -c is used because we only want to compile the code to an object file (not to a native executable), and finally -g causes additional debug information to be stored in the object file, which KLEE will use to determine source line number information. -O0 -Xclang -disable-O0-optnone is used to compile without any optimisation, but without preventing KLEE from performing its own optimisations, which compiling with -O0 would.

If you have the LLVM tools installed in your path, you can verify that this step worked by running llvm-nm on the generated file:

$ llvm-nm Regexp.bc
                 U klee_make_symbolic
---------------- T main
---------------- T match
---------------- t matchhere
---------------- t matchstar

Normally, before running this program, we would need to link it to create a native executable. However, KLEE runs directly on LLVM bitcode files. Since this program only has a single file there is no need for linking. For "real" programs with multiple inputs, the llvm-link tools can be used in place of the regular link step to merge multiple LLVM bitcode files into a single module which can be executed by KLEE.

Executing the code with KLEE

The next step is to execute the code with KLEE (number of instructions varies between LLVM versions and optimisation levels):

$ klee --only-output-states-covering-new Regexp.bc
KLEE: output directory = "klee-out-0"
KLEE: ERROR: Regexp.c:23: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: Regexp.c:25: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 4848112
KLEE: done: completed paths = 6675
KLEE: done: partially completed paths = 763
KLEE: done: generated tests = 16

On startup, KLEE prints the directory used to store output (in this case klee-out-0). By default KLEE will use the first free klee-out-N directory and also create a klee-last symlink which will point to the most recent created directory. You can specify a directory to use for outputs using the -output-dir=path command line argument.

While KLEE is running, it will print status messages for "important" events, for example when it finds an error in the program. In this case, KLEE detected two invalid memory accesses on lines 23 and 25 of our test program. We'll look closer at this in a moment.

Finally, when KLEE finishes execution it prints out a few statistics about the run. Here we see that KLEE executed a total of ~4.8 million instructions, explored 7,438 paths, and generated 16 test cases. KLEE only generates 16 test cases because we limited the test generation to states that actually covered new code with --only-output-states-covering-new. If we would omit this flag, KLEE would create 6,677 test cases! Still, KLEE does not create a test case for every path. Whenever it finds a bug, it creates a test case for the first state that reaches the bug. All other paths that reach the bug at the same location are terminated silently and reported as partially completed paths. If you don't mind the duplication of error cases, use --emit-all-errors to generate test cases for all 7,438 paths.

Note that many realistic programs have an infinite (or extremely large) number of paths through them, and it is common that KLEE will not terminate. By default KLEE will run until the user presses Control-C (i.e. klee gets a SIGINT), but there are additional options to limit KLEE's runtime and memory usage:

-max-time=<time span>: Halt execution after the given amount of time, e.g. 10min or 1h5s.
-max-forks=N: Stop forking after N symbolic branches, and run the remaining paths to termination.
-max-memory=N: Try to limit memory consumption to N megabytes.

KLEE error reports

When KLEE detects an error in the program being executed it will generate a test case which exhibits the error, and write some additional information about the error into a file testN.TYPE.err, where N is the test case number, and TYPE identifies the kind of error. Some types of errors KLEE detects include:

ptr: Stores or loads of invalid memory locations.
free: Double or invalid free().
abort: The program called abort().
assert: An assertion failed.
div: A division or modulus by zero was detected.
user: There is a problem with the input (invalid klee intrinsic calls) or the way KLEE is being used.
exec: There was a problem which prevented KLEE from executing the program; for example an unknown instruction, a call to an invalid function pointer, or inline assembly.
model: KLEE was unable to keep full precision and is only exploring parts of the program state. For example, symbolic sizes to malloc are not currently supported, in such cases KLEE will concretize the argument.

KLEE will print a message to the console when it detects an error, in the test run above we can see that KLEE detected two memory errors. For all program errors, KLEE will write a simple backtrace into the .err file. This is what one of the errors above looks like:

Error: memory error: out of bound pointer
File: .../klee/examples/regexp/Regexp.c
Line: 23
Stack:
  #0 00000146 in matchhere (re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:23
  #1 00000074 in matchstar (c, re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #2 00000172 in matchhere (re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #3 00000074 in matchstar (c, re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #4 00000172 in matchhere (re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #5 00000074 in matchstar (c, re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #6 00000172 in matchhere (re=14816465, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #7 00000231 in matchhere (re=14816464, text=14815300) at .../klee/examples/regexp/Regexp.c:30
  #8 00000280 in match (re=14816464, text=14815296) at .../klee/examples/regexp/Regexp.c:38
  #9 00000327 in main () at .../klee/examples/regexp/Regexp.c:59
Info:
  address: 14816471
  next: object at 14816624 of size 4
  prev: object at 14816464 of size 7

Each line of the backtrace lists the frame number, the instruction line (this is the line number in the assembly.ll file found along with the run output), the function and arguments (including values for the concrete parameters), and the source information.

Particular error reports may also include additional information. For memory errors, KLEE will show the invalid address, and what objects are on the heap both before and after that address. In this case, we can see that the address happens to be exactly one byte past the end of the previous object.

Changing the test harness

The reason KLEE is finding memory errors in this program isn't because the regular expression functions have a bug, rather it indicates a problem in our test driver. The problem is that we are making the input regular expression buffer completely symbolic, but the match function expects it to be a null terminated string. Let's look at two ways we can fix this.

The simplest way to fix this problem is to store '\0' at the end of the buffer, after making it symbolic. This makes our driver look like this:

int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  re[SIZE - 1] = '\0';

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

Making a buffer symbolic just initializes the contents to refer to symbolic variables, we are still free to modify the memory as we wish. If you recompile and run klee on this test program, the memory errors should now be gone.

Another way to accomplish the same effect is to use the klee_assume intrinsic function. klee_assume takes a single argument (an unsigned integer) which generally should be some kind of conditional expression, and "assumes" that expression to be true on the current path (if that can never happen, i.e. the expression is provably false, KLEE will report an error).

We can use klee_assume to cause KLEE to only explore states where the string is null terminated by writing the driver like this:

int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  klee_assume(re[SIZE - 1] == '\0');

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

In this particular example both solutions work fine but in general klee_assume is more flexible:

By explicitly declaring the constraint, this will force test cases to have the '\0' in them. In the first example where we write the terminating null explicitly, it doesn't matter what the last byte of the symbolic input is and KLEE is free to generate any value. In some cases where you want to inspect the test cases by hand, it is more convenient for the test case to show all the values that matter.
klee_assume can be used to encode more complicated constraints. For example, we could use klee_assume(re[0] != '^') to cause KLEE to only explore states where the first byte is not '^'.

There is one important caveat when using klee_assume with multiple conditions. Remember that boolean conditionals like '&&' and '||' may be compiled into code which branches before computing the result of the expression. In such situations KLEE will branch the process before it reaches the call to klee_assume, which may result in exploring unnecessary additional states. For this reason it is good to use as simple expressions as possible to klee_assume (for example splitting a single call into multiple ones), and to use the '&' and '|' operators instead of the short-circuiting ones.

Acknowledgement. This tutorial is based on this Klee tutorial.

Binary Analysis

angr is a multi-architecture binary analysis toolkit, with the capability to perform dynamic symbolic execution (like Mayhem, KLEE, etc.) and various static analyses on binaries.

Installing angr is quite simple, you may find a guide here.

First Steps

Once you have angr installed, please look over this first example and run it. This is a basic script that explains how to use angr to symbolically execute a program and produce concrete input satisfying certain conditions.

Explore at your own peace

Today's task is to go through some of the examples from here. You may pick examples you find interesting.