jywhy6's blog
0%

符号执行引擎 KLEE 学习笔记

Posted on Edited on In
Symbols count in article: 6.8k Reading time ≈ 11 mins.

符号执行 (Symbolic Execution) 是一种程序分析技术，其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。
（摘录自中文维基百科，有改动）

参考资料

关于符号执行

关于 KLEE

编译安装 KLEE

使用 KLEE

常见问题

入门 KLEE

KLEE 是基于 LLVM 编译器架构的符号执行引擎，它对 LLVM bitcode 进行解释，并使用 SMT 求解器来探索可能的符号执行路径。

编译安装 KLEE (Ubuntu)

按照官方教程编译安装即可 (想快速入门的用户也可以考虑直接使用官方提供的 Docker 镜像)。使用 WSL 时，请保证 git clone 等命令全部在 linux 环境下执行，否则可能产生一些问题 (文件中换行变成 CRLF 导致 linux 环境下脚本解析错误、linx 环境下从源码编译时调用了 windows.h 头文件等)。

为了保证 KLEE 功能的完整性，我安装了所有可选功能 (Google test、uClibc 与 POSIX 环境、libc++ 支持)，并选择使用 Z3 作为约束求解器，最后使用的 cmake 命令行参数如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
cmake \
-DENABLE_POSIX_RUNTIME=ON \
-DENABLE_KLEE_UCLIBC=ON \
-DENABLE_KLEE_LIBCXX=ON \
-DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ \
-DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ \
-DENABLE_KLEE_EH_CXX=ON \
-DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ \
-DKLEE_UCLIBC_PATH=/mnt/c/me/code/tools/klee-uclibc \
-DENABLE_UNIT_TESTS=ON \
-DENABLE_SYSTEM_TESTS=ON \
-DGTEST_SRC_DIR=/mnt/c/me/code/tools/googletest-release-1.7.0 \
-DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 \
-DLLVMCC=/usr/bin/clang-9 \
-DLLVMCXX=/usr/bin/clang++-9 \
-DCMAKE_C_COMPILER=clang  \
-DCMAKE_CXX_COMPILER=clang++  \
..

通过简单案例学习 KLEE

本节内容与官方教程 Tutorial One - Testing a Small Function 相同，尝试使用 KLEE 探索一个简单函数的各个执行路径。

首先打开 examples/get_sign/get_sign.c，源代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
#include "klee/klee.h"

int get_sign(int x) {
  if (x == 0)
     return 0;
  if (x < 0)
     return -1;
  else
     return 1;
}

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

然后将源代码编译为 LLVM bitcode：

1
2
3
4
5
6
clang \
-I ../../include \
-emit-llvm -c \
-g \
-O0 -Xclang -disable-O0-optnone \
get_sign.c

其中各个参数的含义为：

  • -I ../../include 添加了编译器 include 路径，使得 clang 能找到头文件 klee/klee.h (其中包含与 KLEE 虚拟机交互的内部函数声明，如 klee_make_symbolic ) 。
  • -emit-llvm -c 让编译器生成 bitcode (.bc) 格式 (而不是人类可读的 .ll 格式) 的 LLVM IR。
  • -g 使得 bitcode 文件中包含源码级别的 debug 信息。
  • -O0 -Xclang -disable-O0-optnone 关闭编译器优化功能，并禁止 optnone 阻止 KLEE 对中间表示码的优化 (请注意这是一个双重否定句，详见 opt is defunct when code built without optimizations ) 。

接下来使用 KLEE 对 bitcode 进行符号执行，可以看到 KLEE 成功探索了 3 条可能的执行路径，并将每条执行路径所对应的输入写入klee-last 文件夹的 .ktest 文件中：

1
2
3
4
5
6
7
$ klee get_sign.bc

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 31
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3
1
2
3
4
5
$ ls klee-last/

assembly.ll      run.istats       test000002.ktest
info             run.stats        test000003.ktest
messages.txt     test000001.ktest warnings.txt

最后可以使用 ktest-tool 查看具体的输入值 (KLEE 采用了内存符号化的方式，没有各个符号的类型信息，因此提供了符号值的多种表示形式)：

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
$ ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

$ ktest-tool klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x01\x01\x01\x01'
object 0: hex : 0x01010101
object 0: int : 16843009
object 0: uint: 16843009
object 0: text: ....

$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

