Author: Edward J. Schwartz, Thanassis Avgerinos, David Brumley Carnegie Mellon University
Topic: Dynamic, Sym_exe, Taint
URL: https://ieeexplore.ieee.org/document/5504796?reload=true
Where: IEEE Symposium on Security and Privacy
Year: 2010
Introducetion: 介绍了动态污点分析及符号执行，总结了这些技术的框架及关键问题
本文只是学习并记录笔记，如有错误或不足请谅解指正，谢谢！
摘要
- 要解决的问题：动态污点分析与正向符号执行虽然被广泛使用，但没有正式定义的算法、没有总结这些技术的关键问题
- 已有的解决方案：无
- 本文提出的创新方案概述：精确地描述了动态污点分析和正向符号执行的算法，作为对通用语言运行时语义的扩展；强调了在安全环境中使用这些技术时的重要实现选择、常见陷阱和注意事项
- 效果：本文将动态污点分析形式化，展示如何使用我们的形式化来梳理和描述各种安全应用程序中常见的实现细节、注意事项和选择
概念与介绍
动态污点分析运行一个程序，观察哪些计算受到预定义污点源（如用户输入）的影响。
动态正向符号执行自动构建描述程序执行路径的逻辑公式，从而将执行推理问题减少到逻辑领域。
这两种分析可以结合使用，以构建仅表示依赖于受污染值的执行部分的公式。
两种技术的应用领域：
- 未知漏洞检查（Unknown Vulnerability Detection）：动态污点分析可以通过监测是否执行了用户输入来防止代码注入攻击
- 自动生成输入过滤器（Automatic Input Filter Generation）：符号执行可用于自动生成输入过滤器，检测并删除输入流中的漏洞
- 恶意软件分析（Malware Analysis）
- 生成测试用例（Test Case Generation）
一种中间语言-SIMPLE（略过）
作者设计了一种中间语言：SIMPIL 来演示动态污染分析和正向符号执行的关键方面，并介绍了该语言的语法、操作语义
SIMPIL示例：
动态污点分析
tip：污点分析三元组<sources, sinks, sanitizers>
- 目的：跟踪信息源（sources）和污点汇聚点（sinks）之间的信息流
- 相关基本概念：
- T：任何依赖于从污染源派生的数据来计算的程序值，都被认为是受污染的
- F：任何其他值都被认为是未受污染的
- 污点策略P：准确地确定程序执行时污点如何流动，哪些操作引入新污点，以及对受污点的值执行什么检查
- 可能出现的错误errors：
- 过度污染：动态污点分析可能将不是从污点源派生的值标记为污点
- 缺失污染：可能会遗漏从sources到sinks的信息流
Dynamic Taint Policies 污点策略
- 属性（对应以下三个规则）：
- 新的污点是怎么被引入到程序中的
- 污点是如何在指令执行时传播的
- 在执行期间，如何检查污点
- 污点引入规则（Taint introduction rules）：指定如何将污点引入系统
- 污点策略通常会区分输入源：
- 面向互联网的网络输入源 可能会引入污染
- 从可信配置文件读取的文件描述符 可能不会
- 污点策略通常会区分输入源：
- 污点传播规则（Taint propagation rules）：指定来自受污染或未受污染操作数的数据的污染状态 通常使用命题逻辑来表达传播策略，例如，t1 ∨ t2 表示如果 t1 被污染或 t2 被污染，则结果被污染
- 污点检查（Taint Checking） 污染状态值通常用于确定程序的运行时行为，例如，如果跳转目标地址被污染，则攻击检测器可能会暂停执行
一种典型的污点策略
受污染跳转策略（ tainted jump policy）
- 目标：保护潜在易受攻击的程序免受控制流劫持攻击
- 该策略的主要思想：从输入派生的值永远不会覆盖控制流值、返回地址、函数指针，确保免受此类攻击
- 过程：该策略将所有
input()的值标记为污染，然后引入程序中，传播污点
如在上图中（污点引入、污点传播、污点检查），检测到input()值最终可能污染y，程序停机 - 缺点：不适用所有应用场景（没考虑输入值是否使内存地址受到污染 即上表中Pmem）Q：为什么没这样做
Challenges and Opportunities 挑战与机遇
（1）Tainted Addresses ：
- 区分存储地址和存储单元值 并不总是合适的（如上面的典型策略）
- 如下面的程序，使用tainted jump policy并不会识别攻击：
- 改进策略：采用
tainted addresses policy（表5），若地址或单元值之一被污染，则结果也判定被污染 但这种改进策略也存在问题：过度污染。举例tcpdump（每次重要运行都会导致taint error）
（2）Time of Detection vs. Time of Attack ：
动态污染分析可能会太晚发出警报，不能保证在此之前程序的完整性没有被破坏。
- 例如：典型的返回地址覆盖利用漏洞（shellcode覆盖返回地址）中， tainted jump policy可以检测到此类漏洞，但是在第一次覆盖返回地址时不会引发error，只有稍后进行跳转时才会引发、报告漏洞。在这之间，有可能产生其他error。
- 问题：动态污点分析跟踪的信息太少，很难验证返回地址的位置是否被覆盖（canary？1998）答：
基于污点的攻击检测工具通常显示检测时间至攻击时间的间隔
（3）控制流污点分析（Control-flow taint）
纯动态污点分析不能计算控制依赖关系，因此不能完成基于控制流的污点分析（因为动态分析一次只在一条路径上执行）
部分解决方法：
- 补充静态分析，以此计算控制依赖关系
- 试探法（heuristics）：根据场景做出选择是否过度/缺失污染
4）消除污点（Sanitization）
动态污点分析只会增加污点的数量，不会主动删除污点。随着程序的执行，被污染的值会越来越多，降低了污染精度。
- 检查常量函数：
- 一些污点分析工具（TEMU、TaintCheck）检查常量函数，以去除不必要的污点
- 例子：X86中常使用
B = A XOR A这种语句来对寄存器清零。即B的值不依赖于A。但若A被污染，默认的污点分析策略会判断B也被污染
- 某些领域中，将加密散列函数的输出视为无污染值：加密函数的输入可能是用户指定的，但很难找到会导致加密散列函数输出任意值的输入。 Newsome等人通过量化用户对函数的输出可以施加多少控制，以此来自动识别这种情况。
- 可能存在依赖于程序的消除。例如，如果程序逻辑本身执行清理，则攻击检测器可能希望不污染值
符号执行 FORWARD SYMBOLIC EXECUTION
正向符号执行 —>构建表示程序执行的逻辑公式 —> 对程序不同输入进行推理
- 优势：可以一次推理多个输入，推断不同的分支
- 与常规执行的区别：用符号替代具体的值
详细理解符号执行，可以看：
Symbolic Execution for Software Testing: Three Decades Later
Challenges and Opportunities 挑战与机遇
问题：符号内存；处理系统调用；路径选择。
（1）Symbolic Memory Addresses 符号内存地址
- 原理：
- 具体执行时，使用具体值；符号执行时，使用表达式。
- 从符号表达式load时，表示从任何符合条件的地址处load
- store到符号地址时，表示能覆盖任何符合条件的地址
问题：
- 别名问题，两个内存操作引用同一地址时，就会出现潜在的地址别名
- 例如：
store( addr1 , v )z = load( addr2 )若：addr1 = addr2，则为别名，load到z中的值为v 若：addr1 ≠ addr2，则不会load v， 因此，符号内存地址也可能导致混叠问题 - 解决方法：
- 去除符号地址，不重名（Vine 可以根据名称选择性地将所有内存地址重写为标量） 例如上面的例子可以改写为：
mem_addr1 = vz = mem_addr2 - SMT求解器进行推理
mem1 = (mem0 with mem0[addr1] = v) ^ z =mem1[addr2]（暂时没看懂） 理解：addr1处的值 = v ，mem1 = mem0 - 别名分析（静态分析），推断两个引用是否指向同一个地址
- 去除符号地址，不重名（Vine 可以根据名称选择性地将所有内存地址重写为标量） 例如上面的例子可以改写为：
- 以往工作： 大多数工作没有专门解决符号地址的问题。 KLEE采用别名分析+SMT求解器；DART[35]、CUTE[56]只处理线性约束的公式，不能处理一般化的符号引用 访问线性地址时，可以解线性方程组，查看是否有别名（2010前没有相关工作）
- 例如：
- 路径选择
- 存在路径爆炸的问题，需要良好的路径选择策略：
- 设置循环迭代次数上限
- 深度优先搜索：如KLEE和EXE，并设置最大深度
- 混合测试：符号执行+实际执行；变形策略：generational search：单次符号执行生成多个具体的测试输入
- 随机路径策略：如KLEE。符号执行引擎通过从根节点到叶节点的随机遍历状态树来选择状态，浅层路径，可以防止执行卡住
- 启发式：探索路径，提高覆盖率
- 存在路径爆炸的问题，需要良好的路径选择策略：
- 符号跳转问题
- 指：GOTO跳转目标不是具体位置，而可能是一个表达式
- 解决方法：
- 符号执行+实际执行：观察下一个jump的目标。缺点：只探索已知的跳转目标
- SMT求解器：条件取反求解其他路径
- 静态分析：源码级间接跳跃分析通常采用指针分析的形式，二进制级跳转静态分析用于识别跳转目标表达式中哪些值会被引用
- 处理系统、库函数问题
- 系统调用会引入新的符号变量
- 解决方法：
- 创建函数的总结（summaries）：描述在具体调用相应代码时发生的副作用的模型，但需要手动生成
- 混合执行：先实际执行，得到系统调用的返回值，再在符号执行中使用该值。但结果不一定可靠，因为每次调用不一定返回相同的值（如时间相关函数）。
- 性能
- a)程序分支数量的运行时间指数，b)公式数量的指数，以及c)每个分支的公式大小的指数
- 解决方法：
- 硬件提升
- 赋予变量不同名称
- 识别公式冗余
- 识别独立的子公式：将多次使用过的公式保存缓存，如KLEE和EXE
- 使用weakest precondition计算公式。如一种算法，在使用该算法之前，必须将程序转换为动态单赋值形式
- 混合执行（Mixed）
- 根据程序的应用及类型，将符号输入限制为某些形式，可能会比较合适
- 例子：server的配置文件不需要符号化（一般不允许改写配置文件），而网络包数据需要符号化
应用
- 自动化测试用例生成（提高代码覆盖率）：符号执行
- 过滤器自动生成：符号执行
- 自动网络协议解析：动态污点分析
其他：恶意软件分析、污点分析框架（动静结合）等
其他作者的笔记：