Using KLEE

KLEE logo One of the most straightforward and most solid automatic verification tools is the KLEE symbolic execution tool that can be used to search for bugs in programs. KLEE was originally developed for C but, because KLEE and the Rust compiler are both based on the LLVM platform, it is possible to use KLEE with Rust programs.

The steps involved in using KLEE to verify Rust programs are:

Compile the program to generate LLVM bitcode.
Run KLEE on the bitcode file.
Examine the output of KLEE.

With minor variations, it should be possible to adapt the basic steps of compiling Rust programs to generate LLVM for use with other LLVM-based verification tools.

Note: The recommended way to use KLEE is with the propverify library and the cargo-verify script as described here. This note describes how to use the KLEE directly in case you wonder how cargo-verify works or want to add support for a different tool. This is going to be a fairly low-level description and most people will be happier not knowing how the sausage is made. (Since there are so many low-level details, there is a risk that we will forget to update this document so you may have to use the source.)

A small test program

As a running example, we will use the same example that we used to explain how to use the verification-annotations crate.

This code is in demos/simple/klee/src/main.rs and the shell commands in this file are in demos/simple/klee/verify.sh.

use verification_annotations::prelude::*;

fn main() {
    let a = u32::abstract_value();
    let b = u32::abstract_value();
    verifier::assume(1 <= a && a <= 1000);
    verifier::assume(1 <= b && b <= 1000);
    if verifier::is_replay() {
        eprintln!("Test values: a = {}, b = {}", a, b);
    }
    let r = a*b;
    verifier::assert!(1 <= r && r < 1000000);
}

The Rust compiler and KLEE are in the Dockerfile so start the Docker image by running

docker/run
cd demos/simple/klee

All remaining commands in this file will be run in this docker image.

(It is usually easiest to run this in one terminal while using a separate editor to edit the files in another terminal.)

Compiling Rust for verification

The Rust compiler works in four stages: first, it compiles Rust source code to HIR (the high-level IR); HIR is converted to MIR (the mid-level IR); MIR is converted to LLVM IR (the low-level virtual machine IR); and, finally, it compiles LLVM IR down to machine code and links the result.

When using an LLVM-based tool like KLEE, we need to modify this behaviour so that the LLVM IR is linked and saved to a file. This can be done by passing extra flags to rustc when using cargo to instruct rustc to link the bitcode files.

export RUSTFLAGS="-Clto -Cembed-bitcode=yes --emit=llvm-bc $RUSTFLAGS"

We also have to pass some configuration flags to cargo and rustc to configure the verification-annotations crate correctly.

export RUSTFLAGS="--cfg=verify $RUSTFLAGS"

Our goal is to find bugs so we turn on some additional error checking in the compiled code to detect arithmetic overflows.

export RUSTFLAGS="-Warithmetic-overflow -Coverflow-checks=yes $RUSTFLAGS"

And, when we find a bug, we want to report it as efficiently as possible so we make sure that the program will abort if it panics.

export RUSTFLAGS="-Zpanic_abort_tests -Cpanic=abort $RUSTFLAGS"

With all those definitions, we can now run

cargo build --features=verifier-klee

Depending on which platform you are running on, the resulting LLVM bitcode file may be placed placed in target/debug/deps/try-klee.bc (OSX) or in a file with a name like target/debug/deps/try_klee-6136b0f50ac42b91.bc (Linux). At least for simple cases, we can refer to both files as target/debug/deps/try_klee*.bc and not worry about the exact filename.

The above should have worked. But, if it produced a linking error involving -lkleeRuntest you may have to point the linker at the directory where the KLEE library was installed. For example, on OSX you might have installed it in $HOME/homebrew/lib and need to use this command

export RUSTFLAGS="-L$HOME/homebrew/lib -C link-args=-Wl,-rpath,$HOME/homebrew/lib $RUSTFLAGS"

Compiling large programs

Finally, on larger, more complex projects than this example, we have seen problems with the Rust compiler generating SSE instructions that KLEE does not support. We don’t have a complete solution for this but we have found that it helps to compile with a low (but non-zero) level of optimization, to disable more sophisticated optimizations and to disable SSE and AVX features.

