From 57bc21a3762e6bc5c48a53e997b08bd0de8d1160 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Wed, 9 Dec 2020 14:42:32 +0100
Subject: [PATCH] array
---
cargo_klee_examples/examples/array.rs | 79 +++++++++++++++++++++++++++
1 file changed, 79 insertions(+)
create mode 100644 cargo_klee_examples/examples/array.rs
diff --git a/cargo_klee_examples/examples/array.rs b/cargo_klee_examples/examples/array.rs
new file mode 100644
index 0000000..1849132
--- /dev/null
+++ b/cargo_klee_examples/examples/array.rs
@@ -0,0 +1,79 @@
+// 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 sum_first_elements(arr: &[u8], index: usize) -> u8 {
+ let mut acc = 0;
+ for i in 0..index {
+ acc += arr[i as usize];
+ }
+ acc
+}
+
+#[no_mangle]
+fn main() {
+ let arr = [0u8; 8];
+ let mut i: usize = 0;
+ klee_make_symbolic!(&mut i, "i");
+ let b = sum_first_elements(&arr, i);
+}
+
+// A) Array indexing is tricky to analyse at compile time.
+// Thus Rust (rustc) will inject code for run-time verification
+// `panic`ing on index out of range.
+//
+// (Compare to C/C++, where a "buffer overflow" might pass unnoticed
+// causing all sorts of problems.)
+//
+// Compare the test generated in release `--release` (optimized) to
+// test generated in debug/dev mode (un-optimized).
+//
+// Try to explain in your own words the difference and why?
+// (Hint, even if we don't use the result `b`, Rust do optimize out the call, why?)
+//
+// [your answer here]
+//
+// B) Fix the code so that you don't get an error.
+// (It should still compute the sum of the n first elements
+// and return the sum of the whole array if index larger than size/length).
+// The fix should be in the function (not on the caller side).
+//
+// [Git commit "B"]
+//
+// C) In the example, the array is holding only zeroes.
+// Figure out a way to make the content symbolic.
+// (Hint, declare as mutable, iterate and set each element symbolic)
+//
+// [Git commit "C"]
+//
+// D) Analyze the example using KLEE. Now a new (maybe unexpected) error should occur!
+//
+// Explain what caused the error.
+//
+// [your answer here]
+//
+// E) Make a sensible fix to the code.
+// Motivate your choice.
+//
+// [your answer here]
+//
+// [Git commit "D"]
+//
+// F) Learning outcome.
+// 70% of Microsoft security updates over the last decade is directly related to
+// memory safety.
+//
+// Explain in your own words what Microsoft would gain by using Rust.
+//
+// [your answer here]
+//
+// Explain in your own words what Microsoft would gain by using `cargo klee`
+// on their Rust code.
+//
+// And YES, Microsoft is rewriting core system functionality in Rust as we speak!
--
GitLab