KLEE 符号执行测试流程总结：

  1. 为了使用 KLEE 对一个函数 (此处为 get_sign ) 进行符号执行测试，首先需要将该函数独立出来，并编写一个专用于测试的源码文件 (记得 #include "klee/klee.h" ) 。
  2. 在源码文件的 main 函数中，将函数的输入符号化 (通过 klee_make_symbolic ) ，然后再调用待测函数。
  3. 将测试专用源码文件编译为 .bc 格式的 LLVM bitcode，然后使用 klee 命令行工具对 bitcode 进行符号执行。
  4. 在 klee-last 文件夹中找到 .ktest 文件，使用 ktest-tool 解析 KLEE 生成的符号执行测试输入。

使用 KLEE 对 C++ 源代码进行符号执行

前置要求：编译 KLEE 时已添加 uClibc 和 libc++ 支持，或直接使用 KLEE 官方提供的 Docker 镜像。

首先不妨创建 examples/test_cpp/test_cpp.cpp，源代码如下：

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
#include <iostream>
#include "klee/klee.h"

class test_a {
   private:
    int a;

   public:
    virtual int get_num() { return a; }

    virtual ~test_a() {}
};

class test_b : public test_a {
   private:
    int b;

   public:
    int get_num() { return b; }
};

int test_sign(test_a* t) {
    if (t->get_num() == 0) return 0;
    if (t->get_num() < 0)
        return -1;
    else
        return 1;
}

int main() {
    test_a* t_b = new test_b();
    test_a* t_a = new test_a();

    uintptr_t vtbl_p = *reinterpret_cast<uintptr_t*>(t_b);
    klee_make_symbolic(t_b, sizeof(*t_b), "t_b");
    klee_assume(vtbl_p == *reinterpret_cast<uintptr_t*>(t_b));

    std::cout << test_sign(t_b) << std::endl;

    return 0;
}

可以看出，代码中实现了一个 C++ 带虚函数类的继承，并 include 了 iostream 这个 C++ 独有的库。

注意到，KLEE 符号执行直接将符号视作连续的内存空间，而并不会解析被符号化的变量的具体含义（例如对于指针类型变量，KLEE 只会符号化指针本身的内存空间，而不会符号化指针所指向地址的内存空间，这也是我没有尝试使用 KLEE 对 STL vector 等数据结构进行符号执行的原因）。因此，如果将带虚函数的类的实例对象符号化，需要使用 klee_assume 保证实例对象的虚函数表指针保持不变，否则将引发运行时错误。

接下来，参考 KLEE mailing list 中的 [klee-dev] Error while using C++ STL, libcxx 这份邮件记录，可以考虑采用如下参数将 C++ 源代码编译为 LLVM bitcode：

1
2
3
4
5
6
7
8
9
LIBCXX_LIB_DIR="/usr/include/c++/9/libc++-install-90/lib"
LIBCXXABI_LIB_DIR="/usr/include/c++/9/llvm-90/libcxxabi/lib"
MY_CXX_FLAGS="-nostdinc++ -stdlib=libc++ -lc++ -lc++abi \
-I/usr/include/c++/9/llvm-90/libcxx/include \
-I/usr/include/c++/9/llvm-90/libcxxabi/include \
-Wl,-L$LIBCXX_LIB_DIR -Wl,-L$LIBCXXABI_LIB_DIR \
-Wl,-rpath=$LIBCXX_LIB_DIR -Wl,-rpath=$LIBCXXABI_LIB_DIR"

clang++ $MY_CXX_FLAGS -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone test_cpp.cpp

可以看出，上方一长串参数的主要目的是使用指定的 libc++ 及其 ABI，保证 KLEE 在符号执行的过程中能正确解析 C++ 库中的函数等。

经过我的实验，似乎只要指定 -stdlib=libc++ 并正确包含指定的 libc++ 及其 ABI 的路径即可，因此我使用的简化版命令行编译参数如下：

1
2
3
4
5
6
7
8
9
$ clang++ \
-stdlib=libc++ \
-I /usr/include/c++/9/llvm-90/libcxx/include \
-I /usr/include/c++/9/llvm-90/libcxxabi/include \
-I ../../include \
-emit-llvm -c \
-g \
-O0 -Xclang -disable-O0-optnone \
test_cpp.cpp

在对生成的 LLVM bitcode 进行符号执行时，必须添加 --libc=uclibc --libcxx 这两个参数，否则可能在符号执行过程中产生找不到 libc 或 libc++ 符号的问题。

使用正确的 KLEE 参数后，符号执行成功，并且在控制台输出中可以看出 KLEE 完整覆盖了三条可能的执行路径：

1
2
3
4
5
6
7
8
9
$ klee --libc=uclibc --libcxx test_cpp.bc
...
0
-11


KLEE: done: total instructions = 67511
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

为 KLEE 添加浮点数支持

截至 2021 年 01 月 14 日，在 KLEE Open Projects 页面上可以了解到，KLEE 暂时缺乏浮点数符号化运算的支持。虽然已有名为 KLEE-Float 的支持浮点数的分支，但 KLEE 官方维护人员认为该分支对 KLEE 原有的表达式结构做了侵入式的修改，而且直接将浮点数符号化导致 KLEE 需要依赖运算速度较慢的浮点数约束求解器。KLEE 官方希望浮点数符号化的实现能基于定点数计算 (fixed-point arithmetic)，以保证 KLEE 符号执行的效率。

我虽然暂时没有能力实现一套基于定点数计算的浮点数符号化方案，但在简略分析 KLEE 与 KLEE-Float 的源代码 diff、参考现有的分支合并尝试 KLEE floating-point support. 后，成功将 KLEE-Float 的分支合并进 KLEE 主分支的最近一次提交，并经本地编译测试，确认可以做到浮点数符号化、uClibc 与 POSIX 环境、libc++ 三者同时支持，并已将源代码放置在 Github 仓库 jywhy6/klee 中，欢迎感兴趣的朋友下载体验 (cmake 编译参数无需更改)。