export RUSTFLAGS="-Copt-level=1 $RUSTFLAGS"
export RUSTFLAGS="-Cno-vectorize-loops -Cno-vectorize-slp $RUSTFLAGS"
export RUSTFLAGS="-Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2 $RUSTFLAGS"

(This is not needed for our simple example.)

Running KLEE

Having built a bitcode file containing the program and all the libraries that it depends on, we can now run KLEE like this:

klee --libc=klee --silent-klee-assume --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc

This command will produce output like this

KLEE: output directory is "try-klee/kleeout"
KLEE: Using STP solver backend
... (possibly warnings about different target triples - probably benign)
KLEE: done: total instructions = 10153
KLEE: done: completed paths = 3
KLEE: done: generated tests = 1

(On OSX, it may also crash and produce a stack dump after producing that output?)

This shows that KLEE explored three paths through the above code, found one path that failed and generated one file containing inputs that can trigger that failing path. To find those input values, we look in the directory kleeout for files with names like test000001.ktest. These are binary files that can be examined using KLEE’s ktest-tool

$ ktest-tool kleeout/test000001.ktest
ktest file : 'kleeout/test000001.ktest'
args       : ['target/debug/deps/try_klee.bc']
num objects: 2

object 0: name: 'unnamed'
object 0: size: 4
object 0: data: b'\x01\x00\x00\x00'
object 0: hex : 0x01000000
object 0: int : 1
object 0: uint: 1
object 0: text: ....

object 1: name: 'unnamed'
object 1: size: 4
object 1: data: b'\x01\x00\x00\x00'
object 1: hex : 0x01000000
object 1: int : 1
object 1: uint: 1
object 1: text: ....

This shows that the program created two non-deterministic objects each called ‘unnamed` and each of size 4. KLEE does not know the way to interpret those so it displays for them several common interpretations.

Replaying the input values

When we compiled the program to produce LLVM bitcode, we also generated a conventional binary. We can run this in the normal way:

cargo run --features=verifier-klee

and KLEE will prompt us for the name of the input file

KLEE-RUNTIME: KTEST_FILE not set, please enter .ktest path:

Or, we can specify the input file when we invoke KLEE:

$ KTEST_FILE=kleeout/test000001.ktest cargo run --features=verifier-klee
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/try-klee`
Test values: a = 1, b = 1

This provides an easier way to view the test values chosen: using Rust’s builtin print function.

Handling larger programs

The instructions above work fine for small programs. But, as we tackle programs with dependencies, we need to add a few more flags to make it all work.

Compiling larger programs

If you add the following dependency on serde

serde = { version = "1.0", features = ["derive"] }

you will likely get a linking error

error: cannot prefer dynamic linking when performing LTO

The (incredibly obscure) workaround for this is to specify a target explicitly. (I have no idea why this helps!)

The first step is to figure out what target you are currently using. You want the “default host” reported by “rustup show”

$ rustup show | grep Default
Default host: x86_64-unknown-linux-gnu

Now that we know the target, we add --target to the cargo build command

cargo build --features=verifier-klee --target=x86_64-unknown-linux-gnu

Unfortunately, this changes where the final bitcode file is put. Instead of target/debug/deps/try_klee*.bc it is put in target/x86_64-unknown-linux-gnu/debug/deps/try_klee*.bc.

Using KLEE with larger programs

In the above, we used this command to invoke KLEE

klee --libc=klee --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc

Some additional flags that are worth using for larger examples are

--exit-on-error causes KLEE to exit as soon as it finds a problem. (KLEE’s default mode is to keep searching for more problems.)
--disable-verify works around a problem in KLEE caused by an interaction between debug information and inlining.

These flags are all added before the bitcode file like this

klee --output-dir=kleeout --warnings-only-to-file --exit-on-error \
     --libc=klee --silent-klee-assume --disable-verify \
     target/x86_64-unknown-linux-gnu/debug/deps/try_klee*.bc

[This post was originally posted as part of the Rust verification project]

Written on September 1, 2020.
The opinions expressed are my own views and not my employer's.