符号执行

维基百科,自由的百科全书
跳到导航 跳到搜索

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

这一思想最初由IBM托马斯·J·华森研究中心的詹姆斯·C.金(James C. King) 于1976年6月在论文Symbolic Execution and Program Testing中提出[3],文中“解析程序的路径后,用符号模拟通过路径并获得输出”的方法如今被称为“经典符号执行”。由于20世纪80年代的研究追求分析的完备性,而大型程序的路径复杂,不可能完全遍历,符号执行这一研究领域遇冷。21世纪后,该领域研究有了新的进展:2006年,克里斯蒂安·卡达尔(Cristian Cadar)在论文中设计了一种“先进行符号执行,后根据符号执行结果生成测试用例”的“执行生成测试”技术[4],并随后将其发展为应用在GNU/Linux内核错误检查中的KLEE[5];2007年,库希克·森(Koushik Sen)在当年的软件工程自动化(Automated Software Engineering)会议提出将符号执行和实际执行结合的“混合执行(Concolic testing)”方法[6];2009年,维塔利·奇波诺夫(Vitaly Chipounov)提出“选择性符号执行”方法,通过选择“对程序设计者有意义”的执行分支进行符号执行测试来提高对大型程序应用符号执行测试的可行性。

符号模拟技术symbolic simulation)则把类似的思想用于电路分析[7]符号计算Symbolic computation)则用于数学表达式分析[8]

符号执行引擎[编辑]

符号执行引擎是符号执行技术的实现产物,可以用于对程序进行符号执行。一个基本的符号执行引擎由下列部分组成:

  1. 状态信息存储器:存储下列符号执行所需状态信息。
    1. :指向需要处理的下一条程序语句,其可以是赋值语句、条件分支语句或者是跳转语句;
    2. :指代路径约束信息,表示为执行到程序特定语句需要经过的条件分支,以及各分支处关于符号值的表达式;
    3. :表示与程序变量相关的符号值集.
  2. 语句执行器:执行每一条语句来获取该程序的控制流程。
  3. 约束解算器(英語:constraint solver):用于在一条路径的符号执行结束后解算路径约束与符号执行结果,为开发者提供一个可供实际执行(英語:concret executino)的值

实例[编辑]

请看下列代码:

int f() {
  y = read();
  z = y * 2;
  if(z == 12){
    fail();
  }else{
    printf("OK");
  }
}

实际执行时,该方法读入一个值存储于变量y,当y的值为6时,该方法调用fail(),反之打印OK

在符号执行时,程序读入一个符号值[註 1]λ,并将 λ * 2 赋值给 z。当运行到 if 条件判断语句,由于无法判断 λ * 2 == 12是否为真,符号执行引擎将执行“为真”与“为假”两种分支。执行时,引擎将判断语句处的程序环境与路径约束复制一份并应用于两条分支。本例中, fail() 分支的路径约束指的是判断条件 λ * 2 == 12 ,而print("OK")分支的路径约束为 λ * 2 != 12。路径结束时,约束解算器计算并得出一个对此路径有意义(即能够完成该分支的)输入变量实际值。该值可供帮助开发者复现错误时进行实际执行使用。本例中,fail()分支的一个约束结算结果是6

局限性[编辑]

路径爆炸[编辑]

大多数符号执行方法不适用于大型程序:随着程序规模的扩大,程序中有意义的路径成指数级扩大[註 2]。有些程序中存在无尽循环或递归调用,这更大大增加了有意义路径,提高了符号执行难度。[9] 为解决此问题,马健强(音译,Kin-Keung Ma)等人提出使用启发式路径搜索算法提高代码覆盖率[10];马特·斯塔特斯(Matt Staats)等人提出并行执行独立路径的方法来降低符号执行耗时[11]; 库兹涅佐夫等人则提出了合并相似分支的方法缓解路径爆炸问题[12]

待测程序输入变量的特点[编辑]

由于利用路径分析进行程序分析,对于输入变量范围大,但程序分支较少的程序,符号执行方法比对输入变量进行分析的方法(如动态程序分析)具有较强优势。但是对于输入变量变化范围小,程序分支多的程序,符号执行的效率较低。

内存地址存在别名[编辑]

由于符号执行根据内存地址分析变量及其变化,对于有内存地址别名[註 3]的程序,符号执行引擎将难以区分不同别名,因此执行结果可能有偏差。[13]

数组的处理[编辑]

由于数组是大量不同值(如内存地址)的集合,符号执行引擎需要选择将数组作为一个单独的完整变量处理还是将每一个数组元素作为单独的变量处理。由于引擎无法得知程序中每个数组的意义[註 4],动态确定每个数组的类型十分具有挑战性。[13]

存在运行环境交互[编辑]

当某一程序(如下代码所示)与超出符号执行引擎控制的运行环境有交互(如进行系统调用并获取系统调用返回信息等)时,符号执行将难以完成:

int main()
{
  FILE *fp = fopen("doc.txt");
  ...
  if (condition) {
    fputs("some data", fp);
  } else {
    fputs("some other data", fp);
  }
  ...
  data = fgets(..., fp);
}

该程序将打开一个文件,并根据条件将不同类型的数据写入该文件,然后回读已写入的数据。 从理论上讲,符号执行引擎将在第5行产生两个路径并在第11行返回与在condition变量中的值一致的数据。然而文件操作被实现为内核中的系统调用,符号执行工具无法控制其行为。 解决这一挑战的主要方法是:

