cargo klee
to compile Rust crates for KLEE analysis
Cargo subcommand KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generetes test cases aiming to cover (all) reachable paths of the input program. The KLEE run-time infers further checks for common program errors, e.g., out of bounds indexing and division by zero. Rust as being designed for safety, catches such errors and panics in precence of such faults. For analysis, a Rust panic
implies an abort
, which is detected as an error by KLEE, thus our klee
tool spots potential panicing behavior of the application at hand.
In effect, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopordizing memory safety and robustnes for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficent to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be
ensured by adding assertions to the source. If those assertions are condititonally compiled (e.g. under a klee-analysis
feature) the assertions (and their implied overhead) will be omitted in a production build.
Requirements
- LLVM KLEE installed from recent package
- LLVM llc and clang for building replay binaries
- GNU gdb for executing replay binaries
- nightly toolchain (edition-2018)
The klee
tool needs to installed and accissible in path. The tool has been tested on a
the master branch of KLEE (https://github.com/klee/klee) as of Sun Nov 25 14:57:29 CET 2018, built under arch linux with the system LLVM (v7) using a modified aur recepie (https://aur.archlinux.org/packages/klee/), altered to refer source
to the KLEE master branch.
TODO
Currently only native KLEE is supported, we need to build a new docker with recent KLEE first in order to re-enable docker usage.
A Rust no_std
application under linux will use the target triple x86_64-unknown-linux-gnu
while KLEE uses the target triple x86_64-pc-linux-gnu
, which renders a KLEE warning. To the best of our understanding both refers to the same (ABI) and thus the warning can be safely ignored.
If the code under analysis is targeting another architecture (e.g., with other byte order or pointer size) the KLEE run-time system should be compiled for the target architecture to ensure complience in between analysis and production code behavior. An ergonomic way of re-targeting KLEE has yet not been investigated. (This is not a Rust klee
issue per-se, but rather a possible feature for further KLEE development.)
usage
$ systemctl start docker.service # if not already started/enabled, docker is optional
$ cargo install --path cargo-klee # add -f, if already installed
$ cd klee-examples
$ cargo klee --example foo --release
KLEE: output directory is "/home/pln/rust/klee/klee-examples/target/release/examples/klee-out-0"
KLEE: Using Z3 solver backend
warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-pc-linux-gnu' whereas 'target/release/examples/foo-cda2f387c054965f.ll' is 'x86_64-unknown-linux-gnu'
KLEE: ERROR: /home/pln/rust/klee/src/lang_items.rs:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 22
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
KLEE generates two test cases, we can view them by:
$ ktest-tool target/release/examples/klee-last/test000001.ktest
ktest file : 'target/release/examples/klee-last/test000001.ktest'
args : ['target/release/examples/foo-cda2f387c054965f.ll']
num objects: 1
object 0: name: b'u'
object 0: size: 1
object 0: data: b'\xff'
$ ktest-tool target/release/examples/klee-last/test000002.ktest
ktest file : 'target/release/examples/klee-last/test000002.ktest'
args : ['target/release/examples/foo-cda2f387c054965f.ll']
num objects: 1
object 0: name: b'u'
object 0: size: 1
object 0: data: b'\x00'
The first test triggers an error, we can view details by:
$ more target/release/examples/klee-last/test000001.abort.err
Error: abort failure
File: /home/pln/rust/klee/src/lang_items.rs
Line: 6
assembly.ll line: 49
Stack:
#000000049 in _ZN4core9panicking9panic_fmt17h8e7152a45a601b4bE () at /home/pln/rust/klee/src/lang_items.rs:6
#100000055 in _ZN4core9panicking5panic17h9a94013c5e0723bbE () at /rustc/edaac35d67bed09260dc0c318acc5212fb66246e/src/libcore/panicking.rs:52
#200000023 in main () at /home/pln/rust/klee/klee-examples/examples/foo.rs:24
In this case it is the Rust built in division by zero detection that causes a panic!
.
The error found is at line 24.
#![no_std]
#![no_main]
#[macro_use]
extern crate klee;
use core::ptr;
#[no_mangle]
fn main() {
let u = ksymbol!("u");
unsafe {
ptr::read_volatile(&f2(f1(u)));
}
}
// add 1 wrapping
fn f1(u: u8) -> u8 {
u.wrapping_add(1)
}
fn f2(u: u8) -> u8 {
100 / u // <- Rust div 0 panic!
}
The application is compiled for #[no_std]
(thus isolating the application to dependencies of the environment). extern crate klee
gives us access to the klee
bindings. ksymbol
marks the variable u
as symbolic (unknown). read_volatile(&T)
ensures that T
is computed (and thus prevents the corresesponding code from being optimized out by the compiler).
Examples
Further examples is found in the klee-examples
directory.
-
foo
, shows the above example. -
foo2
, shows further use ofksymbol!(&mut T, &str)
for making declared variables symbolic.