Merge pull request #50 from trailofbits/klee-support

KLEE API support

bin/deepstate/common.py

@@ -125,6 +125,10 @@ class DeepState(object):
         "--take_over", action='store_true',
         help="Explore the program starting at the `TakeOver` hook.")
 
+    parser.add_argument(
+        "--klee", action='store_true',
+        help="Expect the test binary to use the KLEE API and use `main()` as entry point.")
+
     parser.add_argument(
         "binary", type=str, help="Path to the test binary to run.")
 

bin/deepstate/main_angr.py

@@ -360,13 +360,15 @@ def hook_apis(project, run_state):
   return mc, apis
 
 
-def main_take_over(args, project):
-  takeover_ea = find_symbol_ea(project, 'DeepState_TakeOver')
+def main_take_over(args, project, takeover_symbol):
+  takeover_ea = find_symbol_ea(project, takeover_symbol)
 
-  hook_function(project, takeover_ea, TakeOver)
+  if not args.klee:
+      hook_function(project, takeover_ea, TakeOver)
 
   if not takeover_ea:
-    L.critical("Cannot find symbol `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Cannot find symbol `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
@@ -385,14 +387,16 @@ def main_take_over(args, project):
   try:
     takeover_state = concrete_manager.found[0]
   except:
-    L.critical("Execution never hit `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Execution never hit `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
   try:
     run_state = takeover_state.step().successors[0]
   except:
-    L.critical("Unable to exit from `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Unable to exit from `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
@@ -486,7 +490,9 @@ def main():
     return 1
 
   if args.take_over:
-    return main_take_over(args, project)
+    return main_take_over(args, project, 'DeepState_TakeOver')
+  elif args.klee:
+    return main_take_over(args, project, 'main')
   else:
     return main_unit_test(args, project)
 

bin/deepstate/main_manticore.py

@@ -309,7 +309,7 @@ def find_symbol_ea(m, name):
   return 0
 
 
-def do_run_test(state, apis, test):
+def do_run_test(state, apis, test, hook_test=False):
   """Run an individual test case."""
   state.cpu.PC = test.ea
   m = manticore.Manticore(state, sys.argv[1:])
@@ -338,23 +338,22 @@ def do_run_test(state, apis, test):
   m.add_hook(apis['ClearStream'], hook(hook_ClearStream))
   m.add_hook(apis['LogStream'], hook(hook_LogStream))
 
-  # Here we hook `DeepState_TakeOver()`, even if running unit tests.
-  # In that case, we simply will never hit this hooked function model.
-  m.add_hook(test.ea, hook(hook_TakeOver))
+  if hook_test:
+    m.add_hook(test.ea, hook(hook_TakeOver))
 
   m.subscribe('will_terminate_state', done_test)
   m.run()
 
 
-def run_test(state, apis, test):
+def run_test(state, apis, test, hook_test):
   try:
-    do_run_test(state, apis, test)
+    do_run_test(state, apis, test, hook_test)
   except:
     L.error("Uncaught exception: {}\n{}".format(
-        sys.exc_info()[0], traceback.format_exc()))
+      sys.exc_info()[0], traceback.format_exc()))
 
 
-def run_tests(args, state, apis):
+def run_tests(state, apis, hook_test_ea):
   """Run all of the test cases."""
   pool = multiprocessing.Pool(processes=max(1, args.num_workers))
   results = []
@@ -362,7 +361,7 @@ def run_tests(args, state, apis):
   tests = mc.find_test_cases()
 
   L.info("Running {} tests across {} workers".format(
-      len(tests), args.num_workers))
+    len(tests), args.num_workers))
 
   for test in tests:
     res = pool.apply_async(run_test, (state, apis, test))
@@ -374,11 +373,12 @@ def run_tests(args, state, apis):
   exit(0)
 
 
-def main_takeover(m, args):
-  takeover_ea = find_symbol_ea(m, 'DeepState_TakeOver')
+def main_takeover(m, args, takeover_symbol):
+  takeover_ea = find_symbol_ea(m, takeover_symbol)
   if not takeover_ea:
-    L.critical("Cannot find symbol `DeepState_TakeOver` in binary `{}`".format(
-        args.binary))
+    L.critical("Cannot find symbol `{}` in binary `{}`".format(
+      takeover_symbol,
+      args.binary))
     return 1
 
   takeover_state = m._initial_state
@@ -394,7 +394,11 @@ def main_takeover(m, args):
   del mc
 
   fake_test = TestInfo(takeover_ea, '_takeover_test', '_takeover_file', 0)
-  m.add_hook(takeover_ea, lambda state: run_test(state, apis, fake_test))
+
+  hook_test = not args.klee
+  takeover_hook = lambda state: run_test(state, apis, fake_test, hook_test)
+  m.add_hook(takeover_ea, takeover_hook)
+
   m.run()
 
 
@@ -402,7 +406,7 @@ def main_unit_test(m, args):
   setup_ea = find_symbol_ea(m, 'DeepState_Setup')
   if not setup_ea:
     L.critical("Cannot find symbol `DeepState_Setup` in binary `{}`".format(
-        args.binary))
+      args.binary))
     return 1
 
   setup_state = m._initial_state