在符号执行过程中直接执行系统调用:这种方法的优点是实现起来很简单;缺点是这种调用“并不是符号执行”,其返回内容是实际运行的真实值。

对运行环境建模: 引擎使用模型模拟系统调用,其优点是,能够得到正确的符号执行结果;缺点是需要实现和维护许多可能用到的系统调用模型。 KLEE[14]、Cloud9和Otter[15] 等工具通过实现文件系统操作、套接字、IPC等模型采用了这种方法。

创建整个运行环境的状态分支:基于虚拟机技术的符号执行工具通过创建整个VM状态的分支来解决环境问题。比如S2E[16]中,每个符号执行状态都是一个独立的虚拟机快照。这种方法的空间复杂度较高,对内存的消耗很大。

注释[编辑]

  1. ^ 事实上,大多数程序不接受符号输入。在实现符号执行时,经典符号执行会通过程序分析技术得出程序的控制流程图,然后根据流程图得出符号执行结果。
  2. ^ 当程序中每增加一个流程控制语句(如if),程序增加2倍的路径。
  3. ^ 当有多个变量指向同一个内存地址时,我们称这些变量的变量名为该内存地址的别名
  4. ^ 比如某程序中存在两个数组:数组a是某班级全体学生的名单,一经定义便不会发生改变;数组b是某个学生每次考试的成绩,每次考试该数组元素会+1。此种情况下,数组a应当被视作“一个完整变量”,而数组b的每个元素都需要被视作“一个单独变量”

参考文献[编辑]

  1. ^ Mikejo5000. Dynamic symbolic execution - Visual Studio. docs.microsoft.com. [2021-05-09] (美国英语). 
  2. ^ 叶志斌,严波. 符号执行研究综述. 计算机科学. 2018, 45 (6A): 28-36. 
  3. ^ James C. Kings. Symbolic Execution and Program Testing. Communications of the ACM. 1976, 19: 385-394. 
  4. ^ Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, Dawson Engler. EXE: A system for automatically generating inputs of death using symbolic execution. Proceedings of the ACM Conference on Computer and Communications Security. 2006. 
  5. ^ Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs (PDF). USENIX conference on Operating Systems Design and Implementation (OSDI). 2008: 209-224 [2021-05-09]. (原始内容存档 (PDF)于2022-02-03). 
  6. ^ Sen, Koushik. Concolic testing. Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering. ASE '07 (Atlanta, Georgia, USA: Association for Computing Machinery). 2007-11-05: 571–572. ISBN 978-1-59593-882-4. doi:10.1145/1321631.1321746. 
  7. ^ Bryant, Randal E. Symbolic simulation—techniques and applications. Proceedings of the 27th ACM/IEEE Design Automation Conference. DAC '90 (Orlando, Florida, USA: Association for Computing Machinery). 1991-01-03: 517–521. ISBN 978-0-89791-363-8. doi:10.1145/123186.128296. 
  8. ^ Symbolic Computation | Subgroup | Department of Mathematics | NC State University. math.sciences.ncsu.edu. [2021-05-09]. (原始内容存档于2022-01-05) (英语). 
  9. ^ Anand, Saswat; Patrice Godefroid; Nikolai Tillmann. Demand-Driven Compositional Symbolic Execution. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science 4963. 2008: 367–381. ISBN 978-3-540-78799-0. doi:10.1007/978-3-540-78800-3_28. 
  10. ^ Ma, Kin-Keung; Phang, Khoo Yit; Foster, Jeffrey S.; Hicks, Michael. Directed symbolic execution. Proceedings of the 18th international conference on Static analysis. SAS'11 (Venice, Italy: Springer-Verlag). 2011-09-14: 95–111 [2021-05-09]. ISBN 978-3-642-23701-0. doi:10.5555/2041552.2041563. (原始内容存档于2022-01-21). 
  11. ^ Matt Staats, Corina Pasareanu. Parallel Symbolic Execution for Structural Test Generation∗ (PDF). International Symposium on Software Testing and Analysis. 2010 [2021-05-09]. (原始内容存档 (PDF)于2021-05-10). 
  12. ^ Kuznetsov, Volodymyr; Kinder, Johannes; Bucur, Stefan; Candea, George. Efficient State Merging in Symbolic Execution. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM. 2012-01-01: 193–204. ISBN 978-1-4503-1205-9. doi:10.1145/2254064.2254088. 
  13. ^ 13.0 13.1 DeMillo, Rich; Offutt, Jeff. Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering. 1991-09-01, 17 (9): 900–910. doi:10.1109/32.92910. 
  14. ^ Cadar, Cristian; Dunbar, Daniel; Engler, Dawson. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI'08. 2008-01-01: 209–224 [2021-05-09]. (原始内容存档于2018-12-01). 
  15. ^ Turpie, Jonathan; Reisner, Elnatan; Foster, Jeffrey; Hicks, Michael. MultiOtter: Multiprocess Symbolic Execution (PDF). [2021-05-09]. (原始内容存档 (PDF)于2020-07-20). 
  16. ^ Chipounov, Vitaly; Kuznetsov, Volodymyr; Candea, George. The S2E Platform: Design, Implementation, and Applications. ACM Trans. Comput. Syst. 2012-02-01, 30 (1): 2:1–2:49. ISSN 0734-2071. doi:10.1145/2110356.2110358. 
引用错误:在<references>标签中name属性为“Schwartz”的参考文献没有在文中使用