From ad0daf5bc3c534f93aff24d196efbfef2ef3e36b Mon Sep 17 00:00:00 2001
From: Tomasz Kuchta <t.kuchta@samsung.com>
Date: Thu, 12 Oct 2023 09:51:24 +0200
Subject: Feature: implement single memory object resolution for symbolic
 addresses.

This feature implements tracking of and resolution of memory objects in the presence of
symbolic addresses.
For example, an expression like the following:
int x;
klee_make_symbolic(&x, sizeof(x), "x");

int* tmp = &b.y[x].z;

For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching
memory object - including the ones outside of the object "b".
This behaviour is consistent with symbex approach of exploring all execution paths.
However, from the point of view of security testing, we would only be interested to know if we are still
in-bounds or there is a buffer overflow.

The implemented feature creates and tracks (via the GEP instruction) the mapping between the current
symbolic offset and the base object it refers to: in our example we are able to tell that the reference
should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize
the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug.

The feature is turned on via the single-object-resolution command line flag.

A new test case was implemented to illustrate how the feature works.
---
 test/Feature/SingleObjectResolution.c | 52 +++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 test/Feature/SingleObjectResolution.c

(limited to 'test')

diff --git a/test/Feature/SingleObjectResolution.c b/test/Feature/SingleObjectResolution.c
new file mode 100644
index 00000000..687ce9b6
--- /dev/null
+++ b/test/Feature/SingleObjectResolution.c
@@ -0,0 +1,52 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --single-object-resolution %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log
+
+#include "klee/klee.h"
+#include <stdlib.h>
+
+struct A {
+  long long int y;
+  long long int y2;
+  int z;
+};
+
+struct B {
+  long long int x;
+  struct A y[20];
+  struct A *y1;
+  struct A *y2;
+  int z;
+};
+
+int foo(int *pointer) {
+  //printf("pointer is called\n");
+  int *ptr = pointer + 123;
+  return *ptr;
+}
+
+int main(int argc, char *argv[]) {
+
+  int x;
+  struct B b;
+
+  // create a lot of memory objects
+  int *ptrs[1024];
+  for (int i = 0; i < 1024; i++) {
+    ptrs[i] = malloc(23);
+  }
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  b.y1 = malloc(20 * sizeof(struct A));
+
+  // dereference of a pointer within a struct
+  int *tmp = &b.y1[x].z;
+
+  // CHECK: SingleObjectResolution.c:26: memory error: out of bound pointer
+  // CHECK: KLEE: done: completed paths = 1
+  // CHECK: KLEE: done: partially completed paths = 1
+  // CHECK: KLEE: done: generated tests = 2
+  return foo(tmp);
+}
-- 
cgit 1.4.1