1

定义

符号执行（英语：symbolic execution）是一种计算机科学领域的程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。这一技术在硬件、底层程序测试中有一定的应用，能够有效的发现程序中的漏洞。

基本原理

举例说明：

1
2
3
4
5
6
7
8
9
int f() {
  y = read();
  z = y * 2;
  if(z == 12){
    fail();
  }else{
    printf("OK");
  }
}

对于以上代码，如果实际执行，那么效果是：读入一个值到y，然后令z等于y的2倍。如果z等于6，调用fail(),反之打印ok。

对于符号执行来说，流程中不定的值会被赋为$\lambda$,一个符号值，这个值可以是任何值，在这个例子中，y会等于$\lambda$，z会等于2$\lambda$，当遇到分支时，会模拟执行所有分支，即当2$\lambda$等于12时调用fail(),当2$\lambda$不等于12时打印ok。在符号执行完所有的路径后，会计算出一个能完成这个路径的符号的变量实际值，该例中，调用fail()是$\lambda$==6的结果，打印ok是$\lambda$！=6时成立

上面这个过程中，每一个条件被叫做一个约束，每一个结果对应的所有约束被称为约束集，每一个结果经过的约束集被称为路径，路径可以由执行树表示。而符号执行的目的，就是让符号值遍历所有路径，找到所有对应的约束集。

为了完成以上工作，在整个流程中存在两个变量符号状态$\sigma$和路径条件$PC$，并根据读到的语句对约束进行添加（以下为例子）：

  • 若是输入语句，在$\sigma$中添加映射：$\sigma$={var$\rightarrow$$\lambda_0$},此时$\lambda_0$是var变量的符号值。
  • 若是赋值语句，则把符号值代入计算，在$\sigma$中添加映射：$\sigma$={var$\rightarrow$$\lambda_0$,$var_2$$\rightarrow$$\lambda_0$+7}
  • 当遇到条件语句if(e) a else b.PC会先更新为PC$\land$$\sigma$(e)表示then,然后创建PC$^`$初始化为PC$\neg$$\land\sigma$(e)表示另一条路径
  • 如果遇到exit，错误，前后约束矛盾，这一个路径会终止。