Kirenenko：像污点分析一样实现动态符号执行

 

故事

在 2017 年下半年，Byoungyoung 和我讨论如何使模糊测试在翻转条件分支上更高效。他建议我们可以使用动态污染分析来找到会影响目标分支的输入字节，这样我们就可以专注于改变较小的字节集，而不是整个输入。然而我们面临的一个挑战是，如何进一步提高为这些字节找到一个令人满意的赋值的效率，这样我们就可以翻转分支。我们考虑的一个办法是，得到一堆输入/输出对，利用深度神经网络(DNN)的通用近似定理来训练一个模型(特定于目标分支);然后我们可以利用这个模型来寻找满意的输入。当时，我读了一些关于程序综合的论文，了解到这个想法可能不会实现的很好因为 (1) 神经网络可能不能近似复杂的分支约束，(2) 即使它可以近似，训练模型可能需要许多输入/输出对，(3) 经过训练的模型通常不能用于解决其他分支问题。相反，我建议我们可以使用这些输入/输出对来合成分支约束的符号公式，然后让 SMT 求解器来解决它。这是受到当时一些研究的启发 (例如 DeepCoder),这些研究表明如果我们想要基于一些输入/输出对来近似未知函数 f,使用机器学习来指导合成一个近似函数 f' ，从而产生相同的输入/输出对，这可能比使用 DNN 直接近似 f 更好。所以我们开始构建 SynFuzz。不幸的是，由于许多污点引导的模糊测试器（包括 Angora 和 RedQueen ）已发布，因此我们未能发布 SynFuzz

但是，当我们准备在 2019 年夏季重新提交论文时，我意识到我们实际上可以使用相同的污染分析框架来追踪完整的符号公式，从而避免了繁琐的合成过程。更重要的是，这实际上引出了非常有前景的动态符号执行引擎，因为

• 这些符号公式以相似的污点分析的速度收集，这比以前基于解析的方法（例如 KLEE 和 angr ）要快得多。
• 符号公式是在 LLVM IR 级别上收集的，因此它们比在二进制级别上收集的符号公式更简单,并且更易于求解。

在这篇博文中，我将解释 Kirenenko 的一些技术细节。

由于实现非常简单（对 LLVM 中的数据流清理器进行了小小的修改），所以我认为不值得为此撰写论文。因此，我只是对源代码进行了开源，希望人们能基于它构建更多有趣的工具。

 

问题表述

背景：动态数据流分析

动态数据流分析旨在根据其运行时数据和控件依赖性来跟踪程序变量的其他属性。为方便起见，分析框架将每个程序变量与代表其属性的标签（也称为元数据）相关联。特定的动态数据流分析需要定义四个策略：

• 标签解释定义了要跟踪的属性。典型的解释包括数据是否可信赖以及数据是否包含敏感（例如，个人健康）数据。
• 标签来源定义了引入非默认标签的位置，示例包括读取测试数据、不受信任数据或敏感数据的 api 。
• 标签传播定义了如何通过执行的指令来组合或变换不同的标签。例如，当跟踪来自 Internet 的不可信输入数据的传播时，不可信标签与任何其他标签的组合总是以不可信标签结尾。
• 标签接收器定义在何处以及如何使用其他运行时属性。例如，检测隐私数据泄漏的策略将检查离开本地主机（例如，发送到网络）的数据，以确保其标签不敏感。

安全性中使用的最常见的动态数据流分析形式之一是动态污点分析，其中有两个标签:
tainted 和 untainted 。如上所述，这 tainted 可能意味着不可信任，例如来自网络或用户空间的数据；这也可能意味着敏感信息。动态污点分析已在许多安全应用程序中使用，我将不做列举。

 

背景：动态符号执行

符号执行将程序输入视为符号值，而不是具体值。程序变量（包括存储器和寄存器内容）然后可以表示为符号表达式。符号执行引擎维护（1）符号状态，该状态将程序变量映射到其符号表达式，以及（2）一组路径约束，该路径约束是符号表达式上无量词的一阶公式。为了生成允许程序遵循相同执行轨迹的具体输入，符号执行引擎使用路径约束来向 SMT 求解器查询符号值（即输入字节）的可满足性和可行分配。

观察：用于数据流分析的公式构建

如果我们仔细考虑，我们可以看到保持符号状态是动态数据流分析的一种特殊形式：

• 标签解释：在符号执行中，变量的标签是其符号表达。
• 标签来源：在测试用例生成中，我们将输入字节标记为符号。
• 标签传播：当标签（符号表达式）合并时，我们创建一个新表达式，该新表达式根据操作将“结果”组合在一起。如果表达式存储为抽象语法树（AST），则合并意味着创建一个新的 AST 节点，并将操作数 AST 作为子节点。
• 标签接收器：在条件分支（或其他有趣的地方），如果某些约束可行（例如，如果分支条件可以评估为 true ），则使用收集的符号表达式咨询 SMT 求解器 ；如果是这样，请求一个模型（任务）。

