与符号执行的亲密接触

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

符号执行

在这篇分为两部分的博客文章的第一部分中，我将解释什么是符号执行，以及符号执行如何让我们的“推理系统”学习任意二进制文件的输入。在博客文章的第二部分，我将引导您完成在THREADS上展示的迷宫求解示例。

为了描述符号执行的力量，我们将看一个经典计算机科学问题的三个难度递增的迭代：迷宫求解。在讨论了符号执行的力量之后，我将谈谈KLEE，一个基于LLVM的符号执行框架，以及mcsema如何使KLEE能够在仅有二进制的应用程序上运行。

迷宫求解

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

一个示例迷宫。步进空间是空白的，墙是+-|，END标记是#符号，当前路径是X’s。

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

无地图的迷宫求解

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

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

带有假墙的迷宫求解

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

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

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

作弊取胜

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

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

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

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

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来识别二进制应用程序的所有有效输入。