Skip to content

Symbolic Execution 学习笔记

1. 符号执行概述

静态分析技术符号执行

  1. 经典符号执行技术
  2. 现代符号执行技术：具体执行和符号执行混合
    1. 混合执行测试（Concolic Testing）
      1. 与经典的符号执行不同，由于混合执行在整个执行过程中，需要维护程序的具体状态，因此其输入需要初始具体值。 混合执行测试从一个给定的输入或随机输入开始执行程序，沿着执行的条件语句在输入上收集符号约束，然后使用约束求解推断先前输入的变化，以便引导程序接下来的执行该走向哪一个执行路径。重复此过程，直到探索了所有执行路径，或者满足用户定义的覆盖标准、时间设置到期为止。
      2. 简化了约束求解的难度
    2. 执行生成测试（Execution-Generated Testing）
  3. 主要挑战和解决方案
    1. 路径爆炸
    2. 约束求解
    3. 内存建模
  4. 符号执行工具

image.png

2. 符号执行(1) - 自动生成覆盖率用例之利器

符号执行(1) - 自动生成覆盖率用例之利器

2.1 什么是符号执行

符号执行是借助程序的形式化语义来分析代码的一种方法，具体地说，不考虑循环的情况下，符号执行就是求解霍尔逻辑的最弱前置条件。

霍尔逻辑；可满足性模理论SMT工具；SAT求解器；klee

2.2 klee例子

klee —— 用于C++的符号执行工具

3. 符号执行(2) - 用例搜索时间的控制与优化

符号执行(2) - 用例搜索时间的控制与优化

3.1 指定超时时间

3.2 搜索优化初步

  1. 尝试不同的SMT求解器
  2. 尝试不同的搜索策略

image.png

  1. 交织组合新策略

4. 符号执行(4) - 幕后英雄SMT

符号执行(4) - 幕后英雄SMT

klee生成测试case的主要步骤是通过第二节介绍的搜索逻辑生成SMT表达式，然后通过stp求解器求解SMT表达式来获取可取的值做为测试用例的过程。

5. [important] 符号执行技术笔记

符号执行技术笔记

5.1 通俗地解释符号执行

  • 符号执行技术是一种 白盒的静态分析技术 。即分析程序可能的输入需要能够获取到 目标源代码 的支持。同时，它是静态的，因为并没有实际的执行程序本身，而是 分析程序的执行路径 。
  • 可以规约成约束规划的求解问题（更详细的介绍看这里：Constraint_programming）。比较著名的工具比如SMT（Satisfiability Modulo Theory，可满足性模理论）和SAT。
  • 实际的程序中，可能包含了与外设交互的系统函数，而这些系统函数的输入输出并不会直接赋值到符号中，从而阻断了此类问题的求解。
    • 为了解决这个问题，最经典的项目就是基于LLVM的KLEE（klee)它把一系列的与外设有关的系统函数给重新写了一下，使得符号数值的传递能够继续下去。从比较简化的角度来说，就是把上面的fputs函数修改成，字符串赋值到某个变量中，比如可以是上面的fop里面。再把fgets函数修改成从某个变量获取内容，比如可以是把fop的地址给output。这样，就能够把符号数值的传递给续上。当然，这里举的例子是比较简单的例子，实际在重写函数的时候，会要处理更复杂的情况。在KLEE中，它重新对40个系统调用进行了建模，比如open, read, write, stat, lseek, ftruncate, ioctl。感兴趣的读者可以进一步阅读他们发表在OSDI2008年的论文（KLEE-OSDI08)他们的文章深入浅出，非常适合学习。

5.2 从公式原理上理解符号执行（静态符号执行）

为了形式化地完成这个任务，符号执行会在全局维护两个变量。其一是符号状态 σ ，它表示的是一个从变量到符号表达式的映射。其二是符号化路径约束PC（或者叫路径条件），这是一个无量词的一阶公式，用来表示路径条件。在符号执行的开始，符号状态 σ 会先初始化为一个空的映射，而符号化路径约束PC初始化为true。σ 和PC在符号执行的过程中会不断更新。在符号执行结束时，PC就会用约束求解器进行求解，以生成实际的输入值。这个实际的输入值如果用程序执行，就会走符号执行过程中探索的那条路径，即此时PC的公式所表示的路径。

  • 读语句：var = sys_input()
  • 赋值语句：v = e
  • 条件分支语句：if(e) S1 else S2
  • exit 语句或错误（程序崩溃、违反断言等）
  • 循环和递归

问题：

  • 循环中的无限多路径
    • 对搜索加入限制，要么是限制搜索时间的长短，要么是限制路径数量、循环迭代次数、探索深度等等
  • 符号路径约束包含不能由求解器高效求解的公式

5.3 动态符号执行 Concolic Execution

