符号执行从入门到放弃

基本原理

在不执行程序的前提下，用符号值表示程序变量的值，然后模拟程序执行来进行相关分析

使用符号执行分析一个程序时，使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

传统符号执行技术

void foobar (int a, int b) {
	int x = 1, y = 0;
	if (a != 0) {
		y = 3 + x;
		if (b == 0)
			x = 2 * (a + b);
	}
	assert (x-y != 0);
}

对于foobar，确定哪些输入参数可以使assert失败

a、b两个四字节参数，每个有$2^{32}$种情况，若随机生成并执行程序，不太可能准确的获得使断言失败的输入，遍历所有情况也不可行。但符号执行克服了这些限制，并且可以推断出所有的输入而不是单个输入值

通过静态分析代码不能确定的值（例如函数的实际参数和从流中读取数据的系统调用的结果），用符号$α_i$表示

在任何时候，符号执行引擎都维持着一个状态$(stmt,σ,π)$

其中

1. stmt是下一条要执行的语句，目前假设它可以是赋值、条件分支或跳转

2. σ是一个符号储存，它将程序变量与具体值的表达式或$α_i$的表达式相关联

   如图，对于B，a与$α_i$的表达式$α_a$关联，x与具体值的表达式1相关联

3. π表示路径约束，表示在执行中能够到达stmt的$α_i$的表达式，初始为True

   如图，对于C，若要到达stmt(y=3+x)，需要使$α_a≠0$

得到三种结果，只有一种可以使断言失败，通过约束求解可以得到$α_a$和$α_b$的具体值$(2,0)$

现代符号执行技术

现代符号执行技术的关键要素之一是它们混合具体(Concrete)执行和符号(Symbolic)执行的能力。

Concrete和Symbolic两个洋文单词拼起来就是Concolic

执行生成测试

执行生成测试(Execution-Generated Testing(EGT))

EGT在执行每个操作之前，检查每个相关值是具体的还是符号的，然后动态地混合具体和象征性的执行

如果所有相关值都是精确的，就具体的执行，否则这个操作将被象征性的执行

动态符号执行

动态符号执行(Dynamic Symbolic Execution(DSE))

除了符号储存和路径约束，引擎还维护着一个具体储存(concrete store)

选择任意输入开始后，通过同时更新具体储存、符号储存和路径约束来具体和象征性的执行程序

不同于传统的符号执行技术，动态符号执行需要维护程序执行时的整个精确状态，因此它需要一个精确的初始值

例

void foobar (int a, int b) {
	int x = 1, y = 0;
	if (a != 0) {
		y = 3 + x;
		if (b == 0)
			x = 2 * (a + b);
	}
	assert (x-y != 0);
}

选择a=1，b=1作为输入参数，在这种条件下具体执行路径为A->B->C->E->G

除了图中的符号储存外，具体储存在整个过程的状态如下

断言成功，通过否定最后的路径约束即$α_b≠0$生成新的控制流路径

此时求解器将生成一个新的输入，满足$α_a≠0$且$α_b=0$，此时执行路径为A->B->C->E->F

符号执行面临的问题

复杂结构语义和操作语义的建模

如何处理指针、数组或其他复杂对象

操纵指针、数据结构的代码不仅会产生符号储存的数据，还会产生由符号表达式描述的地址

全局分析

在程序全局分析过程中，当对一个规模较大、包含很多的过程间调用的程序进行上下文敏感的分析时，每当一个过程调用了另一个过程时都进入子过程进行分析，虽然会很精确，但这种方式可能会造成大量的时间空间开销，而使分析过程异常终止或在用户可接受的时间内无法完成。

路径状态空间爆炸

如何处理路径状态空间爆炸

每一个分支条件语句都可能会使当前的路径再分支出一条新的路径，而这是指数级增长的

因此，符号执行引擎不可能在合理的时间内详尽地探索所有可能的状态

约束求解

不能高效求解，在可接受的时间内无法完成，如非线性

参考

Cadar C , Sen K . Symbolic execution for software testing: Three decades later[J]. Communications of the ACM, 2013, 56(2):82-90.

Baldoni R , Coppa E , D’elia, Daniele Cono, et al. A Survey of Symbolic Execution Techniques[J]. ACM Computing Surveys, 2018, 51(3):1-39.