构建KLEE与LLVM 3.2环境
使用KLEE最具挑战性的环节是环境构建。官方构建指南仅支持LLVM 2.9和LLVM 3.4的amd64架构。为分析mcsema生成的bitcode，我们需要在i386架构上构建LLVM 3.2版本的KLEE。虽然这是KLEE的非官方支持配置，但实际运行效果良好。
系统准备与依赖安装
需要在32位Ubuntu 14.04系统上进行构建（切勿在64位系统使用-m32标志）：
1
2
3
|
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
|
LLVM与Clang编译
1
2
3
4
5
6
7
8
9
10
11
12
|
mkdir ~/klee
cd ~/klee
wget http://llvm.org/releases/3.2/llvm-3.2.src.tar.gz
wget http://llvm.org/releases/3.2/clang-3.2.src.tar.gz
tar xzf llvm-3.2.src.tar.gz
tar xzf clang-3.2.src.tar.gz
mv clang-3.2.src llvm-3.2.src/tools/clang
cd llvm-3.2.src
./configure --enable-optimized --enable-assertions --enable-targets=x86
make
export PATH=`pwd`/Release+Asserts/bin:$PATH
|
构建STP求解器
1
2
3
4
5
6
7
|
cd ~/klee
git clone https://github.com/stp/stp.git
cd stp
mkdir build && cd build
cmake -G 'Unix Makefiles' -DCMAKE_BUILD_TYPE=Release ..
make
ulimit -s unlimited
|
编译uClibc运行时库
1
2
3
4
5
|
cd ~/klee
git clone --depth 1 --branch klee_0_9_29 https://github.com/klee/klee-uclibc.git
cd klee-uclibc
./configure -l --enable-release
make
|
最终构建KLEE
使用特定commit版本确保兼容性（10b800db2c0639399ca2bdc041959519c54f89e5）：
1
2
3
4
5
6
7
8
9
10
11
12
13
|
git clone https://github.com/klee/klee.git
cd klee
./configure --with-stp=`pwd`/../stp/build \
--with-uclibc=`pwd`/../klee-uclibc \
--with-llvm=`pwd`/../llvm-3.2.src \
--with-llvmcc=`pwd`/../llvm-3.2.src/Release+Asserts/bin/clang \
--with-llvmcxx=`pwd`/../llvm-3.2.src/Release+Asserts/bin/clang++ \
--enable-posix-runtime
make
export LD_LIBRARY_PATH=`pwd`/../stp/build/lib
make check # 预期结果：141通过，1预期失败，11意外失败
make unittests
|
安装mcsema工具链
1
2
3
4
5
6
7
8
9
10
11
|
cd ~/klee
git clone https://github.com/trailofbits/mcsema.git
cd mcsema
git checkout v0.1.0
mkdir build && cd build
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ..
make
export PATH=$PATH:~/klee/llvm-3.2.src/Release+Asserts/bin/
export PATH=$PATH:~/klee/klee/Release+Asserts/bin/
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:~/klee/stp/build/lib/
|
转换迷宫二进制程序
mcsema最新版本包含迷宫演示程序demo_maze：
1
2
3
4
5
6
|
cd ~/klee/mcsema/mc-sema/tests
source env.sh
${CC} -ggdb -m32 -o demo_maze demo_maze.c
${BIN_DESCEND_PATH}/bin_descend -d -func-map=maze_map.txt -i=demo_maze -entry-symbol=main
${CFG_TO_BC_PATH}/cfg_to_bc -i demo_maze.cfg -driver=mcsema_main,main,raw,return,C -o demo_maze.bc
${LLVM_PATH}/opt -O3 -o demo_maze_opt.bc demo_maze.bc
|
配置符号执行环境
1
2
3
4
5
|
cd ~/klee/klee/examples
mkdir maze
cd maze
cp ~/klee/mcsema/mc-sema/tests/demo_maze_opt.bc ./
cp ~/klee/mcsema/mc-sema/common/RegisterState.h ./
|
创建符号执行驱动文件maze_driver.c：
1
2
3
|
// 驱动程序代码（具体内容参考原文gist链接）
// 主要功能：拦截read()和exit()系统调用
// 将read()输入标记为符号值，在exit(1)时触发断言（表示迷宫求解成功）
|
编译驱动程序：
1
|
clang -I../../include/ -emit-llvm -c -o maze_driver.bc maze_driver.c
|
合并bitcode文件：
1
|
llvm-link demo_maze_opt.bc maze_driver.bc > maze_klee.bc
|
运行符号执行
1
2
|
klee --emit-all-errors -libc=uclibc maze_klee.bc
ls klee-last/*assert* # 显示4个成功解：test000178.assert.err等
|
KLEE从mcsema bitcode中识别出的迷宫解决方案与Felipe原始博文结果完全一致：
1
|
sddwddddsddwssssddddwwaawwddddsddwsddwddddssssddwwwwssssddddwwaawwddddssssddwwww
|
技术总结
符号执行技术能够同时执行程序的所有可能输入路径。通过mcsema和KLEE的组合，我们可以对闭源二进制程序进行符号执行分析。本案例成功实现了：
- 从原始二进制文件中发现隐藏墙壁迷宫的所有解
- 在不了解迷宫结构、未针对字符串输入优化的条件下完成分析
- 展示了mcsema将KLEE能力扩展到闭源二进制分析的强大潜力
这种技术可应用于闭源二进制的高覆盖率测试生成和任意二进制应用的安全漏洞挖掘。