最早将实际执行(concrete execution)和符号执行(symbolic execution)结合起来的是2005年发表的DART[5]，全称为“Directed Automated Random Testing”(或称concolic testing)，以及2005年发表的CUTE[6]，即“A concolic unit testing engine for C”。

Concolic执行维护一个实际状态(concrete state)和一个符号化状态(symbolic state)：实际状态将所有变量映射到实际值，符号状态只映射那些有非实际值的变量。Concolic执行首先用一些给定的或者随机的输入来执行程序，收集执行过程中条件语句对输入的符号化约束，然后使用约束求解器去推理输入的变化，从而将下一次程序的执行导向另一条执行路径 简单地说来，就是在已有实际输入得到的路径上，对分支路径条件进行取反，就可以让执行走向另外一条路径。这个过程会不断地重复，加上系统化或启发式的路径选择算法，直到所有的路径都被探索，或者用户定义的覆盖目标达到，或者时间开销超过预计。

注意在这个搜索过程中，其实Concolic执行使用了深度优先的搜索策略。也就是说每次产生新的输入Concolic执行都将执行完整个程序，直到程序结束，然后才返回上一个没有测试的路径约束条件，取反约束条件，得到新的输入，进入新的路径。

Cristian Cadar在2006年发表EXE，以及2008年发表EXE的改进版本KLEE，对上述Concolic执行的方法做了进一步优化。其创新点主要是在实际状态和符号状态之间进行区分，称之为执行生成的测试（Execution-Generated Testing），简称EGT。 这个方法在每次运算前动态检查值是不是都是实际的，如果都是实际的值，那么运算就原样执行，否则，如果至少有一个值是符号化的，运算就会通过更新当前路径的条件符号化地进行。例如，对于我们的例子程序，第17行把y=sym_input()改变成y=10，那么第6行就会用实际参数10去调用函数twice，并实际执行。然后第7行变成if(20==x)，符号执行若走then路径，则加入约束x=20；对条件进行取反就可以走else路径，约束是x≠20。在then路径上，第8行变成if(x>20)，那么该if的then路径就不能走了，因为此时有约束x=20。 简言之，EGT本质上还是将实际执行与符号执行相结合，通过路径取反探索所有可能路径。

正是因为concolic执行的出现，让传统静态符号执行遇到的很多问题能够得到解决—— 那些符号执行不好处理的部分、求解器无法求解的部分，用实际值替换就好了。 使用实际值，可以让因外部代码交互和约束求解超时造成的不精确大大降低，但付出的代价就是，会有丢失路径的缺陷，牺牲了路径探索的完全性。

然而总的来说，Concolic执行的方法是非常实用的，有效解决了遇到不支持的运算以及应用与外界交互的问题。比如调用库函数和系统调用的情况下，因为库和系统调用无法插桩，所以这些函数相关的返回值会被实际化，以此获得简化的程序约束。

