MultiSE: Multi-Path Symbolic Execution using Value Summaries
ABSTRACT
已经提出动态符号执行（DSE）来有效地生成用于真实世界节目的测试输入。不幸的是，DSE技术无法很好地扩展到大型现实程序，因为程序的可行执行路径的数量通常会随着执行路径长度的增加而呈指数级增长。 在本文中，我们提出了MultiSE，一种在符号执行过程中逐步合并状态的新技术，不使用辅助变量。
MultiSE的关键思想是基于状态的替代表示，其中我们将每个变量（包括程序计数器）映射到一组称为值摘要的受保护符号表达式。与传统的DSE和传统的状态合并技术相比，MultiSE具有以下几个优点：值汇总可以在多个路径上共享符号表达式和路径约束，从而避免冗余执行。 MultiSE不引入辅助符号变量，这使得它能够1）即使在合并约束求解器不支持的值时也能取得进展，2）在解析函数调用和跳转时避免使用昂贵的约束求解器调用，以及3）执行大多数操作具体。此外，MultiSE在每个赋值指令处逐步更新值汇总，这使得无需识别连接点并跟踪要在连接点处合并的变量。
我们在公开的开源工具中实现了MultiSE for JavaScript程序。我们在几个程序上对MultiSE的评估表明：1）值汇总是利用多个执行路径上的值共享的有效技术，2）MultiSE可以比传统的动态符号执行快得多，并且3）与传统的状态合并技术相比，MultiSE节省了大量的状态合并。
1 INTRODUCTION
符号执行是一种从程序中自动生成符号模型的技术。它已成功用作各种应用的关键组件，包括为C [20,44,11,10,16]，C ++ [33]，C＃[48]，Java [3,36]生成高覆盖率测试。 ，2,29,42]，PHP [4]，JavaScript [41,43]，x86-binaries [22,47,5]。
象征性执行背后的关键理念是在大约40年前引入的[30,17]。在本文中，我们考虑符号执行的动态变体（DSE），其中使用符号值代替输入的混合值来执行程序。
符号执行技术无法扩展到大型现实程序，因为程序的可行执行路径的数量通常随执行路径的长度呈指数增长。由于符号执行需要探索程序的多个路径，因此尝试缓解此路径爆炸问题至关重要。在这方面，现有技术是一种称为状态合并的技术[19,1,23,32,5,49]，其中从在连接点会聚的多个路径获得的符号状态被合并。例如，考虑条件语句“if p then x = v1 else x = v2”。状态合并将象征性地执行两个分支，并且在连接点处将为x的合并值引入新的符号值，比如x0。 （这些值被称为辅助变量[5,32]，以区别于输入符号值。）符号状态基本上是（x = x0）∧（（p∧x0= v1）∨（∧p∧） x0 = v2））。
我们工作的部分动力是辅助变量引入了几个问题。最重要的一点是，如果合并值（例如v1和v2）在约束求解器的域之外，例如浮点值，函数作为第一类值或对象，则不能使用此技术，因为逻辑公式在这些情况下，上述提到的不合法。例如，JavaScript中的语句“if p then x = 1.2 else x = function（y）{return y + 1}”将生成状态（x = x0）∧（（p∧x0= 1.2）∨（¬p ∧x0= function（y）{re-turn y + 1}））如果我们的约束求解器不支持浮点数或函数数据类型，则这不是合法公式。现有的符号执行技术通常通过避免合并和丢弃其中一条路径来处理这种情况。此外，在合并的值是函数（被视为第一类值）或计算的跳转标签，并且合并的值被包含的情况下，符号执行需要确定继续执行的位置。这些类型的操作在动态类型编程语言（如JavaScript，Python和Ruby）中非常常见。现有技术使用SMT求解器来尝试确定要调用的可能函数集。
在本文中，我们提出了MultiSE，一种新的符号执行框架，它可以在不使用辅助变量的情况下实现状态合并。 MultiSE基于状态的新表示，我们将每个变量（包括程序计数器）映射到一组称为值汇总的受保护符号表达式。对于我们的示例，上面示例状态的值总和表示将是：x→{（p，v1），（¬p，v2）}。
本质上，该表示编码如下事实：如果谓词p成立，则x的值等于v1，否则等于v2。关键思想是将路径约束与变量值分开。值摘要的路径约束部分（例如p和¬p）被限制在约束求解器的域内;但是，值摘要中的值部分（例如v1和v2）可以是包括浮点数，函数的任何符号表达式或具体程序对象。虽然这似乎是一个很小的变化，但它有重要的影响：
-
即使在约束求解器不支持某些合并的值时，MultiSE也经常在合并后执行符号执行，而传统的状态合并则必须丢弃一些路径。只要值摘要的路径约束部分不涉及不支持的值类型，就是如此。约束求解器仅用于状态的路径约束组件，例如，用于确定不可行路径，或者为启用一个特定路径的输入产生满足值。我们在第5节中表明，如果使用传统的状态合并执行，大约一半的基准测试将需要除整数或字符串以外的辅助变量，有时为数千，对于高达60％的州合并;传统的状态合并必须在所有这些合并中丢弃可行路径，而MultiSE可以在不丢弃路径的情况下继续。
- MultiSE可以更经常地利用符号执行中的常见优化：尽可能执行混合计算。由于MultiSE不引入辅助变量，因此值摘要中的值是具体的，只要它们不依赖于输入的数据。在我们的例子中，如果v1为0.1且v2为0.2，并且条件语句后跟“x = x + 1”，则MultiSE将具体执行增量操作，并产生值总和{（p ，1.1），（¬p，1.2）}而不是符号状态（x = x0 +1）∧（（p∧x0= 0.1）∨（¬p∧x0= 0.2））其中x的值是象征性地计算的。此优化可能适用于任何数据类型，如函数，数组，浮点数和对象等;在这种情况下，如果有这些数据类型的辅助变量，我们不需要担心会出现不支持的符号表达式。
- 传统的状态合并必须扫描整个两个状态，以便在连接点合并，以便构造合并状态。相比之下，MultiSE使用一种新颖的算法来更新值摘要，因为它处理每条指令并实现隐式和递增合并的效果，即使存在非结构化或计算的控制流。
我们在公开的开源工具1中实现了MultiSE for JavaScript程序。我们使用二元决策图（BDD）[9]来简明地表示和有效地操纵路径约束和值总结的保护。我们在多个程序上对MultiSE的评估表明，与传统的状态合并技术相比，MultiSE的运行速度明显快于传统的DSE，并实现更精确的状态合并。