@@ -428,7 +432,7 @@ def main():
     m = manticore.Manticore(args.binary)
   except Exception as e:
     L.critical("Cannot create Manticore instance on binary {}: {}".format(
-        args.binary, e))
+      args.binary, e))
     return 1
 
   m.verbosity(1)
@@ -438,7 +442,9 @@ def main():
   m._binary_obj = m._initial_state.platform.elf
 
   if args.take_over:
-    return main_takeover(m, args)
+    return main_takeover(m, args, 'DeepState_TakeOver')
+  elif args.klee:
+    return main_takeover(m, args, 'main')
   else:
     return main_unit_test(m, args)
 

examples/CMakeLists.txt

@@ -46,3 +46,6 @@ set_target_properties(Squares PROPERTIES COMPILE_DEFINITIONS "DEEPSTATE_TEST")
 
 add_executable(TakeOver TakeOver.cpp)
 target_link_libraries(TakeOver deepstate)
+
+add_executable(Klee Klee.c)
+target_link_libraries(Klee deepstate)

examples/Klee.c

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2018 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <deepstate/Klee.h>
+
+DEEPSTATE_NOINLINE int get_sign(int x) {
+  if (x == 0) {
+    printf("zero\n");
+    return 0;
+  }
+
+  if (x < 0) {
+    printf("negative\n");
+    return -1;
+  } else {
+    printf("positive\n");
+    return 1;
+  }
+}
+
+int main(int argc, char *argv[]) {
+  int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  return get_sign(a);
+}

src/include/deepstate/Klee.h

@@ -0,0 +1,146 @@
+/*
+ * Copyright (c) 2018 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef SRC_INCLUDE_DEEPSTATE_KLEE_H_
+#define SRC_INCLUDE_DEEPSTATE_KLEE_H_
+
+#include <deepstate/DeepState.h>
+
+DEEPSTATE_BEGIN_EXTERN_C
+
+/* Unsupported. */
+/* static void klee_define_fixed_object(void *addr, size_t nbytes); */
+
+static void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
+  DeepState_SymbolizeData(addr, addr + nbytes);
+}
+
+static int klee_range(int begin, int end, const char *name) {
+  return DeepState_IntInRange(begin, end);
+}
+
+static int klee_int(const char *name) {
+  return DeepState_Int();
+}
+
+DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
+  exit(status);
+}
+
+DEEPSTATE_NORETURN static void klee_abort(void) {
+  abort();
+}
+
+/* Unsupported. */
+/* static size_t klee_get_obj_size(void *ptr); */
+
+static void klee_print_expr(const char *msg, ...) {
+  /* KLEE debugging command, no DeepState equivalent. */
+  /* See impl in `runtime/Runtest/intrinsics.c`. */
+}
+
+static uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t out;
+  klee_make_symbolic(&out, sizeof(out), "klee_choose");
+
+  if (n <= out) {
+    klee_silent_exit(0);
+  }
+
+  return out;
+}
+
+/* Unsupported. */
+/* static unsigned klee_is_symbolic(uintptr_t n); */
+
+/* Unsupported. */
+/* static void klee_assume(uintptr_t condition); */
+
+static void klee_warning(const char *message) {
+  DeepState_Log(DeepState_LogWarning, message);
+}
+
+static void klee_warning_once(const char *message) {
+  DeepState_Log(DeepState_LogWarning, message);
+}
+
+static void klee_prefer_cex(void *object, uintptr_t condition) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
+
+static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
+
+/* Unsupported. */
+/* static void klee_mark_global(void *object); */
+
+#define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type val)
+
+/* Unsupported. */
+/* static KLEE_GET_VALUE(f, float); */
+
+/* Unsupported. */
+/* static KLEE_GET_VALUE(d, double); */
+
+static KLEE_GET_VALUE(l, long) {
+  DeepState_MinInt(val);
+}
+
+/* Unsupported. */
+/* static KLEE_GET_VALUE(ll, long long) */
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(_i32, int32_t) {
+  DeepState_MinInt(val);
+}
+
+/* TODO(joe): Implement */
+/* Unsupported. */
+/* static KLEE_GET_VALUE(_i64, int64_t); */
+
+#undef KLEE_GET_VALUE
+
+/* Unsupported. */
+/* static void klee_check_memory_access(const void *address, size_t size); */
+
+static void klee_set_forking(unsigned enable) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
+
+/* Unsupported. */
+/* static void
+ * klee_alias_function(const char *fn_name, const char *new_fn_name); */
+
+static void klee_stack_trace(void) {
+  /* KLEE debugging command, no DeepState equivalent. */
+}
+
+static void klee_print_range(const char *name, int arg) {
+  /* KLEE debugging command, no DeepState equivalent. */
+}
+
+static void klee_open_merge(void) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
+
+static void klee_close_merge(void) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
+
+DEEPSTATE_END_EXTERN_C
+
+#endif  /* SRC_INCLUDE_DEEPSTATE_KLEE_H_ */