- 入坑 pwn 以来一直对 Fuzzing 感兴趣但一直苦于没有
说人话的合适的教程，但经过进一步了解后才发现 Fuzzing 所涉及到的领域很广、结合很深，只学 Fuzzing 而不顾其他是不现实的，所以开个系列做做 Program Analysis 相关技术的笔记 笔记实际上本来还涵盖了如程序分析、污点分析、模糊测试等等很多技术的内容，但暂时只写了符号执行，看看以后能不能填上这个巨坑（）
符号执行（Symbolic Execution）
定义
符号执行（Symbolic Execution）是一种程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。具体而言，符号执行分析程序时，会使用符号值而非具体值作为输入，然后探索尽可能多的程序路径获得约束，最后通过约束求解器求解约束获得可以触发目标代码的具体输入
emmm……定义非常抽象，我们一个词一个词解释
具体值、符号值
具体值就是我们日常运行程序时所输入的各种具体的内容，可以是某个数字、字符串，也可以是某种文件，总之是具体的内容
相对的，符号值就是抽象的内容，可以理解成方程式里的 XYZ 这样的变量
所以符号执行所“执行”的是一个符号、一个变量，或者说是一个布尔方程，每个方程的 True 和 False 构成了一个个分支
程序路径
程序的执行流程表可以征成树，也就是执行树，程序的分支点就是树的内点，树的根与叶的每条通路也就是程序路径了
由于每个分支点都有 True 和 False ，所以我们用一个布尔序列来表示一条执行路径
约束
前面我们将每个分支点抽象成一个命题，所以这个命题的两种可能性就形成了两个关系式，也就是约束
举个简单例子，有分支条件 x > 5 ，那么这个命题的真假就形成了 x > 5、x <= 5 两个互斥的约束 接下来我们选择的路径必然会获得其中一个约束，到达树某顶点的所有条件的合取就是总的约束了
约束求解器
一种求解约束的程序，其求解的是可满足性问题，也就是一连串的命题
根据命题的不同可以大致分成两种求解器：针对布尔可满足性问题 SAT 的求解器和针对可满足性模理论问题 SMT 的求解器，求解约束用的求解器一般是 SMT 求解器
著名的 Z3 求解器就是一个 SMT 求解器，在 angr 内部就内置了一个定制的 Z3 求解器
所以现在重新翻译一下定义就是：探索程序的各种可能的执行路径，并将到达各路径的条件作为方程式来求解判定能否触发目标 这里的目标可以是我们期望获得的密文，也可以是我们所期望触发的漏洞，这些都可以用一组约束来表示并与路径约束合取进行求解
基本原理
符号执行分为过程内分析与过程间分析
过程内分析
过程内分析是指只对单个过程的代码进行分析
首先，对待分析的单个过程代码对象构建控制流图（Control Flow Graph，CFG）。控制流图是编译器内部用有向图表示一个程序过程的一种抽象数据结构，图中的节点表示一个程序基本块，基本块是没有任何跳转的顺序语句代码块，控制流图中的边表示代码中的跳转，它是有向边，起点和终点都是基本块。在CFG上从入口节点开始模拟执行，在遇到分支节点时，使用约束求解器判定哪条分支可行，并根据预先设计的路径调度策略实现对该过程所有路径的遍历分析，最后输出每条可执行路径的分析结果 如果要进行源代码的安全性检测，则需要在过程内分析时，根据具体的安全知识库来添加安全约束。例如，如果要添加缓冲区溢出的安全约束，则在执行时遇到对内存进行操作的语句时，就要对该语句所操作的内存对象的边界添加安全约束。以上面的方式来进行安全约束的添加，并且每次在添加之后就使用约束求解器对所有的安全约束进行求解，以判定当前是否可能潜在一个安全问题
过程间分析
过程间分析则是基于过程内分析的结果对整个程序进行上下文敏感的分析
首先，为整个程序代码构建函数调用图（Call Graph，CG），在函数调用图中，节点表示函数，边表示函数间的调用关系。根据预设的全局分析调度策略，对 CG 中的每个节点（对应一个函数）进行过程内分析，最终给出CG每种可行的调用序列的分析结果
动态符号执行
之前我们所说的其实都是静态分析方法，静态分析虽然很详尽，但相对而言其开销与误报率更大 目前在静态符号执行技术的基础上发展出了动态符号执行，也叫 Concolic 测试（Concrete and Symbolic，Concolic Testing）。动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍
动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的开销大很多；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。但是动态符号执行的结果是对程序的所有路径的一个下逼近，即其最后产生路径的集合应该比所有路径集合小，但这种情况在软件测试中是允许的
局限性与解决方案
路径爆炸（Path Explosion）
在分析各种各样的循环和分支结构的相互嵌套耦合的时候我们常常面临路径过多导致分析效率极低的情况，称为路径爆炸 路径爆炸问题至今仍是无法彻底避免的，目前的解决方案主要有两种：
- 启发式搜索：利用上下文信息来优化路径选择
- Soundness 程序分析：通过剪枝、重用、合并等方法来简化分析过程
约束求解（Constraint Solving）
符号执行的最终结果依赖于约束求解，求解器的效率和能力直接影响了符号执行的效率和能力。所以对于求解器的优化是目前瓶颈之一
内存建模（Memory Modeling）
符号执行实现时需要对被分析代码的结构语义进行建模，然后再对被分析代码的操作语义进行建模，最后构建一个虚拟机模型。由于符号执行是路径敏感的分析方法，因此一般为每条路径都会创建一个专属的虚拟机模型，以保证路径之间的相互独立性。该模型的准确程度将直接影响静态分析结果的精度。由于编程语言中使用的复杂数据结构和复杂操作语句具有较高的灵活性，使得它们的建模变得十分困难 有一种惰性初始化的方法，其思想是为每个数据结构（特别是复杂数据结构）建模时，在声明或者定义时只为其构建类型信息，直到被使用的时候，才根据使用的需要来初始化该变量的对象信息。还有一些其他复杂对象建模方法的解决方案
全局分析
在程序全局分析（过程间分析）过程中，当对一个规模较大、包含很多的过程间调用的程序进行上下文敏感的分析时，每当一个过程调用了另一个过程时都进入子过程进行分析，虽然会很精确，但这种方式可能会造成大量的时间空间开销，而使分析过程异常终止或在用户可接受的时间内无法完成 一种比较好的全局分析方法叫做函数摘要。函数摘要的方法是在过程内分析的基础上对已分析过的函数进行一个摘要记录的操作。在以后的分析中遇到调用其他函数时，如果存在被调用函数的摘要，则直接调用该函数的摘要并对该摘要行为进行解释；如果不存在被调用函数的摘要信息，则进入被调用函数进行分析，并在分析之后进行摘要保存。通过函数摘要我们可以很好地提高全局分析的效率，对于比较完备的第三方库也可以通过建模来大大提高分析效率。当然，如果选择程序摘要，对程序建模的便捷度和精准度的把控非常关键
Comments NOTHING