本篇博客是对发表在S&P 10上的论文All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution的系统介绍。
1. 基本介绍
动态污点分析和前向符号执行是动态分析技术中最广为使用的两类，前者运行程序并观测被预定义的污染源影响的计算，后者为程序执行路径建立逻辑公式从而将对执行的推断转换为对逻辑的推理。
虽然已有大量工作使用这类技术，但至今仍缺少对这些技术的确切算法的定义、对实现权衡和缺陷的介绍。因此，本篇文章通过定义语言的形式化运行语义来准确描述运行时分析是如何开展的，并揭示更具体的实现细节和选择。
2. 定义通用语言
对动态污点分析或前向符号执行的准确定义需要依赖特定语言，作者在本文中提出SimpIL作为示例，其格式类似中间表示。程序由一系列标记号码的语句组成，可能的语句包含赋值、断言、无条件跳转和条件跳转，表达式是无副作用的(不会对程序状态产生影响)。
考虑到动态程序分析定义在实际程序执行之上，因此我们需要考虑语言的操作语义。操作语义明确指定如何运行由特定语言编写的程序。SimpIL的完整操作语义如下所示。每条语句规则采取形式：
规则从下至上，从左至右阅读。给定一条语句，我们通过模式匹配寻找可用规则，并运行规则上方给出的计算，如果成功则将状态转移至结束状态。如果没有匹配的规则或者计算失败，程序异常退出。
具体来说，执行的上下文由5个参数描述：程序语句集合$\Sigma$，当前内存状态$\mu$，变量的当前值$\Delta$，程序计数器$pc$和当前语句$\iota$。前三者表示为映射，例如$\Delta[x]$表示变量$x$的当前值而更新上下文变量$x$的值为$v$表示为$x \leftarrow v$。表达式使用$\mu, \Delta \vdash e \Downarrow v$表示在给定$\mu$和$\Delta$的当前状态下表达式$e$衡量为值$v$。
3. 动态污点分析
动态污点分析的意图是跟踪从污染源到汇聚点的信息流。任何依赖于从污染源衍生的数据计算得到的程序值被认为是受污染的(T)，否则是未受污染的(F)。污点策略P(taint policy)决定在程序执行过程中污点是如何传播的，哪些操作引入新的污点以及在受污染值上采取哪些检查。污点分析通常会出现两种错误，即overtainted和undertaining，前者指假阳性而后者指假阴性。
本文基于语言的操作语义表达动态污点分析，将污点策略添加到操作语义规则当中。为追踪每一程序值的污点状态，采用$\langle v, \tau \rangle$表示值，其中$\tau$表示值$v$对应的污点状态。此外，$\tau_{\Delta}$和$\tau_{\mu}$分别将变量和内存地址映射到对应污点状态。如下所示，污点分析策略P被添加到SimpIL中，其独立于原始语义。
更深入地分析来看，污点策略声明三种属性：
- 污点引入(Taint Introduction)：污点引入规则声明污点是如何被引入系统的，在
SimpIL中用户输入只有单一源头$get\_input$，而在实现时输入源可能多种多样，例如从库调用调用返回的值。 - 污点传播(Taint Propagation)：污点传播规则确定从受污染或未受污染的操作符衍生出的数据的受污染状态，一般采用命题逻辑来表述。
- 污点检查(Taint Checking)：污点状态值常被用来确定程序的运行时行为，例如攻击检测器在发现跳转目标地址受污染时会提前终止程序。在
SimpIL中，这种检查是通过向操作语义的Premise中添加策略实现的。
污点分析最经典的应用场景就是攻击检测，下面展示的就是添加到SimpIL操作语义规则中的污点跳转策略(tainted jump policy)。该策略确保由输入生成的值永远不会覆写控制流值，诸如返回地址或函数指针，从而规避控制流劫持攻击。
该策略将所有由$get\_input$返回的值标记为引入的污点值，污点在程序中以相对直观的形式传播，例如被赋值变量将被标记为受污染，倘若赋值操作右侧的值也是受污染的。
目前来说，动态污点分析主要面临如下问题：
- 受污染的地址(Tainted Addresses)：内存赋值操作通常涉及地址和值两方面。倘若仅考虑值的受污染情况，攻击者仍能操作内存写入地址完成攻击。可将$P_{mem}$更新为$P_{mem}(t_a, t_v) \equiv t_a \vee t_v$来缓解这一问题，然而这同样会引入假阳性。
- 控制流污染(Control-flow taint)：控制流依赖同样会影响信息流动，具体来说，如果语句$s_1$控制语句$s_2$是否会执行，那么$s_2$就控制依赖于$s_1$。如果在污点分析时不考虑控制依赖，就会造成undertaint的问题。为此，可考虑添加静态分析来预先计算控制依赖。
- 漂洗(Sanitization)：由于上述策略不会移除污点，随着程序执行将会有越来越多值被污染，这通常导致污点精度的下降。一个显而易见的例子是常量函数$b=a \oplus a$，显然$b$的值为常量但污点分析可能将其错误地标记为受污染的。污点分析工具通常会针对这些情况进行特殊处理。
4. 前向符号执行
前向符号执行通过对程序执行构建逻辑公式来推断程序在不同输入上的行为，其最显著的优势是能够一次推断多种输入可能。
前向符号执行与常规执行最主要的区别在于$get\_input$返回符号值而非具体值。当新符号被引入时，其值不受任何约束并代表任何可能值。相应地，表达式只能被表示为符号表达式而非具体值，修改后的SimpIL如下所示，其中$\Pi$是路径谓词并表示程序某条路径上的约束。分支将符号变量约束到执行某条路径的取值区间内，断言要求符号变量的值必须满足断言表达式的要求。最后通过求解路径约束$\Pi$就能得到遍历某条路径的具体输入值。
前向符号执行从概念上十分直观，然而仔细思考便会发现存在很多问题，接下来对主要困难进行讨论。
4.1 符号化内存地址
符号化内存地址问题是指在内存读写操作中的地址是从用户输入生成的符号表达式而非具体值。从完备性角度看，当从内存读写数据时需要考虑任何能满足约束的赋值所产生的表达式值。符号化内存地址会进一步导致别名问题，例如两个内存操作指向相同的内存地址。为解决这一问题，常用的做法是交由后续的分析步骤来处理，例如将内存更新表达为约束传递给SMT求解器。又或者依赖于静态的别名分析先对内存别名进行识别。
4.2 路径选择
前向符号执行必须考虑在遇到分支时优先遍历哪条分支的问题。例如，循环很有可能导致符号执行无限递归下去从而无法有效探索状态空间，因此一般会为前向符号执行设置最大循环迭代次数。目前的路径选择策略包括深度优先搜索、随机路径选择、启发式规则、混合符号测试(Concolic Testing)等。
4.3 符号化跳转
在前向符号执行中，跳转目标同样可能是表达式而非具体位置，一个常见原因就是跳转表的使用。目前存在三种处理符号跳转的方法：
- 使用混合符号分析，首先运行程序来观测间接跳转的目标位置，再针对具体路径进行符号执行。
- 使用SMT求解器，当需要在路径约束$\Pi$的前提下跳转至目标位置$e$，可以要求SMT求解器生成一个能满足$\Pi \wedge e$的回答。
- 采用静态分析来定位可能的跳转目标，例如指针分析等。
4.4 处理系统和库调用
部分系统级调用除了引入新符号化变量外也会产生副作用，例如read会更新指向文件当前读取位置的内部指针，后续对read的调用理应不能返回相同输入。一种处理系统级调用的方法是总结各调用产生的副作用(side effects)，但其需要手动撰写。另一种方法是采取混合符号执行，将先前实际执行时系统调用返回的值用在符号执行中。
5. 总结
本篇论文形式化定义了动态污点分析和前向符号执行是如何在操作语义的基础上展开的，并介绍了将这两类技术运用到实际场景所面临的挑战、权衡和机遇。