与符号执行的亲密接触（第二部分）- Trail of Bits博客
Artem Dinaburg
2014年12月4日
compilers, mcsema, symbolic-execution
这是由两部分组成的博客文章的第二部分，展示了如何将KLEE与mcsema结合使用来符号化执行Linux二进制文件（参见第一部分！）。本部分将涵盖如何构建KLEE和mcsema，并提供一个详细示例，说明如何使用它们来符号化执行现有二进制文件。我们将符号化执行的二进制文件是一个包含隐藏墙壁的迷宫预言机，正如第一部分所承诺的。
作为可视化示例，我们将展示如何从空迷宫到已解决迷宫的过程：
在Ubuntu 14.04上使用LLVM 3.2构建KLEE
使用KLEE最困难的部分之一是构建它。官方构建说明涵盖了在amd64上使用LLVM 2.9和LLVM 3.4的KLEE。为了分析mcsema生成的位码，我们需要在i386上为LLVM 3.2构建KLEE。这是KLEE不支持的配置，但它仍然运行良好。
我们将使用i386版本的Ubuntu 14.04。构建32位KLEE需要32位版本的Ubuntu。不要尝试在64位版本上向CFLAGS添加-m32。这会浪费你数小时的时间，而且无法挽回。获取32位Ubuntu。下面的说明非常详细。请注意：构建所有内容需要一些时间。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
# 这些是如何构建KLEE和mcsema的说明。
# 这是博客文章的一部分，解释如何使用KLEE
# 来符号化执行闭源二进制文件。
# 安装先决条件
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
# 我们假设所有与KLEE相关的内容都将存放在~/klee中。
cd ~
mkdir klee
cd klee
# 获取LLVM和Clang源代码，解压两者
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
# 将clang移动到LLVM源代码树中：
mv clang-3.2.src llvm-3.2.src/tools/clang
# 通常你会在这里使用cmake，但今天你必须使用autotools。
cd llvm-3.2.src
# 对于此示例，我们仅启用x86目标。
# 构建需要一段时间。去喝杯咖啡，小睡一会儿等。
./configure --enable-optimized --enable-assertions --enable-targets=x86
make
# 将生成的二进制文件添加到你的$PATH中（用于后续构建步骤）
export PATH=`pwd`/Release+Asserts/bin:$PATH
# 确保在执行clang时使用正确的clang——你可能
# 意外安装了另一个在$PATH中优先级更高的clang。让我们
# 验证版本以确保正确。你的输出应与下面的内容匹配。
#
#$ clang --version
#clang version 3.2 (tags/RELEASE_32/final)
#Target: i386-pc-linux-gnu
#Thread model: posix
# 一旦clang构建完成，就该为KLEE构建STP和uClibc。
cd ~/klee
git clone https://github.com/stp/stp.git
# 使用CMake构建STP。与LLVM和clang相比，
# STP的构建时间会感觉瞬间完成。
cd stp
mkdir build && cd build
cmake -G 'Unix Makefiles' -DCMAKE_BUILD_TYPE=Release ..
make
# STP构建完成后，让我们为STP和KLEE设置ulimit：
ulimit -s unlimited
# 为KLEE构建uclibc
cd ../..
git clone --depth 1 --branch klee_0_9_29 https://github.com/klee/klee-uclibc.git
cd klee-uclibc
./configure -l --enable-release
make
cd ..
# 现在是KLEE本身。KLEE更新相当频繁，我们正在
# 构建一个不支持的配置。这些说明可能不
# 适用于未来版本的KLEE。这些示例已使用
# 提交10b800db2c0639399ca2bdc041959519c54f89e5进行测试。
git clone https://github.com/klee/klee.git
# 使用LLVM 3.2正确配置KLEE需要这个长的voodoo命令
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
# KLEE带有一组测试以确保构建正常工作。
# 在运行测试之前，libstp必须在库路径中。
# 更改$LD_LIBRARY_PATH以确保链接libstp正常工作。
# 大量文本将滚动，最后显示测试摘要。
# 请注意，你的结果可能略有不同，因为KLEE
# 项目可能已添加或修改了测试。绝大多数
# 测试应该通过。少数测试失败，但我们在
# 不支持的配置上构建KLEE，因此预期会有一些失败。
export LD_LIBRARY_PATH=`pwd`/../stp/build/lib
make check
#这些是预期结果：
#预期通过：141
#预期失败：1
#不支持测试：1
#意外失败：11
# KLEE还有一组单元测试，为了确保，也运行它们。
# 所有单元测试都应该通过！
make unittests
# 现在我们准备好第二部分：
# 使用mcsema与KLEE来符号化执行现有二进制文件。
# 首先，我们需要克隆并构建最新版本的mcsema，其中
# 包括对链接ELF二进制文件的支持，并附带必要的
# 示例以开始使用。
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在示例中包含来自Felipe博客的迷宫程序，名为demo_maze。在下面的说明中，我们将把迷宫预言机编译为32位ELF二进制文件，然后通过mcsema将二进制文件转换为LLVM位码。
1
2
3
4
5
6
7
8
9
10
11
12
|
# 注意：tests/demo_maze.sh自动完成这些步骤
cd ~/klee/mcsema/mc-sema/tests
# 加载我们的环境变量
source env.sh
# 将演示编译为32位ELF可执行文件
${CC} -ggdb -m32 -o demo_maze demo_maze.c
# 使用mcsema的bin_descend恢复CFG
${BIN_DESCEND_PATH}/bin_descend -d -func-map=maze_map.txt -i=demo_maze -entry-symbol=main
# 通过mcsema的cfg_to_bc将CFG转换为LLVM位码
${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
|
我们将使用此步骤生成的优化位码（demo_maze_opt.bc）作为KLEE的输入。现在一切准备就绪，让我们进入有趣的部分——使用KLEE找到所有迷宫解决方案。
1
2
3
4
5
6
7
8
|
# 在其他KLEE示例旁边创建一个工作目录。
cd ~/klee/klee/examples
mkdir maze
cd maze
# 将mcsema生成的位码复制到工作目录
cp ~/klee/mcsema/mc-sema/tests/demo_maze_opt.bc ./
# 复制寄存器上下文（需要构建驱动来运行位码）
cp ~/klee/mcsema/mc-sema/common/RegisterState.h ./
|
现在我们有了LLVM位码格式的迷宫预言机二进制文件，我们需要告诉KLEE哪些输入是符号化的，以及何时迷宫被解决。为此，我们将创建一个小型驱动程序，它将拦截read()和exit()系统调用，将read()的输入标记为符号化，并在exit(1)时断言，表示成功的迷宫解决方案。
要制作驱动程序，创建一个名为maze_driver.c的文件，内容来自此gist，并使用clang将迷宫驱动程序编译为位码。驱动程序中的每个函数都有注释，以帮助解释其工作原理。
1
|
clang -I../../include/ -emit-llvm -c -o maze_driver.bc maze_driver.c
|
现在我们有两个位码文件：迷宫程序的翻译和启动程序并将输入标记为符号化的驱动程序。两者需要合并为一个位码文件以供KLEE使用。这两个文件可以使用llvm-link合并。会有兼容性警告，在这种情况下可以安全忽略。
1
|
llvm-link demo_maze_opt.bc maze_driver.bc > maze_klee.bc
|
运行KLEE
一旦我们有了合并的位码，让我们进行一些符号执行。大量输出将滚动，但我们可以看到KLEE解决迷宫并尝试程序的每个状态。如果你从驱动程序中回忆，我们可以识别成功状态，因为它们将在KLEE中触发断言。原始迷宫有四个解决方案，所以让我们看看我们有多少个。应该有4个结果——一个好迹象（注意：你的测试数字可能不同）：
1
2
3
4
5
6
|
klee --emit-all-errors -libc=uclibc maze_klee.bc
# 大量内容将滚动
ls klee-last/*assert*
# 对我来说，输出是：
# klee-last/test000178.assert.err klee-last/test000315.assert.err
# klee-last/test000270.assert.err klee-last/test000376.assert.err
|
现在让我们使用一个快速的bash脚本来查看输出，看看它们是否与原始结果匹配。从mcsema位码中由KLEE识别的解决方案是：
sddwddddsddwssssddddwwaawwddddsddwsddwddddssssddwwwwssssddddwwaawwddddssssddwwww…
它们与Felipe原始博客文章中的结果匹配！
结论
符号执行是一种强大的工具，可以一次性执行程序的所有输入。使用mcsema和KLEE，我们可以符号化执行现有的闭源二进制程序。在这个例子中，我们找到了一个带有隐藏墙壁的迷宫的所有解决方案——从一个不透明的二进制文件开始。KLEE和mcsema可以在对迷宫一无所知且未针对字符串输入进行调整的情况下完成此操作。
这个例子很简单，但它展示了什么是可能的：使用mcsema，我们可以将KLEE的强大功能应用于闭源二进制文件。我们可以为闭源二进制文件生成高代码覆盖率测试，或在任意二进制应用程序中发现安全漏洞。
注意：我们正在寻找有才华的系统工程师来从事mcsema和相关项目（合同和全职）。如果你有兴趣获得报酬来使用或与mcsema合作，请给我们发送电子邮件！
如果你喜欢这篇文章，请分享：
Twitter
LinkedIn
GitHub
Mastodon
Hacker News
页面内容
在Ubuntu 14.04上使用LLVM 3.2构建KLEE
转换迷宫二进制文件
运行KLEE
结论
最近帖子
构建安全消息传递很难：对Bitchat安全辩论的 nuanced 看法
使用Deptective调查你的依赖关系
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
使你的智能合约超越私钥风险
Go解析器中意外的安全陷阱
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。