5.4 面临挑战 & 解决方案

  1. 路径爆炸
    1. 使用启发式函数对路径进行搜索，目的是先探索最值得探索的路径；
      1. 启发式搜索是一种路径搜索策略，比深度优先或者宽度优先要更先进一些。大多数启发式的主要目标在于获得较高的语句和分支的覆盖率，不过也有可能用于其他优化目的。最简单的启发式大概是随机探索的启发式，即在两边都可行的符号化分支随机选择走哪一边。
      2. 还有一个方法是，使用静态控制流图（CFG）来指导路径选择，尽量选择与未覆盖指令最接近的路径。另一个方法是符号执行与进化搜索相结合，其fitness function用来指导输入空间的搜索，其关键就在于fitness function的定义，例如利用从动态或静态分析中得到的实际状态(concrete state)信息或者符号信息来提升fitness function。
    2. 使用一些可靠的程序分析技术减少路径探索的复杂性。
      1. 用程序分析和软件验证的思路去减少路径探索的复杂性，也是一种缓解路径爆炸问题的方式。一个简单的方法是，通过静态融合减少需要探索的路径，具体说来就是使用select表达式直接传递给约束求解器，但实际上是将路径选择的复杂性传递给了求解器，对求解器提出了更高的要求。
      2. 还有一种思路是重用，即通过缓存等方式存储函数摘要，可以将底层函数的计算结果重用到高级函数中，不需要重复计算，减小分析的复杂性。
      3. 还有一种方法是剪枝冗余路径，RWset技术的关键思路就是，如果程序路径与此前探索过的路径在同样符号约束的情况下到达相同的程序点，那么这条路径就会从该点继续执行，所以可以被丢弃。
  2. 约束求解
    1. 不相关约束消除 Irrelevant Constraint Elimination
      1. 在符号执行的约束生成过程中，尤其是在concolic执行过程中，通常会通过条件取反的方式增加约束，一个已知路径约束的分支谓词会取反，然后由此产生的约束集会检查可满足性以识别另一条路径是否可行。一个很重要的现象是，一个程序分支通常只依赖一小部分程序变量，所以我们可以尝试从当前路径条件中移除与决定当前分支结果不相关的约束。
    2. 增量求解 Incremental Solving
      1. 本质上也是利用重用的思想。符号执行中生成的约束集有一个重要特性，就是表示为程序源代码中的静态分支的固定集合。所以，很多路径有相似的约束集，可以有相似的解决方案。通过重用以前相似请求的结果，可以利用这种特性来提升约束求解的速度，这种方法在CUTE和KLEE中都有实现。举个例子来说明，在KLEE中，所有的请求结果都保存在缓存中，该缓存将约束集映射到实际变量赋值。
  3. 内存建模
    1. 程序语句转换为符号约束的精度对符号执行能实现的覆盖率以及约束求解的可伸缩性有很大影响。
      1. 使用数学整数(actual mathematical integers)去近似去代替固定宽度的整数变量，这样的内存模型可能会更有效率，但另一方面，根据诸如算术溢出之类的极端情况，可能导致代码分析不精确-这可能会导致符号执行遗漏路径或探索不可行的路径。
      2. 另外一个问题是指针。在访问内存的时候，内存地址（指针）用来引用一个内存单元，当这个地址的引用来自于用户输入时，内存地址就成为了一个表达式。当符号化执行时，我们必须决定什么时候将这个内存的引用进行实际化。一个可靠的策略是，考虑为从任何可能满足赋值的加载，但这个可能值的空间很大，如果实际化不够精确，会造成代码分析的不精确。
      3. 还有一个是别名问题。即地址别名导致两个内存运算引用同一个地址，比较好的方法是进行别名分析，事先推理两个引用是否指向相同的地址，但这个步骤要静态分析完成。KLEE使用了别名分析和让SMT考虑别名问题的混合方法。而DART和CUTE压根没解决这个问题，只处理线性约束的公式，不能处理一般的符号化引用。
      4. 符号化跳转也是一个问题。主要是switch这样的语句，常用跳转表实现，跳转的目标是一个表达式而不是实际值。
  4. 处理并发

5.5 发展脉络（至2017）

本节仍然摘录自r1ce的文章，主要是以时间的顺序梳理符号执行技术的发展脉络，同时对值得关注的项目和论文做一个小小总结和推荐。

符号执行最初提出是在70年代中期，主要描述的是静态符合执行的原理，到了2005年左右突然开始重新流行，是因为引入了一些新的技术让符号执行更加实用。Concolic执行的提出让符号执行真正成为可实用的程序分析技术，并且大量用于软件测试、逆向工程等领域。在2005年作用涌现出很多工作，如DART[5]、CUTE[6]、EGT/EXE[7]、CREST[8]等等，但真正值得关注和细读的，应该是2008年Cristian Cadar开发的KLEE[3]。KLEE可以说是源代码符号执行的经典作品，又是开源的，后来的许多优秀的符号执行工具都是建立在KLEE的基础上，因此我认为研究符号执行，KLEE的文章是必读的。

基于二进制的符号执行工具则是2009年EPFL的George Candea团队开发的S2E[9]最为著名，其开创了选择符号执行这种方式。2012年CMU的David Brumley团队提出的Mayhem[10]则采用了混合offline和online的执行方式。2008年UC Berkeldy的Dawn Song团队提出的BitBlaze[11]二进制分析平台中的Rudder模块使用了online的执行方式，也值得一看。总之，基于二进制的符号执行工作了解这三个就足够了。其中，S2E有开源的一个版本，非常值得仔细研究。最近比较火的angr[12]，是一个基于Python实现的二进制分析平台，完全开源且还在不断更新，其中也实现了多种不同的符号执行策略。

在优化技术上，近几年的两个工作比较值得一看其一是2014年David Brumley团队提出的路径融合方法，叫做Veritesting[13]，是比较重要的工作之一，angr中也实现了这种符号执行方式。另一个是2015年Stanford的Dawson Engler（这可是Cristian Cadar的老师）团队提出的Under-Constrained Symbolic Execution[14]。

另外，近年流行的符号执行与fuzzing技术相结合以提升挖掘漏洞效率，其实早在DART和2012年微软的SAGE[15]工作中就已经有用到这种思想，但这两年真正火起来是2016年UCSB的Shellphish团队发表的Driller[16]论文，称作符号辅助的fuzzing（symbolic-assisted fuzzing），也非常值得一看。

5.6 学习更多

摘自r1ce的文章：

