It seems like all of the cool kids nowadays are into Symbolic Execution, especially for vulnerability research. It's probably all because of DARPA's Cyber Grand Challenge - a government-sponsored challenge to develop a system that automates vulnerability discovery.
If you start to dive into the topic, you'll undoubtedly come across KLEE, a project coming out of Standford University. KLEE is a great tool to get you started with symbolic execution, however the set up can be slightly daunting for the "app crowd" :) KLEE's home page has a Getting Started page, but it lacks some updates. In this blog post we'll walk you through the most up to date build process from a fresh install of Ubuntu 14.04 LTS Desktop 64-bit.
Packages
As with all installations, first make sure you're all up to date:sudo apt-get update
sudo apt-get upgrade
Apt Packages
Now we'll get the easy stuff out of the way, and install all of the required packages:sudo apt-get install g++ curl python-minimal git bison flex bc libcap-dev build-essential libboost-all-dev ncurses-dev cmake
LLVM-GCC Binaries
Next we'll need to download the LLVM-GCC binaries and extract them to our home directory:wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
tar -jxvf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
Environment Variables
At this point, we'll need to set up a few environment variables for everything else to run properly. As stated on the KLEE's Getting Started page, most issues people have are related to not setting these:export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
export PATH=$PATH:$HOME/llvm-gcc4.2-2.9-x86_64-linux/bin
It's also recommended to add these to your
.bashrc
:echo "export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> .bashrc
echo "export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> .bashrc
echo "export PATH=$PATH:$HOME/llvm-gcc4.2-2.9-x86_64-linux/bin" >> .bashrc
Building LLVM 2.9
KLEE specifically requires that you use LLVM 2.9. Now, Ubuntu does have allvm-2.9
package, and LLVM 2.9 binaries are available from a couple of different locations. However, I decided to stay as true to KLEE's Getting Started instructions. Let's download the source:wget http://llvm.org/releases/2.9/llvm-2.9.tgz
tar -zxvf llvm-2.9.tgz
cd llvm-2.9
Before we build, we need to apply one patch:
wget http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01302/unistd-llvm-2.9-jit.patch
patch -p1 < unistd-llvm-2.9-jit.patch
And now we can build:
./configure --enable-optimized --enable-assertions
make
cd $HOME
The build might produce some warnings but they can all be safely ignored.
Building Simple Theorem Prover
Simple Theorem Prover (STP) was the source of a couple problems, rather than following the Getting Start Page, take this approach:git clone https://github.com/stp/stp.git
cd stp
mkdir build && cd build
cmake -G 'Unix Makefiles' $HOME/stp
make
sudo make install
sudo ldconfig
ulimit -s unlimited
cd $HOME
KLEE-uclibc
Our last dependancy isklee-uclibc
, to get that set up we:git clone --depth 1 --branch klee_0_9_29 https://github.com/klee/klee-uclibc.git
cd klee-uclibc/
./configure --with-llvm-config $HOME/llvm-2.9/Release+Asserts/bin/llvm-config --make-llvm-lib
make -j`nproc`
cd $HOME
Building KLEE
With all of our dependancies out of the way, we can build KLEE:git clone https://github.com/klee/klee.git
cd klee
./configure --enable-posix-runtime --with-stp=/usr/local --with-llvm=$HOME/llvm-2.9/ --with-uclibc=$HOME/klee-uclibc/
make ENABLE_OPTIMIZED=1
make check
make unittests
sudo make install
cd $HOME
Testing with an example
Just to confirm everything is working, you can run through Tutorial 1:cd $HOME/klee/examples/get_sign
llvm-gcc -I ../../include --emit-llvm -c -g get_sign.c
klee get_sign.o
You're ready to go! Good luck!