diff --git a/docs/index.md b/docs/index.md index d5a9e2d7..25d26813 100644 --- a/docs/index.md +++ b/docs/index.md @@ -35,6 +35,7 @@ slug: documentation 2. [Second tutorial]({{site.baseurl}}/tutorials/testing-regex/): Testing a simple regular expression library. 3. [Using a symbolic environment]({{site.baseurl}}/tutorials/using-symbolic/): Guide with examples on how to use the symbolic environment such as symbolic files and command-line arguments for the program under test. 4. [Testing Coreutils]({{site.baseurl}}/tutorials/testing-coreutils/): In-depth description of how to use KLEE to test GNU Coreutils. +5. [Using UBSan]({{site.baseurl}}/tutorials/using-ubsan/): An example of how KLEE can be leveraged alongside the UBSan instrumentation framework built in to compilers like `clang` ## External Resources diff --git a/docs/options.md b/docs/options.md index 568b9956..8623b15f 100644 --- a/docs/options.md +++ b/docs/options.md @@ -287,3 +287,16 @@ helper and helper2, can be done with the following command: {% highlight bash %} $ klee -link-llvm-lib=libhelper.so.bc -link-llvm-lib=libhelper2.so.bc test.bc {% endhighlight %} + +## UBSan Runtime + +KLEE includes handlers for the UBSan function calls inserted by `clang` during the compilation process. This runtime can +be enabled by passing the `--ubsan-runtime` flag. A tutorial that concerns this functionality exists +[here]({{site.baseurl}}/tutorials/using-ubsan/). + +Please note that the following checks are not supported: + +* `-fsanitize=local-bounds` +* `-fsanitize=function` +* `-fsanitize=objc-cast` +* `-fsanitize=vptr` diff --git a/tutorials/using-ubsan.md b/tutorials/using-ubsan.md new file mode 100644 index 00000000..47e3428e --- /dev/null +++ b/tutorials/using-ubsan.md @@ -0,0 +1,116 @@ +--- +layout: default +title: UBSan +subtitle: Taking Advantage of The Undefined Behavior Sanitizer +slug: documentation +--- +KLEE introduced handlers for the UBSan runtime calls inserted by the LLVM Undefined Behavior Sanitizer in +[release 3.0](https://github.com/klee/klee/releases#release-v3.0). This functionality is intended to supplement the checks +that KLEE already includes internally to detect division by zero and overshift overflow (KLEE can reliably detect these +specific behaviors, since they are visible without viewing the source-language metadata) as well as the undefined behavior +that will be located by KLEE during the symbolic execution phase itself. It is profitable for KLEE to utilize the UBSan +instrumentation machinery implemented by the LLVM frontend itself as certain checks, such as signed integer overflow and +locating misaligned pointers, require information that is absent or ambiguous in the LLVM IR itself, such as whether an +integer operation originated from a signed type to provide an accurate determination. This tutorial provides an example +of a basic C program that exhibits signed integer overflow and demonstrates how KLEE is capable of catching this behavior +should the program be compiled with the appropriate UBSan flags. + +Let us consider the following program 'badDivision.c': +{% highlight c %} +#include +#include +#include + +#include + +double noUB(void) { + double a = 85.3; + double b = 19.8; + double c = 0.11; + return (-b + sqrt(b*b - 4*a*c)) / (2*a); +} + +static int signed_division_overflow(void) { + int x; + int y; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(y), "y"); + + return x / y; + } + +int main(void) { + unsigned path; + + klee_make_symbolic(&path, sizeof(path), "path"); + klee_assume(path <= 1); + + switch (path) { + case 0: + printf("clean path: %lf\n", noUB()); + break; + case 1: + signed_division_overflow(); + printf("A valid division operation occurred in this path!\n"); + break; + } + + return 0; +} +{% endhighlight %} + +# Compiling The Program + +If one wishes to take advantage of the UBSan handlers in KLEE, it is first compulsory to enable UBSan instrumentation +within the appropriate LLVM frontend during the compilation process itself. Considering C, one can enable this with the +`-fsanitize` flag in `clang`. In this case, we only enable instrumentation for signed division overflow with the +`-fsanitize=signed-integer-overflow` flag, though one can enable most checks by utilizing the `-fsanitize=undefined` +flag (it enables Clang’s standard subset of undefined-behavior checks, though omits checks such as unsigned integer +overflow and implicit conversions). Additional details regarding UBSan and its specific checks can be found [here](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html). + + +Command to compile our example program: +{% highlight bash %} +$ clang -c -g -O0 -Xclang -disable-O0-optnone -emit-llvm -fsanitize=signed-integer-overflow ./badDivision.c -o ./badDivision.bc +{% endhighlight %} + +# Demonstrating The UBSan Handlers Found In KLEE + +When we execute this program with KLEE, we can see that the path that contains signed division overflow causes KLEE to +throw an error and terminate the offending execution state. Please note that the flag `--ubsan-runtime` is required to +enable KLEE's UBSan handlers. +{% highlight bash %} +$ klee --libc=uclibc --ubsan-runtime --posix-runtime ./badDivision.bc +KLEE: NOTE: Using POSIX model: /tmp/klee_build130stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca +KLEE: NOTE: Using klee-uclibc : /tmp/klee_build130stp_z3/runtime/lib/klee-uclibc.bca +KLEE: output directory is "/home/klee/klee_ubsan_test/./klee-out-0" +KLEE: Using STP solver backend +KLEE: SAT solver: MiniSat +KLEE: Deterministic allocator: Using quarantine queue size 8 +KLEE: Deterministic allocator: globals (start-address=0x7f40af200000 size=10 GiB) +KLEE: Deterministic allocator: constants (start-address=0x7f3e2f200000 size=10 GiB) +KLEE: Deterministic allocator: heap (start-address=0x7e3e2f200000 size=1024 GiB) +KLEE: Deterministic allocator: stack (start-address=0x7e1e2f200000 size=128 GiB) +KLEE: WARNING: undefined reference to function: sqrt +KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 132543126962176) at klee_src/runtime/POSIX/fd.c:997 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: ./badDivision.c:21: divide by zero +KLEE: NOTE: now ignoring this error at this location +KLEE: WARNING ONCE: calling external: sqrt(4644944186881844708) at ./badDivision.c:11 14 +KLEE: WARNING ONCE: calling external: printf(133741053739008) at ./badDivision.c:37 5 +A valid division operation occurred in this path! +clean path: -0.005695 +KLEE: ERROR: klee_src/runtime/Sanitizer/ubsan/ubsan_handlers.cpp:37: integer division overflow +KLEE: NOTE: now ignoring this error at this location + +KLEE: done: total instructions = 13532 +KLEE: done: completed paths = 2 +KLEE: done: partially completed paths = 2 +KLEE: done: generated tests = 4 +{% endhighlight %} + +Notice that the two invalid cases are detected differently. Division by zero is detected directly by KLEE while +interpreting the LLVM division instruction, whereas signed division overflow is reported through the UBSan handler +inserted by Clang.