与符号执行的亲密接触

在THREADS 2014会议上，我展示了mcsema的一项新功能：能够对仅以二进制形式存在的软件使用符号执行框架KLEE。在演讲中，我描述了如何利用mcsema和KLEE来学习一个从未见过的二进制文件中定义的未知协议。在我们的示例中，我们成功解析了穿越迷宫所需的一系列步骤。我们在DARPA网络大挑战赛中的竞赛正需要这种能力——我们的"推理系统"将没有任何先验知识或人工指导，却必须学会与数十、数百甚至数千个具有独特输入的二进制程序进行交互。

符号执行

在这篇分为两部分的博客文章的第一部分，我将解释什么是符号执行，以及符号执行如何让我们的"推理系统"学会为任意二进制程序生成输入。在第二部分，我将引导您完成在THREADS会议上展示的迷宫求解示例。为了说明符号执行的威力，我们将通过计算机科学经典问题——迷宫求解的三个难度递增版本来进行阐述。在讨论完符号执行的强大功能后，我将介绍基于LLVM的符号执行框架KLEE，以及mcsema如何让KLEE能够在仅二进制应用程序上运行。

迷宫求解

迷宫求解是计算机科学一年级课程中的经典问题之一。简单来说，问题是这样的：你获得了一个迷宫地图，任务是从起点找到通往终点的路径。更正式的定义是：迷宫由一个矩阵定义，其中每个单元格可以是通道或墙壁。可以移动到通道单元格，但不能移动到墙壁单元格。唯一有效的移动方向是上、下、左或右。从一个单元格到另一个单元格的移动序列称为路径。某个单元格被标记为起点（START），另一个单元格被标记为终点（END）。给定这个迷宫，找到从起点到终点的路径，或者证明不存在这样的路径。

一个示例迷宫。通道空间为空白，墙壁为+-|，终点标记为#号，当前路径为X。

迷宫问题的典型解决方案是枚举从起点开始的所有可能路径，并搜索终止于终点的路径。该算法在这个Stack Overflow帖子中有简洁的总结。该算法有效是因为它拥有迷宫的完整地图。地图用于创建有限的有效路径集合，可以快速搜索这个集合以找到有效路径。

无地图的迷宫求解

在人工智能课程中，可能会遇到一个更困难的问题：在没有地图的情况下解决迷宫。在这个问题中，求解器必须在找到从起点到终点的路径之前发现地图。更正式地说，问题是：你获得了一个回答迷宫路径问题的预言机（oracle）。当给定一个路径时，预言机会告诉你该路径是否解决了迷宫、撞墙或移动到通道位置。给定这个预言机，找到从起点到终点的路径，或者证明没有路径。

这个问题的解决方案是回溯。求解器将一次构建一个移动的路径，在每个移动时询问预言机关于路径的情况。如果尝试的移动撞墙，求解器将尝试另一个方向。如果没有方向有效，求解器将返回到上一个位置并尝试新方向。最终，求解器将找到终点或访问每个可能的位置。回溯有效是因为通过预言机的每个回答，求解器都能了解更多地图信息。最终，求解器将学到足够的地图信息来找到终点。

带有假墙的迷宫求解

让我们假设一个更困难的问题：带有假墙的迷宫。也就是说，有些墙壁实际上是通道。由于有些墙壁是假的，求解器在询问完整解决方案之前无法从预言机中学到任何东西。如果这不太清楚，想象一个完全由假墙构成的地图：对于任何路径，除了解决迷宫的路径外，预言机总是回答"墙"。更正式地说，现在的问题是：给定一个只验证从起点到终点的完整路径的预言机，解决迷宫。

这比以前困难得多：求解器无法学习地图。唯一的通用解决方案是询问预言机关于每个可能的路径。求解器最终会猜到一个有效路径，因为它必须在所有路径的集合中（假设迷宫是有限的）。这种"暴力"求解器比之前的更强大：它将解决所有迷宫，无论有无地图。

尽管强大，暴力求解器有一个巨大的问题：它缓慢且不实用。

作弊取胜

最后一个问题等同于以下更一般的问题：给定一个验证解决方案的预言机，找到一个有效的解决方案。理想情况下，我们想要比暴力猜测更快找到有效解决方案的方法。特别是在处理通用问题时，因为我们甚至不知道输入是什么样子的！

所以让我们制作一个"通用问题求解器"。暴力破解缓慢且不实用，因为它按顺序尝试每个具体输入。如果求解器可以同时尝试所有输入呢？人类一直在这样做而不加思考。例如，当我们解方程时，我们不会尝试每个数字直到找到解。我们使用一个可以代表任何数字的变量，并通过算法识别答案。

那么我们的求解器如何同时尝试每个输入呢？它将作弊取胜！我们的求解器手中有一张王牌：预言机是一个真正的程序。求解器可以查看预言机，分析它，并在不猜测的情况下找到解决方案。遗憾的是，这对每个预言机都是不可能的（因为你会遇到停机问题）。但对于许多真实的预言机，这种方法有效。

例如，考虑以下声明赢家或输家的预言机：

1
2
3
4
5
6

x = input();
if(x > 5 && x < 9 && x % 4 == 0) {
  winner();
} else {
  loser();
}

求解器可以确定赢家输入必须是一个大于5、小于9且能被4整除的数字。这些约束可以转化为一组线性方程并求解，显示唯一的赢家值是8。

一个假设的问题求解器可以这样工作：它将把输入到预言机的内容视为一个符号。也就是说，不是选择特定值作为输入，而是将该值视为变量。然后，求解器将应用与预言机程序中不同分支对应的约束。当求解器在预言机中找到"有效解决方案"状态时，输入的约束被求解。如果约束可以求解，结果将是一个达到有效解决方案状态的具体输入。问题求解器通过将预言机转化为线性方程组来同时尝试每个可能的输入。

这个假设的问题求解器是真实的：发现约束的部分称为符号执行框架，解方程的部分称为SMT求解器。

未来已来

有几个软件包将符号执行与SMT求解器结合来分析程序。我们将关注KLEE，因为它与LLVM字节码配合使用。我们可以使用KLEE作为通用问题求解器，在给定验证这些输入的预言机的情况下找到所有有效输入。KLEE可以解决带有隐藏墙壁的迷宫：Felipe Manzano有一篇优秀的博客文章展示了如何使用KLEE来解决 exactly such a maze。

那么mcsema与此有什么关系呢？嗯，KLEE适用于用LLVM字节码编写的程序。在mcsema之前，KLEE只能分析带有源代码的程序。使用mcsema，KLEE可以成为任意二进制应用程序的问题求解器！例如，给定一个检查带有隐藏墙壁的迷宫解决方案的编译二进制文件，KLEE可以找到通过迷宫的所有有效路径。或者它可以做更有用的事情，比如自动生成具有高代码覆盖率的应用程序测试，甚至可能在二进制程序中找到安全漏洞。

但回到迷宫求解。在本博客文章的第2部分，我们将取一个解决迷宫的二进制文件，使用mcsema将其转换为LLVM，然后使用KLEE找到通过迷宫的所有有效路径。更具体地说，我们将取Felipe的迷宫预言机并将其编译为Linux二进制文件。然后，我们将使用mcsema和KLEE找到所有可能的迷宫解决方案。所有操作都将在不修改原始二进制文件的情况下完成。KLEE唯一知道的是如何提供输入以及如何检查解决方案。本质上，我们将展示如何使用mcsema和KLEE来识别二进制应用程序的所有有效输入。