Kirenenko 是基于此观察结果而构建的。

 

技术细节

背景：DFSan

Kirenenko 基于 LLVM 项目中的 DataFlowSanitizer (DFSan) 构建。DFSan 是一个字节粒度动态数据流分析框架。它执行源代码（实际上是IR）级别的检测以跟踪运行时数据流。这在两个级别上完成。对于 LLVM 寄存器中的数据（IR值），它使用影子寄存器存储标签。对于内存中的数据，它使用高度优化的影子存储器将每个内存字节映射到影子存储器中的相应标签。与其他动态污点分析框架相比，DFSan 最具吸引力的设计是 DFSan 不会在标签本身中存储任何信息。相反，标签是另一个元数据结构的索引，该结构称为 union table，它存储实际的输入依赖项。而且，为了跟踪按字节粒度的数据流，联合表已被构造为树：当合并两个标签（即两组输入依赖项）时，DFSan 将分配一个新标签（联合表条目）并分配两个标签作为子节点。

struct dfsan_label_info {
  dfsan_label l1;
  dfsan_label l2;
  const char *desc;
  void *userdata;
};

dfsan_label __dfsan_union(dfsan_label l1, dfsan_label l2) {
  // simplified
  dfsan_label label =
    atomic_fetch_add(&__dfsan_last_label, 1, memory_order_relaxed) + 1;
  __dfsan_label_info[label].l1 = l1;
  __dfsan_label_info[label].l2 = l2;
  return label;
}

请注意，整个联合表在初始化期间被分配为一个大数组，因此分配一个新条目非常容易，只需分配一个 atomic_fetch_add 即可。

扩展联合表

按照问题的表述，可以很直观地看出，要跟踪符号表达式，而不仅仅是输入依赖项，我们可以将联合表条目扩展到 AST 节点，并在合并两个标签（两个子表达式）时跟踪更多信息。

struct dfsan_label_info {
  dfsan_label l1; // symbolic sub-expression, 0 if the operand is concrete
  dfsan_label l2; // symbolic sub-expression, 0 if the operand is concrete
  u64 op1;        // concrete operand, 0 if the operand is symbolic
  u64 op2;        // concrete operand, 0 if the operand is symbolic
  u16 op;         // the operation of the node, using LLVM IR operations
  u16 size;       // size of the result
};

dfsan_label __taint_union(dfsan_label l1, dfsan_label l2, u16 op, u16 size,
                          u64 op1, u64 op2) {
  // omitted  
}

从概念上讲，就这么简单。我们需要对工具的 pass 进行修改，以便我们可以跟踪其他信息。我们还需要修改方式 load 和 store 处理方式：当存储一个大于一个字节的表达式时，我们需要使用该 extract 操作将其分解；当加载大于一个字节的表达式时，我们需要 cancat 子表达式。最后，我们还需要添加一个哈希表来对符号表达式进行重复数据删除，以使它们不会破坏联合表。

生成新的测试输入

为了生成新的测试输入，我们对条件 branch 指令和 switch 指令（即​​LLVM IR指令）进行了检测，以在运行时调用回调函数。在回调函数内部，我们将遍历联合表条目（即遍历AST）以将 LLVM IR 级别的 AST 转换为 Z3 AST，然后咨询 Z3 SMT 求解器以检查分支目标的可行性。如果是这样，我们获取模型并生成一个新输入。对于此步骤，我们遵循 QSYM 的作用：跟踪嵌套分支，如果嵌套分支求解失败，则进行乐观求解。

额外的库

Kirenenko 的最大限制是它对第三方库的支持，它继承自 DFSan。具体来说，DFSan 执行源代码（IR）级检测，因此它无法传播所检测的动态库的数据流。一个例子是 libc 。为了支持这些库，我们要么需要创建包装函数来指定应如何传播数据流（请参阅参考资料 dfsan_custom.cc ），要么使用工具编译该库。虽然其他基于源代码的符号执行工具（例如 KLEE 和 SymCC ）也面临相同的问题，但确实使其不如 QSYM 等基于二进制的工具方便。

 

性能

Kirenenko 之所以快是因为以下三个原因：

1. 符号约束收集是以本机速度完成的，或者使用 SymCC 的术语，基于编译，而不是基于解释。
2. 符号约束是在 LLVM IR 级别上收集的，因此它们更简单，更快速地解决，如 SymCC 的评估所示。
3. 它建立在高度优化的清理器基础结构之上：快速访问标签，快速访问每个 AST 节点以及快速分配每个 AST 节点。

那么到底有多快？这是我得到的一些快速测试结果，请随时为代码评分并尝试一下。

我们可以看到，尽管它仍然比本机执行慢很多，但是现在收集符号约束本身非常快，瓶颈是约束求解。我没有提供 QSYM 和 SymCC 的编号，如果您有兴趣，可以进行自我测试。

这是将 Kirenenko 与 AFL++ 配对时的一些 FuzzBench 的结果。