一、总结：

主要内容：采用SimpIL语言统一描述DTA和SE过程，并描述其中的挑战。

挑战：DTA的主要挑战是地址也被污染，控制流被污染，去掉不必要的污染，检测被攻击的时机；

            SE的挑战是符号化内存地址（别名分析），执行路径选择，符号化的跳转地址（如jump tables），处理系统/库调用，优化性能，部分变量符号化mixed execution。

应用：DTA和SE主要用于未知漏洞检测；自动输入筛选器生成（入侵检测）；恶意软件分析；测试样例生成。

二、DTA 动态污点分析

1.动态污染策略Dynamic Taint Policies

（1）污点引入

get_input(.)，污点策略会区别不同输入源，如网络输入（都引入污点），文件输入（配置文件不属于污点）。

（2）污点传播

采用命题逻辑来表示。

（3）污点检查

目的是检查程序运行时的行为，如跳转地址是否污染，维护程序安全。

2.典型污点策略

Tainted jump policy：输入绝不能覆盖返回地址/函数指针。

缺点：没考虑内存地址是否污染，会错过某些攻击。

3.DTA挑战与机会

（1）Tainted Addresses—地址污染

例如：

x := getinput(.)

y := load(z+x)

goto y

分析：能够使攻击者跳转到未污染但用户可控区域，反映了tainted jump policy不足。

改进：tainted addresses policy，若值和地址其一被污染则表示内存单元被污染。Eg，TaintCheck[49]实现该策略。

真实漏洞示例：tcpdump。

问题：tainted address policy—过污染问题；tainted jump policy—欠污染问题。

（2）Control-flow taint—控制流污染

例如：y与x是控制流污染。

        x := get_input(.)                     

        if x=1 then goto 3 else goto 4

                y := 1

        z := 42                                     

分析：若不计算控制依赖，则不能确定基于控制流的污染，导致欠污染。

问题：DTA不能分析控制流污染，原因是分析控制依赖需分析多条路径，而DTA一次只执行一条路径。

解决：a.静态分析辅助DTA，静态分析可以计算控制依赖。

            b.启发式策略，根据具体场景决定是否污染。

（3）Sanitization消毒

问题：去除不必要的污染。

方法：a.识别常数函数，如TEMU[7], TaintCheck[49]。

        b.自动识别hash函数-[48]，因为hash函数返回值很难污染成指定值。

        c.下标未越界，则可以去污染。

（4）Time of Detection vs Time of Attack

问题：监测点/攻击点，检测到之前就已经被攻击，如tainted jump policy。

问题2：DTA记录信息过少，很难记录返回地址存放位置，以及是否被覆盖。

示例：DTA难检测整数溢出漏洞。

工具：BitBlaze[7]，离线分析执行路径上的指令序列。

三、SE符号执行

原理：采用逻辑公式表示程序执行，一次能描述多个输入的程序行为；get_input(.)返回符号值而非具体值。

符号执行挑战与机会

问题：符号内存；处理系统调用；路径选择。

（1）符号化内存地址

原理：具体执行时，使用具体值；符号执行时，使用表达式。从符号表达式load时，表示从任何符合条件的地址处load；store到符号地址时，表示能覆盖任何符合条件的地址。

问题：别名问题，两个内存操作指向同一地址。例如example 7，addr1与addr2都是符号值，可能相等也可能不等。

                store(addr1,v)

                z=load(addr2)

解决：a.去掉符号地址，不重名，如vine[7]。Example 7改写成mem_addr1=v，z=mem_addr2。

        b.用SMT解释所有重名关系，mem1 = (mem0 with mem0[addr1] = v) ^ z =mem1[addr2]。

        c.别名分析—静态分析，alias analysis，弄清两个引用是否指向同一地址。

相关工作：KLEE采用别名分析+SMT求解器；DART[35]、CUTE[56]只处理线性约束的公式，不能处理一般化的符号引用。

（2）路径选择

问题：路径爆炸问题，需路径选择策略，例如，有符号条件的loop不会终止，影响其他路径的探索。

示例：while(3^n+4^n == 5^n ) { n++; . . . }

解决：a.深度优先搜索DFS，缺点是可能陷入无终止的loop，需设定循环上限。

        b.concolic testing，concrete execution-CE先生成执行路径，SE跟着路径走，并生成新的具体输入。改进—generational search[36]，一次SE生成多个具体输入。

        c.随机选路，防止卡住，如KLEE。缺点是陷入浅层路径，但避免卡在有符号条件的loop。

        d.启发式，探索未覆盖路径。

（3）符号化跳转

问题：符号跳转symbolic jump，例如jump tables。

解决：a.concrete and symbolic (concolic) analysis [56]，发现跳转目标。一旦CE执行跳转目标，就用SE执行该路径；缺点是只探索了已知跳转目标，不能保证代码全覆盖。

        b.使用SMT solver，条件取反求解其他路径，缺点是效率低。

        c.使用静态分析，定位所有可能的跳转目标，源码级间接跳转分析一般采用指针分析，二进制级跳转静态分析用于识别跳转目标表达式中哪些值会被引用。Eg，函数指针表。

（4）处理系统/库调用

方法：a.函数总结，缺点是需要手动生成。

        b.在concolic testing时，使用上次具体执行的返回值，缺点是有些调用总是返回不同值，如gettimeofday()。

（5）性能

问题：执行时间，公式数量，公式长度增长。

示例：example 9如下，展开后就是x->s+s+s+s+s+s+s+s。

            x := get_input(.)     

            x := x + x                 

            x := x + x                 

            x := x + x                 

            if e then S1 else S2 

            if e2 then S3 else S4

            if e3 then S5 else S6

            assert(x<10) ;           

解决：a.用更快的硬件；

        b.每个变量赋予不同的name，x1=x0+x0 ^ x2=x1+x1 ^ x3=x2+x2。

        c.识别公式冗余，Bouncer[21]采用启发式识别公式中的共性；[36]采用离线优化公式。

        d.识别独立的子公式，计算过的公式保存于cache中，如EXE/KLEE[16,18]。

        e.使用weakest precondition [26]来计算公式[40]。

（6）混合执行mixed execution

方法：部分变量符号化，如server的配置文件不需要符号化（一般不允许改写配置文件），而网络包数据需要符号化。