符号执行 Symbolic Execution

基本原理

符号执行是一种经典的程序分析技术,它使用符号值 (symbolic value) 而不是具体值 (concrete value) 作为程序输入。因此,由这些输入变量组成的符号表达式可以被用来表示程序中其他变量的值。在符号执行过程中,对于任一程序位置,对应的程序状态包括:

  • (1) 程序变量的符号表达式值;
  • (2) 由输入变量的符号表达式组成的路径约束 (path constraint,记为 pc),即只有满足该约束公式的输入值才能到达约束条件对应的程序位置,形式上是一个布尔表达式;
  • (3) 指向下一条将要被执行的程序语句的程序指针。

对于一个待测程序 PP, 假设它有 nn 个输入变量,如 x1,...xi,...,xnx_{1},...x_{i},...,x_{n},在符号执行前,这些输入变量将被初始化为符号值,即 x1=X1,...,xi=Xi,...,xn=Xnx_1 = X_1,...,x_i = X_i,..., x_n=X_n。于是程序 PP 中的其他变量的值可以被表示为只包含上述符号(即 x1,...,Xi,...,Xnx_1,...,X_i,...,X_n)的符号表达式,即 exp(X1,...,Xi,...,Xn)exp(X_1,...,X_i,...,X_n)。在执行过程中,程序指针指向下一条将要被执行的语句 stmtstmt,

  • (1)当 stmtstmt 为赋值计算语句时,相关变量的符号值将在执行stmtstmt 后被更新;
  • (2)当 stmtstmt 为条件判断语句时,假设对应的条件约束为C(X1,...,Xi,...,Xn)C(X_1,...,X_i,...,X_n),那么在执行 stmtstmt 时,原先的路径约束 pp 将被这个新的约束条件所更新。

具体来说,符号执行技术将检查当前条件语句的两个执行方向是否都可行,即检查真分支方向和假分支方向的路径约束是否可以被满足,这里真分支方向上的路径约束为 pcC(X1,...,Xi,...,Xn)pc \land C(X_1,...,X_i,...,X_n),
假分支方向上的路径约束为 pc¬C(X1,...,Xi,...,Xn)pc \land \neg C(X_1,...,X_i,...,X_n),只要对应的路径约束存在可行解,那么符号执行将在对应的路径方向上继续进行下去,否则将在那个方向上停止。这个过程将不断进行下去,直到所有的程序路径都被执行到,因此符号执行技术是一种以程序路径为分析对象,不断进行约束求解的程序分析方法。由于程序P中可能存在许多分支语句。于是可以搜索的程序路径方向也会有许多,如何确定优先搜索哪个路径方向的算法就被称之为路径搜索策略。路径搜索策略的设计好坏将直接影响测试用例生成的效率,尤其是在基于特定覆盖标准生成对应的测试用例的情况下。

动态符号执行 Dynamic Symbolic Execution

对于经典的符号执行技术,不可能总能求解出所有的路径约束,特别是当路径约束包含有系统库函数(其源代码实现不可获得)或者非线性运算符时,符号执行的能力就被大大限制。事实上,求解一般性约束本身就是不可判定的。为了克服这个困难, Godefroid 和 sen 等人把符号执行与具体执行结合在了一起,该混合技术就称为动态符号执行。它和经典的静态符号执行技术一样,沿着程序路径来收集路径约束,但是它的路径都是由输入变量的具体值执行得到的。如果收集到的路径约束过于复杂,超过了底层约束求解器的能力,那么这些具体值将通过值替换的方式简化约束,从而能够求解出路径约束。

动态符号执行通常从一条执行路径(由某个初始的程序输入执行得到)出发,并进入如下的迭代:从一条执行路径 p=l1,...,li,...lnp = l_1,...,l_i,...l_n 上,动态符号执行技术选择某个条件语句被执行过的某个分支(即一个分支节点)。然后把从 l1,...,li1l_1,...,l_{i-1} 收集到的路径约束与在 lil_i 上被执行分支对应的约束的非(negation)合并在一起,求解之,得到对应的一个新的测试输入。这个测试输入将在下一次选代中被用作一个新的测试用例,并能执行出一条新的路径 p=l1,...,li1,lip' = l_1,...,l_{i-1}, l_{i}' 这条路径在 lil_{i}' 控制点位置与原路径 pp 发生偏离,其中是原先在 lil_i 位置执行到的分支的另外一个分支方向,但路径 pppp 共享相同的路径前缀 l1,...,li1l_1,...,l_{i-1}

可见,动态符号执行技术也是***基于路径的测试方法***,对程序路径进行逐条搜索,并生成对应的测试用例,直到所有的程序路径被遍历(由于程序路径一般是无限的,所以通常会通过限定测试时间的方式限定符号执行的时间。

基于模型的测试

基于模型的测试(model-based testing)以表示待测软件的某种抽象模型为基础,从该模型中以一定的策略生成测试用例,然后在实际软件上执行这些用例,并观察软件行为是否符合规格需求的一类测试方法。该测试技术一般应用于黑盒测试中,即不需要被测系统的源码实现,但是需要事先建立用于描述待测软件的行为的模型。但通常这个行为模型为抽象模型,从这个模型中产生的测试用例也一般是抽象层次的测试用例,因此需要增加具体特定的信息后,才能在待测软件上执行。

在基于模型的测试中,有限状态机模型(Finite State Machines,FSM)是种用于描述软件行为的常用模型,它可以刻画被测软件的不同状态,以及在接受相关外部输入事件后,软件各个状态之间的转移关系。

定义(有限状态机模型).

有限状态机模型 MM 可以被记为一个五元组
M=(Q,Σ,σ,q0,F)M=(Q,\Sigma,\sigma,q_0,F),其中:

  • QQ 表示被测软件的所有状态集合,q(qQ)q (q\in Q) 表示软件的一个状态。
  • Σ\Sigma 表示被测软件所能够接受的外部事件,e(eΣ)e (e\in \Sigma) 表示一个外部事件。
  • σ\sigma 表示被测软件状态之间的转移函数,即 σ:Q×Σ Q\sigma:Q \times \Sigma \ \rightarrow Q,它接受一个状态 q1q_1 和一个外部事件 ee 为输入,以另外一个状态 q2q_2 为输出,即被测软件从个状态迁移到另外一个状态。
  • q0q_0 表示被测软件的起始状态,且 q0Qq_0\in Q
  • FF 表示被测软件的终止状态集合,它是 QQ 的一个子集。

在基于模型的测试中,测试人员需要按照一定的测试策略从模型中生成测试用例,以满足测试需求。其中,比较常用的测试策略有节点覆盖(也称为状态覆盖)、边覆盖(也称为事件覆盖)。节点覆盖要求,生成的测试集 TT 能够覆盖到模型上的所有节点,即状态集 QQ;边覆盖要求,测试集T能够覆盖到模型上的所有的边,即事件集 Σ\Sigma

========

Symbolic Execution

Symbolic execution is a classic program analysis technique that uses a symbolic value instead of a concrete value as a program input. Therefore, a symbolic representation consisting of these input variables can be used to represent the values of other variables in the program. During the symbol execution process, for any program location, the corresponding program state includes:

  • (1) the symbolic expression value of the program variable;
  • (2) a path constraint consisting of the symbolic expression of the input variable (as pc), that is, only the input value satisfying the constraint formula can reach the program position corresponding to the constraint, which is a Boolean expression;
  • (3) program pointer which points to the next program statement to be executed.

《基于覆盖准则的软件测试用例自动化生成方法的研究与实现》苏亭博士论文