artemdinaburg

# These directions will:
# 1. Build a binary version of the Symbolic Maze by Felipe Manzano
# 2. Convert the binary to LLVM bitcode with mcsema
# 3. Optimize the resulting LLVM bitcode
#
# These same actions are done by 
# ~/klee/mcsema/mc-sema/tests/demo_maze.sh
# if you would like to run them automatically

cd ~/klee/mcsema/mc-sema/tests

artemdinaburg

# These are instructions for how to build KLEE and mcsema. 
# These are a part of a blog post explaining how to use KLEE
# to symbolically execute closed source binaries.

# install the prerequisites
sudo apt-get install vim build-essential g++ curl python-minimal \
  git bison flex bc libcap-dev cmake libboost-dev \
  libboost-program-options-dev libboost-system-dev ncurses-dev nasm

# we assume everything KLEE related will live in ~/klee.

artemdinaburg

for i in klee-last/*assert*; do \
  ktest-tool $(echo $i | cut -f 1 -d '.').ktest; \
  done

#My Output:
#ktest file : 'klee-last/test000178.ktest'
#args       : ['maze_klee.bc']
#num objects: 1
#object    0: name: 'syminput'
#object    0: size: 28

artemdinaburg

#include <klee/klee.h>
#include <stdlib.h>
#include "RegisterState.h"

extern int mcsema_main(RegState *);

// this will call the main() of the original application
// Note: mcsema includes the option to auto-generate these drivers
// but they will *NOT* work with KLEE, because the auto generation
// code uses mmap(), which KLEE can't deal with.