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

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

parents a5439e74 85ddad0c
No related branches found
No related tags found
No related merge requests found
/target target
**/*.rs.bk **/*.rs.bk
Cargo.lock
# 1 minute introduction # KLEE bindings for Rust
## requirements 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.
- docker
- nightly toolchain (nightly-2018-01-10) 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` feature) the assertions (and their implied overhead) will be omitted in a production build.
## Requirements
- docker (optional)
- KLEE (optional)
- nightly toolchain (edition-2018)
The `klee` tool needs either access to a docker image providing KLEE, or KLEE being natively 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 ## usage
``` console ``` console
$ systemctl start docker.service # if not already started/enabled $ 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
...@@ -15,39 +33,66 @@ $ cd klee-examples ...@@ -15,39 +33,66 @@ $ cd klee-examples
$ cargo klee --example foo --release $ cargo klee --example foo --release
KLEE: output directory is "/mnt/target/release/examples/klee-out-0" KLEE: output directory is "/home/pln/rust/klee/klee-examples/target/release/examples/klee-out-0"
KLEE: Using STP solver backend KLEE: Using Z3 solver backend
KLEE: ERROR: /home/pln/klee/klee-rust/klee/src/lib.rs:24: abort failure 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: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 20 KLEE: done: total instructions = 22
KLEE: done: completed paths = 2 KLEE: done: completed paths = 2
KLEE: done: generated tests = 2 KLEE: done: generated tests = 2
```
$ more target/release/examples/klee-out-0/test000001.abort.err KLEE generates two test cases, we can view them by:
``` sh
$ 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:
``` sh
$ more target/release/examples/klee-last/test000001.abort.err
Error: abort failure Error: abort failure
File: /home/pln/klee/klee-rust/klee/src/lib.rs File: /home/pln/rust/klee/src/lang_items.rs
Line: 24 Line: 6
assembly.ll line: 76 assembly.ll line: 49
Stack: Stack:
#000000076 in _ZN4core9panicking9panic_fmt17hc7d7358b749037fdE () at /home/pln/klee/klee-rust/klee/src/lib.rs:24 #000000049 in _ZN4core9panicking9panic_fmt17h8e7152a45a601b4bE () at /home/pln/rust/klee/src/lang_items.rs:6
#100000070 in _ZN4core9panicking5panic17h4680eb5ae9b0e3d0E () at HOME/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/pani #100000055 in _ZN4core9panicking5panic17h9a94013c5e0723bbE () at /rustc/edaac35d67bed09260dc0c318acc5212fb66246e/src/libcore/panicking.rs:52
cking.rs:51 #200000023 in main () at /home/pln/rust/klee/klee-examples/examples/foo.rs:24
#200000044 in main (=1, =94362321163792) at PWD/klee-examples/examples/foo.rs:22
``` ```
The error found is at line 22. In this case it is the Rust built in division by zero detection that causes a `panic!`.
``` rust The error found is at line 24.
``` rust
#![no_std] #![no_std]
#![no_main]
#[macro_use] #[macro_use]
extern crate klee; extern crate klee;
use core::ptr; use core::ptr;
#[no_mangle]
fn main() { fn main() {
let u = ksymbol!("u"); let u = ksymbol!("u");
...@@ -62,6 +107,15 @@ fn f1(u: u8) -> u8 { ...@@ -62,6 +107,15 @@ fn f1(u: u8) -> u8 {
} }
fn f2(u: u8) -> u8 { fn f2(u: u8) -> u8 {
100 / u // <- error found here is a Rust div 0 panic! . 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.
\ No newline at end of file
[[package]]
name = "cargo-klee"
version = "0.1.0"
dependencies = [
"libc 0.2.33 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "libc"
version = "0.2.33"
source = "registry+https://github.com/rust-lang/crates.io-index"
[metadata]
"checksum libc 0.2.33 (registry+https://github.com/rust-lang/crates.io-index)" = "5ba3df4dcb460b9dfbd070d41c94c19209620c191b0340b929ce748a2bcd42d2"
[package]
authors = ["Jorge Aparicio <jorge@japaric.io>"]
name = "cargo-klee"
version = "0.1.0"
[dependencies]
libc = "0.2.33"
extern crate libc;
use std::io::{self, Read, Write};
use std::process::{Command, Stdio};
use std::{env, str};
fn main() {
// first argument is the path to this binary; the second argument is always "klee" -- both can
// be ignored
let args = env::args().skip(2).collect::<Vec<_>>();
// turn `cargo klee --example foo` into `xargo rustc --example foo -- (..)`
let mut c = Command::new("cargo");
c.arg("rustc")
.args(&args)
// verbose output for debugging purposes
.arg("-v")
.arg("--color=always")
.arg("--")
// ignore linking
.args(&["-C", "linker=true"])
// force LTO
.args(&["-C", "lto"])
// also output the LLVM-IR (.ll file) for debugging purposes
.arg("--emit=llvm-bc,llvm-ir")
// force panic=abort in all crates
.env("RUSTFLAGS", "-C panic=abort")
// collect stderr
.stderr(Stdio::piped());
// print full command for debugging purposes
eprintln!("{:?}", c);
// spawn process and drive it completion while replicating its stderr in ours
let mut p = c.spawn().unwrap();
let mut pstderr = p.stderr.take().unwrap();
let mut buf = [0; 1024];
let mut output = vec![];
let stderr = io::stderr();
let mut stderr = stderr.lock();
loop {
if let Ok(n) = pstderr.read(&mut buf) {
stderr.write(&buf[..n]).unwrap();
output.extend_from_slice(&buf[..n]);
}
if let Some(status) = p.try_wait().unwrap() {
assert!(status.success());
break;
}
}
// next we are going to try to run the .bc file using klee inside a docker container
// FIXME the way we find out which .bc file we have to use is pretty hacky; using Cargo as a
// library would be cleaner, I suppose
// find out the argument passed to `--example`, if used at all
let mut example = None;
let mut iargs = args.iter();
while let Some(arg) = iargs.next() {
if arg == "--example" {
example = iargs.next();
break;
}
}
// get the suffix of the example
let (example, suffix) = if let Some(example) = example {
let mut suffix = None;
let output = str::from_utf8(&output).unwrap();
for line in output.lines() {
if line.contains(&format!("examples/{}.rs", example)) {
for part in line.split(' ') {
if part.starts_with("extra-filename=") {
suffix = part.split('=').nth(1);
}
}
}
}
(example, suffix.unwrap())
} else {
// nothing to do if the user didn't use `--example`
return;
};
let profile = if args.iter().any(|a| a == "--release") {
"release"
} else {
"debug"
};
// let mut docker = Command::new("docker");
// docker
// .arg("run")
// .arg("--rm")
// .args(&["--user", &format!("{}:{}", uid(), gid())])
// .args(&[
// "-v",
// &format!("{}:/mnt", env::current_dir().unwrap().display()),
// ])
// .args(&["-w", "/mnt"])
// .arg("-it")
// .arg("afoht/llvm-klee-4")
// .args(&[
// "/usr/bin/klee",
// &format!("target/{}/examples/{}{}.bc", profile, example, suffix),
// ]);
// // print full command for debugging purposes
// eprintln!("{:?}", docker);
//
// assert!(docker.status().unwrap().success());
let mut klee_cmd = Command::new("klee");
klee_cmd.arg(&format!(
"target/{}/examples/{}{}.ll",
profile, example, suffix
));
eprintln!("{:?}", klee_cmd);
assert!(klee_cmd.status().unwrap().success());
}
// NOTE from cross
fn gid() -> u32 {
unsafe { libc::getgid() }
}
// NOTE from cross
fn uid() -> u32 {
unsafe { libc::getuid() }
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment