From dbe6defa3acb1e2f880f99f7c8e7d8a31455bc16 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 8 Dec 2020 23:03:52 +0100
Subject: [PATCH] Cargo klee examples
---
.gitignore | 3 +
.vscode/settings.json | 7 +-
README.md | 25 +++++-
cargo_klee_examples/.gitignore | 3 +
cargo_klee_examples/Cargo.toml | 30 +++++++
cargo_klee_examples/README.md | 12 +++
cargo_klee_examples/examples/get_sign.rs | 106 +++++++++++++++++++++++
7 files changed, 182 insertions(+), 4 deletions(-)
create mode 100644 .gitignore
create mode 100644 cargo_klee_examples/.gitignore
create mode 100644 cargo_klee_examples/Cargo.toml
create mode 100644 cargo_klee_examples/README.md
create mode 100644 cargo_klee_examples/examples/get_sign.rs
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..98e5fcf
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+target
+**/*.rs.bk
+Cargo.lock
diff --git a/.vscode/settings.json b/.vscode/settings.json
index 7f80cba..8ce88ac 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,13 +1,18 @@
{
"cSpell.ignoreWords": [
+ "cmake",
"core",
"cstr",
"datatypes",
"ktest",
"libklee",
+ "libz",
"llvm",
+ "mkdir",
"runtest",
"rustc",
- "satisfiability"
+ "satisfiability",
+ "skylake",
+ "znver"
]
}
\ No newline at end of file
diff --git a/README.md b/README.md
index c23c8c4..e7b7a98 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,10 @@
# KLEE tutorial
-Installing and testing klee.
+- Installing and testing klee.
+
+- Manual use of the KLEE tools for C and Rust programs.
+
+- Simplified usage adopting `klee-sys` and `cargo klee`.
## Dependencies
@@ -28,7 +32,6 @@ Under arch with `yay` installed simply:
> sudo apt install z3 libz3-4 libz3-cil libz3-dev libz3-java libz3-jni libz3-ocaml-de
-
## Install KLEE from source
The instructions recommend LLVM 9, but the current master (2.2-pre) supports LLVM 11 (which is what you would have under arch as of 2020-12-07).
@@ -107,8 +110,24 @@ Here you learn:
---
+## klee-sys and Cargo-klee
+
+See the `cargo-klee-examples` folder.
+
+Here you learn:
+
+- an easy way to compile and run KLEE on Rust code
+- an easy way to replay test cases for Rust programs
+
+TODO:
+
+More interesting verification problems using `cargo klee`.
+
+--
+
+
## Why KLEE on Rust
Out the box, Rust provides superior memory safety and guarantees to well defined behavior. However there are cases where the Rust compiler (rustc) cannot statically (at compile time) ensure these guarantees. For such cases (e.g., division by zero, slice/array indexing etc.) Rust injects code for run-time verification that emit a `panic!` (with appropriate error message). While still being safe (the code never runs into memory unsafety or undefined behavior) this limits the reliability (availability) of the system (as its very hard to recover from a `panic!`.) In practice, the developer would typically reboot/reset the system (and store some error code/trace for post-mortem analysis).
-With KLEE we can do better! We bind Rust `panic!` to KLEE `abort` (a path termination), and let. For all reachable `panic!`s, KLEE will provide a concrete test, which we can replay and address in our source code. When done, we have a proof of `panic` freedom and thus defined behavior, with huge impact to reliability (and security) of the system at hand.
\ No newline at end of file
+With KLEE we can do better! We bind Rust `panic!` to KLEE `abort` (a path termination), and let. For all reachable `panic!`s, KLEE will provide a concrete test, which we can replay and address in our source code. When done, we have a proof of `panic` freedom and thus defined behavior, with huge impact to reliability (and security) of the system at hand.
diff --git a/cargo_klee_examples/.gitignore b/cargo_klee_examples/.gitignore
new file mode 100644
index 0000000..6936990
--- /dev/null
+++ b/cargo_klee_examples/.gitignore
@@ -0,0 +1,3 @@
+/target
+**/*.rs.bk
+Cargo.lock
diff --git a/cargo_klee_examples/Cargo.toml b/cargo_klee_examples/Cargo.toml
new file mode 100644
index 0000000..259380e
--- /dev/null
+++ b/cargo_klee_examples/Cargo.toml
@@ -0,0 +1,30 @@
+[package]
+name = "cargo_klee_examples"
+version = "0.1.0"
+authors = ["pln <Per Lindgren>"]
+edition = "2018"
+
+[dependencies.klee-sys]
+git = "https://gitlab.henriktjader.com/KLEE/klee-sys.git"
+version = "0.2.0"
+
+[dependencies.panic-klee]
+git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
+version = "0.1.0"
+
+
+[profile.dev]
+panic = "abort"
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
+
+[profile.release]
+panic = "abort"
+debug = true # better debugging
+incremental = false # better optimization
+lto = true # better optimization
+codegen-units = 1 # better optimization
+
+[features]
+klee-analysis = ["klee-sys/klee-analysis"]
diff --git a/cargo_klee_examples/README.md b/cargo_klee_examples/README.md
new file mode 100644
index 0000000..1bde704
--- /dev/null
+++ b/cargo_klee_examples/README.md
@@ -0,0 +1,12 @@
+# Examples on `cargo-klee` usage
+
+## Install
+
+Clone the [cargo-klee](https://gitlab.henriktjader.com/pln/cargo-klee).
+
+Follow install instructions.
+
+## Examples
+
+- `examples/get_sign.rs`, same simple example again but now using the `cargo klee` cargo sub-command. The example also uses `klee-sys` bindings.
+
diff --git a/cargo_klee_examples/examples/get_sign.rs b/cargo_klee_examples/examples/get_sign.rs
new file mode 100644
index 0000000..0136817
--- /dev/null
+++ b/cargo_klee_examples/examples/get_sign.rs
@@ -0,0 +1,106 @@
+// get_sign.rs
+// Showcase how we automatically can interface Rust to KLEE
+//
+
+#![no_std]
+#![no_main]
+
+use klee_sys::klee_make_symbolic;
+use panic_klee as _;
+
+fn get_sign(x: i32) -> i32 {
+ if x == 0 {
+ return 0;
+ }
+ if x < 0 {
+ return -1;
+ } else {
+ return 1;
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let mut a: i32 = 0;
+ klee_make_symbolic!(&mut a, "a");
+ get_sign(a);
+}
+
+// A) Compile a Rust program for KLEE analysis.
+//
+// The bindings to klee are abstracted into `klee-sys`.
+// The panic handler into `panic_klee` (essentially KLEE `abort`).
+// The tedious build process into `cargo klee`.
+//
+// > cargo klee -help
+//
+// The default is to generate LLVM-IR run KLEE on the generated LLVM-IR.
+// This enables the `klee-analysis` feature of `klee-sys`.
+//
+// Using the `-v` option we see verbose output.
+//
+// > cargo klee -v --example get_sign
+// "cargo" "rustc" "-v" "--features" "klee-analysis" "--example" "get_sign" "--color=always" "--" "-C" "linker=true" "-C" "lto" "--emit=llvm-ir"
+// ...
+//
+// KLEE: Using Z3 solver backend
+//
+// KLEE: done: total instructions = 92
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+// This should be familiar to the build you did in the previous exercise.
+//
+// Now locate the generated tests. Give the relative path to `klee-last`.
+//
+// [your answer here]
+//
+// B) Replay test cases
+//
+// By giving the `-r` (or `--replay`), you can easily replay the test cases:
+//
+// > cargo klee -v -r -g --example get_sign
+//
+// (gdb) set environment KTEST_FILE=klee-last/test000001.ktest
+// (gdb) break get_sign
+// (gdb) run
+//
+// What path of the program does this path trigger?
+//
+// [your answer here]
+//
+// Just out of curiosity, you may test the other test cases as well...
+//
+// B) UX/IX
+//
+// Compare to the "stock KLEE for C" experience.
+//
+// How does `klee-sys` and `cargo-klee` score on a 0..5 scale?
+//
+// [your answer here]
+//
+// If below 5, what could be done to improve the UX/IX?
+//
+// [your answer here]
+//
+// C) Inner workings.
+//
+// Have a look on the source code of `klee-sys`.
+// You will find that it is very similar to the code you saw in the
+// previous exercise.
+//
+// Try to follow the `klee-analysis` feature.
+// What modules in `klee-sys` does this feature enable?
+//
+// [your answer here]
+//
+// Have a look at the source code of `cargo klee`.
+// (The actual sub-command is in the folder `cargo-klee`.)
+//
+// Try to figure out how the correct `.ll` file is determined.
+// Which one will it pick, and why?
+//
+// [your answer here]
+//
+// Actually this is one of the "bad seeds" in the internal design.
+// Seems there is no "stable" way of controlling/retrieving the "metadata"
+// (i.e., the hashing). Ideas welcome!
--
GitLab