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.
PackagesAs with all installations, first make sure you're all up to date:
sudo apt-get update sudo apt-get upgrade
Apt PackagesNow 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 BinariesNext 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 VariablesAt 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
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.9KLEE specifically requires that you use LLVM 2.9. Now, Ubuntu does have a
llvm-2.9package, 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://firstname.lastname@example.org/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 ProverSimple 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-uclibcOur last dependancy is
klee-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 KLEEWith 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 exampleJust 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!