对于符号执行入门，有两篇文章可以参考。其一是2010年David Brumley团队在S&P会议上发表的《All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)》[1]。这篇文章同时介绍了动态污点分析和前向符号执行的基本概念，作者构造了一种简化的中间语言，用来形式化地描述这两种程序分析技术的根本原理。其二是2011年Cristian Cadar发表在ACM通讯上的一篇短文《Symbolic execution for software testing: three decades later》[2]，以较为通俗的语言和简单的例子阐述了符号执行的基本原理，并介绍了符号执行技术的发展历程和面临挑战。

其实这两篇文章的作者都是二进制分析领域大名鼎鼎的人物，卡内基梅隆的David Brumley是AEG的提出者，其带领团队是DARPA CGC比赛的第一名；英国帝国理工的Cristian Cadar则是符号执行引擎KLEE[3]的作者——KLEE在符号执行领域的地位不言而喻。这两篇文章各有千秋：前者更加学术化一些，用中间语言进行的形式化描述有些晦涩难懂，但对于进一步研究符号执行引擎的源码很有帮助；后者则更通俗一些，有助于初学者的理解，且对于符号执行的发展脉络有更多的介绍。

5.7 Reference

r1ce：https://zhuanlan.zhihu.com/p/26927127

符号执行——从入门到上高速：https://www.anquanke.com/post/id/157928

http://pwn4.fun/2017/03/20/符号执行基础

[2]* Symbolic execution for software testing: three decades later：https://people.eecs.berkeley.edu/~ksen/papers/cacm13.pdf

[1] Schwartz E J, Avgerinos T, Brumley D. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) [C]// Security & Privacy. DBLP, 2010:317-331.

[2] Cadar C, Sen K. Symbolic execution for software testing: three decades later[M]. ACM, 2013.

[3] C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI’08), volume 8, pages 209–224, 2008.

[4] R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234–245, 1975.

[5] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI’05, June 2005.

[6] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE’05, Sep 2005.

[7] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 322–335, 2006.

[8] J. Burnim and K.Sen,“Heuristics for scalable dynamic test generation,” in Proc. 23rd IEEE/ACM Int. Conf. Autom. Software Engin., 2008, pp. 443–446.

[9] V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea. Selective Symbolic Execution. In Proceedings of the 5th Workshop on Hot Topics in System Dependability, 2009.

[10] S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley. Unleashing Mayhem on Binary Code. In Proceedings of the IEEE Symposium on Security and Privacy, pages 380–394, 2012.

[11] Song D, Brumley D, Yin H, et al. BitBlaze: A New Approach to Computer Security via Binary Analysis[C]// Information Systems Security, International Conference, Iciss 2008, Hyderabad, India, December 16-20, 2008. Proceedings. DBLP, 2008:1-25.

[12] Yan S, Wang R, Salls C, et al. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis[C]// Security and Privacy. IEEE, 2016:138-157.

[13] T. Avgerinos, A. Rebert, S. K. Cha, and D. Brumley. Enhancing Symbolic Execution with Veritesting. pages 1083–1094, 2014.

[14] D. a. Ramos and D. Engler. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Security Symposium, pages 49–64, 2015.

[15] P. Godefroid, M. Y. Levin, and D. Molnar. SAGE: Whitebox Fuzzing for Security Testing. ACM Queue, 10(1):20, 2012.

[16] N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proceedings of the Network and Distributed System Security Symposium, 2016.

6. 符号执行入门（author: r1ce）

符号执行入门（author: r1ce） 同 section 5

对于符号执行入门，有两篇文章可以参考。其一是2010年David Brumley团队在S&P会议上发表的《All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)》[1]。这篇文章同时介绍了动态污点分析和前向符号执行的基本概念，作者构造了一种简化的中间语言，用来形式化地描述这两种程序分析技术的根本原理。其二是2011年Cristian Cadar发表在ACM通讯上的一篇短文《Symbolic execution for software testing: three decades later》[2]，以较为通俗的语言和简单的例子阐述了符号执行的基本原理，并介绍了符号执行技术的发展历程和面临挑战。

7. [important]符号执行技术总结

符号执行技术总结

  1. 推荐资料
  2. 符号执行工具

Java

  • JPF-Symbc - Symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers, lazy initialization, etc.
  • JDart - Dynamic symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers using JConstraints.
  • CATG - Concolic execution tool that uses ASM for instrumentation. Uses CVC4.
  • LimeTB - Concolic execution tool that uses Soot for instrumentation. Supports Yices and Boolector. Concolic execution can be distributed.
  • Acteve - Concolic execution tool that uses Soot for instrumentation. Originally for Android analysis. Supports Z3.
  • jCUTE - Concolic execution tool that uses Soot for instrumentation. Supports lp_solve.
  • JFuzz - Concolic execution tool built on Java PathFinder.
  • JBSE - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
  • Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).