Cargo subcommand cargo klee to compile Rust crates for KLEE analysis
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. KLEE 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, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time, and thus 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), tested with nightly-2019-01-25-x86_64-unknown-linux-gnu
The klee tool needs to installed and accissible in path. The tool has been tested on 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
$ cargo install --path cargo-klee # add -f, if already installed
$ cd klee-examples
$ cargo klee --help
cargo-klee 0.2.0
Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>
KLEE analysis of Rust application
USAGE:
cargo-klee [FLAGS] [OPTIONS] --bin <NAME> --example <NAME>
FLAGS:
--all-features Activate all available features
-g, --gdb Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the
`gdb` working directory, if unset `gdb` will execute in the current working directory
-h, --help Prints help information
-k, --klee Run KLEE test generatation [default enabled unless --replay]
--release Build artifacts in release mode, with optimizations
-r, --replay Generate replay binary in target directory
-V, --version Prints version information
-v, --verbose Use verbose output
OPTIONS:
--bin <NAME> Build only the specified binary
--example <NAME> Build only the specified example
--features <FEATURES> Space-separated list of features to activate
$ cargo klee --bin foo --release
....
KLEE: output directory is "/home/pln/rust/cargo-klee/klee-examples/target/release/deps/klee-out-5"
KLEE: Using Z3 solver backend
KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 10
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2You may analyse code using either --bin and --examples. See src/foo.rs for a complete example for analysis and replay functionality.