【S2E】路径引导功能设计

工具
,

整理一下之前实现的路径引导相关的内容。

问题描述

已有使程序崩溃的 seed，在 S2E 中复现相同的崩溃，从而借助符号执行分析。

具体来说是，在 S2E 将程序输入替换为符号变量，但执行路径要遵循 seed 具体执行时的路径，从而在 S2E 中探索程序崩溃时的状态。

解决方案概述

已知符号执行在每次执行至分支时会 fork 出两个状态，分别探索这两个不同的分支。因为我们已经有 seed，因此可以判断出具体执行时会选择哪个分支，此时只需要探索该分支即可。根据这种方式，既能实现剪枝（减少开销），也能将符号执行最终引导至目标点（崩溃点）。

判断方法是类似污点分析的方式。每次执行到条件分支语句时，符号执行可以捕获条件表达式，进而分析出该条件被哪些输入的字节所影响。通过查找 seed 对应的字节，就能计算出具体执行时，该条件为 true 还是 false。此时我们也令符号执行选择和具体执行相同的分支去执行即可。

举栗说明

下面用一个栗子来说明。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
#include <stdio.h>
#include <stdlib.h>
int main()
{
    char buf[64] = {0,};
    read(0, buf, 64);

    if (buf[0] == 'X') {
        if (buf[1] + buf[2] == 'Y' + 'Z') {
            puts("success!");
            return 0;
        }
        exit(2);
    }
    exit(1);
}

该程序从 stdin 中读取 64 字节保存至 buf 缓冲区。后续有 2 个条件分支语句，产生 3 条分支。这两个分支表达式分别为：

  1. buf[0] == 'X'

  2. buf[1] + buf[2] == 'Y' + 'Z'

而在 S2E 中，这样的条件表达式使用 KQuery 语言描述。（KQuery 由 KLEE 定义，而 S2E 的符号执行是基于 KLEE 实现）。官方文档：https://klee.github.io/docs/kquery/

因此在 S2E 执行过程中，上述两条分支表达式分别为：

1
2
3
4
5
6
7
8
9
10
1. (Eq false
     (Eq 0x0
         (Extract w8 0 (Add w64 0xffffffffffffffa8
                                (ZExt w64 (Read w8 0x0 v0___symfile____tmp_input_0___0_256_symfile___0))))))

2. (Eq false
     (Eq 0x0
         (Extract w32 0 (Add w64 0xffffffffffffff4d
                                 (ZExt w64 (Extract w32 0 (Add w64 (ZExt w64 (SExt w32 (Read w8 0x0 v2___symfile____tmp_input_0___2_256_symfile___2)))
                                                                   (ZExt w64 (SExt w32 (Read w8 0x0 v1___symfile____tmp_input_0___1_256_symfile___1))))))))))

阅读一下 KQuery 的官方文档，就可以对这个表达式进行解释了。需要先搞清楚这个表达式：v0___symfile____tmp_input_0___0_256_symfile___0 ，这个是 S2E 中的独特写法，它是 KQuery 语言描述的一个数组，对应的是一字节的符号变量。这个字符串的命名规则在 https://github.com/S2E/s2e/blob/master/libs2eplugins/src/s2e/Plugins/ExecutionTracers/TestCaseGenerator.cpp 中有解释，下面直接引用了：

1
 v0___symfile____(guest_file_name)___(chunk_id)_(number_of_chunks)_symfile___0

  • (guest_file_name) 表示 guest 使用的符号文件的名字，这个例子是 tmp_input_0，因为 bootstrap.sh 里写了符号文件是 input-0；

  • (chunk_id) 表示的是该 chunk 在符号化文件中的位置；

  • (number_of_chun) 表示一共有多少个 chunk；

  • 注：默认每个 chunk 表示 1 字节。

所以，表达式 v0___symfile____tmp_input_0___0_256_symfile___0 的含义其实就是：符号化文件 input-0 中的第 0 字节，该符号化文件共有 256 字节。由于我启动 S2E 时，是以这样的形式运行目标程序的：cat "${SYMB_FILE}" | "${TARGET}" ，即把符号化文件的内容，重定向到目标程序作为程序的标准输入，因此表达式 v0___symfile____tmp_input_0___0_256_symfile___0 最终可以被解释为：

程序标准输入的第 0 个字节（且程序共接受 256 个字节作为标准输入）。

接下来继续回到第一个表达式：

1
2
3
4
(Eq false
     (Eq 0x0
         (Extract w8 0 (Add w64 0xffffffffffffffa8
                                (ZExt w64 (Read w8 0x0 v0___symfile____tmp_input_0___0_256_symfile___0))))))

Read 表示读取操作。前面简单的提到，v0___symfile____tmp_input_0___0_256_symfile___0 是一个数组，不过数组中仅有一个元素，大小为 1 字节。Read w8 0x0 array 操作表示从数组 array 中读取第 0 个元素，宽度为 8 bit，即 1 字节。

ZExt 是一个截断操作，且截断后所有高位设置为 0。由于我们已经知道仅读取 1 字节，所以这个截断 64 bit 等于什么也没做。

Add 是数学操作，把刚刚取出来的 1 字节表达式和 0xffffffffffffffa8 相加。0xffffffffffffffa8 实际上是 0x58 （即：ascii 'X' ）的相反数的补码。其实就是将取出的字节减去 0x58。

Eq 对比了刚才相减的结果是否为 0。再外面一层 Eq 含义是判断上次对比的结果是否为 False。

综上所述，该表达式可以被解释为：

取程序输入的第 0 个字节（符号变量），令其减去 0x58，判断结果是否为 0。

即：判断程序输入的第 0 字节是否为字符 ‘X’ 。

同时，当我们解析出该条件表达式和程序输入的第 0 字节有关时，我们可以直接从 seed 中取出第 0 字节，将其带入到表达式中，计算出结果。计算结果为 True，就表示具体执行会走向 True 分支，反之则表示具体执行会走向 False 分支。接下来我们令符号执行探索相同的路径即可。

分支处理

前面已经识别出应该选择 True 还是 False 分支了。下一步就是如何使 S2E 探索我们指定的分支，且避免探索另一条分支。

早期版本中，S2E 在 onStateFork 事件中并未提供条件表达式。当时的处理思路是：在 ExecutionState 中新增一个标志位，先允许 S2E fork 出两个不同的状态（ExecutionState），对于我们需要探索的路径对应的状态，将其标志位置为 True，反之置为 False。当 ExecutionState 执行时，如果标志位为 False，则直接 Terminate，从而阻止不必要路径的探索。

新版本中，onStateFork 事件提供了条件表达式：

1
2
3
4
5
6
7
8
9
10
/* libs2ecore/include/s2e/CorePlugin.h */
... ...
    ///
    /// Signal emitted when the state is forked.
    ///
    sigc::signal<void,
                 S2EExecutionState* /* original state */,
                 const std::vector<S2EExecutionState*>& /* new states */,
                 const std::vector<klee::ref<klee::Expr>>& /* new conditions */>
        onStateFork;

因此，直接注册该事件，将表达式计算结果不匹配的状态直接杀死即可。