一 简介
angr是一个与平台无关的二进制分析框架
- 反汇编和中间件Disassembly and intermediate-representation lifting
- 程序插桩Program instrumentation
- 符号执行Symbolic execution
- 控制流分析Control-flow analysis
- 数据依赖分析Data-dependency analysis
- 值集合分析Value-set analysis (VSA)
- 反编译Decompilation
二 基础知识
(一) 符号执行
具体参考 链接
符号执行技术使用 符号值 代替 数字值 执行程序，得到的变量的值是由输入变量的 符号值和常量 组成的 表达式。
符号执行是一种重要的 形式化方法 和 静态分析技术，它使用数学和逻辑首先定义一些基本概念。
程序的路径（path）是程序的一个语句序列，这个 语句序列 包括程序的一些顺序的代码片段，代码片段之间的连接是由于分支语句 导致的控制转移。
一个路径是可行的（feasible），是指存在程序输入变量的至少一组值，如果以这组值作为输入，程序将沿着这条路径执行。否则，路径就是不 可行的（infeasible）。
路径条件（path condition,PC）是针对一个路径的，它是一 个关于程序输入变量的符号值的约束，一组输入值使得程序沿着这条路径执行当 且仅当这组输入值满足这条路径的路径条件。
另一种解释：符号执行(Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。
1. 符号执行原理
符号执行是指在不执行实际程序的前提下，把源程序翻译为一种中间语言，用符号值表示程序变量的值，然后基于中间语言模拟程序执行来进行相关分析的技术。
它可以分析代码的所有语义信息，也可以只分析部分语义信息（如只分析“内存是否释放”这一部分的语义信息）。
符号执行通常可表示为三元组的形式：<指令指针，路径函数，路径条件>。
- 指令指针指出了当前被分析的指令；
- 路径函数表示程序路径中不同位置处变量的值（可以是符号值，也可以是常量，或二者形成的函数），可用函数映射表示;
- 路径条件是路径在各个分支执行点（位置）的分支条件的合取逻辑表示，可用布尔公式表示。
符号执行分为过程内分析和过程间分析（又称全局分析）。
程序的全局分析是在过程内分析的基础上进行的，但过程内分析中包含了函数调用时就也引入了过程间分析，因此两者之间是相对独立又相互依赖的关系。
- 过程内分析是指只对单个过程的代码进行分析；
- 全局分析指对整个软件代码进行上下文敏感的分析。
- 所谓上下文敏感分析是指在当前函数入口点要考虑当前的函数间调用信息和环境信息等。
如果要进行源代码的安全性检测，则需要在过程内分析时，根据具体的规则知识库来添加安全约束。例如，如果要添加缓冲区溢出的安全约束，则在执行时遇到对内存进行操作的语句时，就要对该语句所操作的内存对象的边界添加安全约束。以上面的方式来进行安全约束的添加，并且每次在添加之后就使用约束求解器对所有的安全约束进行求解，以判定当前是否可能潜在一个安全问题。
在程序全局分析处理过程中，首先需要为整个程序代码构建函数调用图。在函数调用图中，节点表示函数，边表示函数间的调用关系。根据预设的全局分析调度策略，对CG中的每个节点（对应一个函数）进行过程内分析，最终给出函数调用图每种可行的调用序列的分析结果。
动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。
动态符号执行使用具体值作为输入，同时启动模拟执行器。模拟器可基于不同层次的，比如用户态级别，只支持printf, write, read等基本IO函数；也可是全系统级别的，可以支持应用程序和操作系统在模拟器上执行。
然后，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。
动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的花销大很多；
并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。
但是动态符号执行的结果是对程序的所有路径的一个“下逼近”，即其最后产生路径集合应该比所有路径集合小，但这种情况在软件测试中是允许的。
2. 符号执行实现概述
符号执行通常可表示为三元组的形式：<指令指针，路径函数，路径条件>。
- 初始化指令指针执行程序入口点
- 初始化的路径函数一般是恒等函数
- 初始化的路径条件为真
在符号执行中需要更新指令指针，路径函数，路径条件：
- 指令指针通常从指向当前指令转到指向其后续指令或指向jmp/call的目的地址处的指令
- 路径函数一般通过复合路径上每条指令的语义函数（如操作语义或指称语义）得到更新
- 路径函数的更新保证了可获取到路径中每个分支的分支条件，通过合取逻辑操作来合并路径中每条分支的分支条件
比如： 变量a,b执行如下指令语句
1 if(a<10)
2 assert(a<10);
3 else if(b<10)
4 assert(a<10 && b<10);
5 else assert (a>10 && b>10);
6 end则符号执行的表示如下：
value: (0,0) path：1-2-6 path_condition (a<10)
新的路径条件 !(a<10)，用求解器可得一个具体值 a=10
value: (10,0) path：1-3-4-6 path_condition !(a<10)&&(b<10)
新的路径条件 !(a<10)&&!(b<10)，用求解器可得一个具体值 a=10, b=10
value: (10,10) path：1-3-5-6 path_condition !(a<10)&&!(b<10)
在执行每条指令时，对于非分支指令，可通过函数的复合操作来更新路径函数。
对于分支指令，由于要执行一条新路径，所以需要创建新的进程，并将原路径条件与美国分支目标满足的分支条件执行合取逻辑操作，形成新的路径条件。
当某符号执行进程结束时，可调用约束求解器求解路径条件以获取可导致程序执行该路径的具体输入值的集合。
当所有符号执行的进程都结束了，则整个符号执行过程结束。
