Skip to content
Snippets Groups Projects
Select Git revision
  • 9a503050c35f4de4a7b28560028b99416982854f
  • master default protected
  • klee-args
  • stable
4 results

cargo-klee

Forked from Per Lindgren / cargo-klee
23 commits behind the upstream repository.
Per Lindgren's avatar
Per Lindgren authored
9a503050
History

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. 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 of ksymbol!(&mut T, &str) for making declared variables symbolic.