Skip to content
Snippets Groups Projects
Commit dffae9e1 authored by Per Lindgren's avatar Per Lindgren
Browse files

Merge branch 'master' of gitlab.henriktjader.com:pln/cargo-klee

parents 2f1186a1 9c2b272b
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
README.md
+ 37
− 85
View file @ dffae9e1
# Cargo subcommand `cargo klee` to compile Rust crates for KLEE analysis # 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. 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.
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 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. 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 ## Requirements
...@@ -10,10 +12,10 @@ ensured by adding assertions to the source. If those assertions are condititonal ...@@ -10,10 +12,10 @@ ensured by adding assertions to the source. If those assertions are condititonal
- LLVM KLEE installed from recent package - LLVM KLEE installed from recent package
- LLVM llc and clang for building replay binaries - LLVM llc and clang for building replay binaries
- GNU gdb for executing replay binaries - GNU gdb for executing replay binaries
- nightly toolchain (edition-2018) - 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 a 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.
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 ## TODO
...@@ -26,97 +28,47 @@ If the code under analysis is targeting another architecture (e.g., with other b ...@@ -26,97 +28,47 @@ If the code under analysis is targeting another architecture (e.g., with other b
## usage ## usage
``` console ``` console
$ systemctl start docker.service # if not already started/enabled, docker is optional
$ cargo install --path cargo-klee # add -f, if already installed $ cargo install --path cargo-klee # add -f, if already installed
$ cd klee-examples $ cd klee-examples
$ cargo klee --example foo --release $ cargo klee --help
cargo-klee 0.2.0
KLEE: output directory is "/home/pln/rust/klee/klee-examples/target/release/examples/klee-out-0" Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>
KLEE: Using Z3 solver backend KLEE analysis of Rust application
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 USAGE:
KLEE: done: completed paths = 2 cargo-klee [FLAGS] [OPTIONS] --bin <NAME> --example <NAME>
KLEE: done: generated tests = 2
```
KLEE generates two test cases, we can view them by: FLAGS:
--all-features Activate all available features
``` sh -g, --gdb Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the
$ ktest-tool target/release/examples/klee-last/test000001.ktest `gdb` working directory, if unset `gdb` will execute in the current working directory
ktest file : 'target/release/examples/klee-last/test000001.ktest' -h, --help Prints help information
args : ['target/release/examples/foo-cda2f387c054965f.ll'] -k, --klee Run KLEE test generatation [default enabled unless --replay]
num objects: 1 --release Build artifacts in release mode, with optimizations
object 0: name: b'u' -r, --replay Generate replay binary in target directory
object 0: size: 1 -V, --version Prints version information
object 0: data: b'\xff' -v, --verbose Use verbose output
$ 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: OPTIONS:
--bin <NAME> Build only the specified binary
``` sh --example <NAME> Build only the specified example
$ more target/release/examples/klee-last/test000001.abort.err --features <FEATURES> Space-separated list of features to activate
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. $ cargo klee --bin foo --release
``` rust ....
#![no_std]
#![no_main]
#[macro_use] KLEE: output directory is "/home/pln/rust/cargo-klee/klee-examples/target/release/deps/klee-out-5"
extern crate klee; 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
use core::ptr; KLEE: NOTE: now ignoring this error at this location
#[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 { KLEE: done: total instructions = 10
100 / u // <- Rust div 0 panic! KLEE: done: completed paths = 2
} KLEE: done: generated tests = 2
``` ```
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). You may analyse code using either `--bin` and `--examples`. See `src/foo.rs` for a complete example for analysis and replay functionality.
\ No newline at end of file
## 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.
\ No newline at end of file
klee-examples/src/foo.rs
+ 13
− 13
View file @ dffae9e1
//! Showcase how individual fields can be made symbolic //! Showcase how individual fields can be made symbolic
//! $ cargo klee --bin foo --release -r -k -g -v //! $ cargo klee --bin foo -r -k -g -v
//! ... //! ...
//! Reading symbols from register.replay...done. //! Reading symbols from register.replay...done.
//! //!
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest //! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
//! (gdb) run //! (gdb) run # for the generated test the program will run to end
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay
//! [Inferior 1 (process 25074) exited with code 01] //! [Inferior 1 (process 25074) exited with code 01]
//! //!
//! (gdb) set env KTEST_FILE=klee-last/test000002.ktest //! (gdb) set env KTEST_FILE=klee-last/test000002.ktest
//! (gdb) run //! (gdb) run # for the generated test the program will panic du to a division by zero, line 60
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay
//! //!
//! Program received signal SIGILL, Illegal instruction. //! Program received signal SIGILL, Illegal instruction.
//! rust_begin_unwind (_info=0x7fffffffd6a8) //! rust_begin_unwind (_info=0x7fffffffd9b8) at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31
//! at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31
//! 31 unsafe { intrinsics::abort() } //! 31 unsafe { intrinsics::abort() }
//!
//! (gdb) backtrace //! (gdb) backtrace
//! #0 rust_begin_unwind (_info=0x7fffffffd6a8) //! #0 rust_begin_unwind (_info=0x7fffffffd9b8) at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31
//! at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31 //! #1 0x000055555555530c in core::panicking::panic_fmt () at src/libcore/panicking.rs:85
//! #1 0x000055555555530c in core::panicking::panic_fmt ()
//! at src/libcore/panicking.rs:85
//! #2 0x000055555555538b in core::panicking::panic () at src/libcore/panicking.rs:49 //! #2 0x000055555555538b in core::panicking::panic () at src/libcore/panicking.rs:49
//! #3 0x0000555555555281 in foo::f2 (u=0) at src/foo.rs:60 //! #3 0x0000555555555281 in foo::f2 (u=0) at src/foo.rs:60
//! #4 0x0000555555555234 in main () at src/foo.rs:51 //! #4 0x0000555555555234 in main () at src/foo.rs:51
//!
//! (gdb) frame 4 //! (gdb) frame 4
//! #4 0x0000555555555234 in main () at src/foo.rs:51 //! #4 0x0000555555555234 in main () at src/foo.rs:51
//! 46 let _ = f2(f1(u.a)); //! 51 let _ = f2(f1(u.a));
//! (gdb) print u //!
//! //! (gdb) print u
//! $1 = foo::A {a: 255, b: 7} //! $1 = foo::A {a: 255, b: 7}
#![no_std] #![no_std]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment