0x00 Questions

这篇文章意在解决“嵌套”的条件结构（注意这里的嵌套并不是狭义上控制结构嵌套），这是一个比较难处理的问题，在找到一个能触发新分支 b 的输入 i ，接下来的策略肯定就是在这个输入 i 上，去构造新的输入 i' 来触发更多的新的分支，但是这里面有一 个问题，假设新分支 b 内有一个子分支条件是 s ,这个分支条件位置为 P (reachable by i ),那么分支 b 的子分支就可以抽象为 \{s\} \cap P ,构造出来的输入 i' ,极有可能 P 点并不是reachable，因为可能 P 点之前的某个分支条件满足性，在输入 i 和 i' 上并不相同:

这里通过一个代码片段，来特别地说明几种特殊的情况：

控制流依赖，L6依赖于L2，L3，L4。（这里的依赖对象是分支条件，下同）
数据流依赖，L6依赖于L2，L3。

如果我们想要进入L6的true分支，首先(1 L6 is reachable，（2 satisfies L6’s condition。

0x01 The ways

1.1 分支条件的控制流依赖

这个依赖可以看作是从CFG上剥离出来的东西，图上的点从基本块变成了分支条件，什么是分支条件？可以更具体一点，cmp/jmpz(nz) 等等的组合，为了把分支条件之间的关系，描述更加紧密，文中抽象了一个叫prior conditional statements 的概念，对一个指定的路径条件 s ,它的prior conditional statements是可能导致 s 变成unreachable的一组路径条件。

这个定义在实现过程中还是比较抽象，需要具体的研究一下它的性质，首先考虑它并不是一个等价关系（不满足对称性），那么它是一个偏序吗？自反性很显然，传递性也很显然，反对称性呢？考虑两个不相同的路径条件是否相互为prior conditional statement ,这个不要去想的太复杂，在这篇文章描述的依赖关系下，是不可能做到，因为执行流，两个statements，肯定有一个是先执行的。

抛开反对称性不说，重点关注它的传递性，这里prior conditional statement 关系我用
\preccurlyeq 表示。传递性可以描述为

\text{if}\ a \preccurlyeq b, b \preccurlyeq c ,\text{then}\ a \preccurlyeq c

为了找到指定路径条件 s 所有的prior conditional statements，可以使用这个性质，但是还需要定义一个immediate prior conditional statement,如果 r 是 s 的一个immediate prior conditional statement,则在 r 和 s 之前找不到第二个prior conditional statement,这个“之前”是指所有执行到 s 到路径，往后看 r 都是最后一个路径条件。可以简单的理解为 r 离 s 最近。这个定义对研究路径的同学来说，是非常熟悉的，就是dominator tree的定义，仿照它的定义，是可以给出计算prior conditional statements的算法的。

Prior(s) = IPrior(b) \cup IPrior(IPrior(b))\cdots

其中IPrior表示immediate prior conditional statement

通常来说dominator tree只定义在过程内，文中又进一步改进，引入了过程间的prior conditional statement 关系，这个也很好理解，如果一个路径条件 s 在过程内没有prior conditional statement,那就去找调用个过程的call的prior conditional statement，这里会产生一个疑惑不是描述路径条件之前的关系吗？怎么又突然来了一个call，按照定义描述的是“可能导致这个call 变成unreachable的路径条件”，其实是合理的。

我以为文中技术实现是完全建立在静态分析上，但是直到读到这里，trace和stack的出现，告诉我极有可能是在动态过程中做的，而且文中给的找immediate prior conditional statement的算法是可以在动态做的。

Intraprocedural immediate prior conditional statement：（ r of s ）

• r 和 s在同一个函数内

• s 不是 r 的 post-dominator (post-dominator ：如果 r 到exit -point的所有路径都经过 s )

Interprocedural immediate prior conditional statement（ r of s ）

• r 和 s 不在同一个函数内
• 当 s 执行的时候， f_r 的返回地址在当前的栈中。
• r_c 是 f_r 执行过的最后一个调用， r_c 不是 r 的post-dominators

文中还提到的路径分支包含terminator的情况，其实这种属于上面第一种情况了，因为第二个条件已经限定了。但是作者在这里还是特别的拿出来说了一下，我还是在这个放个小例子：

if(x==1){
  exit();
}

if(y==2){//target
  //...
}

1.2 分支条件的数据流依赖

用 b(s) 表示流到分支条件 s 上的input bytes集合， s 表示一个或者多个分支条件。当input在 s 处可达，为了进入 s 代表的分支，需要进一步修改input, 在修改之后， Prior(s) 里面路径条件选择不变的情况下， s 还是reachable，从直觉上来说，为了尽可能小的影响 Prior(s) 里面的路径条件，需要尽可能的避免修改 b(Prior(s)) 的input bytes,但是这样做有可能带来负反馈，例如F2中 b(Prior(s_{l6}))=\{x,y,z\} ,这将直接导致根本无法进入L6所代表的分支。

这种情况下只考虑了分支条件的控制流依赖，并没有考虑路径条件之前的数据流依赖，这里文中又定义了第二种关系effective prior conditional statements ,我们需要稍微去改变一下上面我们的直觉，先忽略考虑reachable，我们需要改变 s 里面涉及到的input bytes ，改变这些input bytes 意味着 Prior(s) 里面和它相关的路径条件的选择可能就会发生变化，我们需要尽可能保证他们的选择，所以应该去重点修改 b(s)\setminus b(EPrior(s)) ,很显然在这里 EPrior(s) \subset Prior(s) 。这个直觉要比第一次的直觉要好那么一点点，但是也有问题，例如F2中 b(s_{l6})=\{y\} , b(EPrior(s_{l2}))=\{x,y\} ,所以 b(s_{l6}) \setminus b(EPrior(s_{l6}))=\emptyset . 这个直觉在Matryoshka中是第一个求解约束的策略Prioritize reachability

1.3 求解约束

前面已经提到求解约束的一个策略，在这里需要综合考量reachable 和 satisfy constraints ，文中在这里提出了三种可选的策略，顺序执行：

1. Prioritize reachability
2. Prioritize satisfiability
3. Joint optimization for both reachability and satisfiability

1.3.1 Prioritize satisfiability

这个策略非常有意思，修改 input 之后可能导致 s 变成unreachable,但是强制使 EPrior(s) 里面的路径条件选择不变（运行时），这个过程叫forward, 当在某次修改input之后，满足了条件$s$,结果有两种：(1 如果 EPrior(s) 中的路径条件选择并没有发生变化，代表 forward 成功了 （2 如果 EPrior(s) 中的路径条件选择发生了变化，则需要修补发生改变的路径条件，进入backtrack过程。

bracktrace过程从 s 向后按顺序fuzz EPrior(s) 里面的每个路径条件 r ,这个过程中需要避免修改流入$s$ 或者在 r 后面的effective prior conditional statements的input bytes,bracktrace成功的标志是处理完所有*EPrior(s)*的路径条件。

还是用F2中的例子来说明问题：假设当前的输入为 x=1,y=1,z=1111 , L2,L3是L6的effective prior conditional statements，L2和L3下进入都是true分支，目标是进入L6的true分支，在修改 s 关联的input bytes过程中，强制使L2和L3也保持true分支,假设 y=2 ,满足了 s 但是L3选择是false，所以进入bracktrace过程，继续slove L3，这个时候需要避免动 y 的值，当 x=0 的时候，就找到一组满足L6的input bytes.但是这里如果在一个forward过程中选择了y=3,就直接导致后面的bracktrace失败了。

1.3.3 Joint optimization for both reachability and satisfiability

总结一下，Prioritize reachability旨在修改那些不会影响EPrior(s)的input bytes，保证 s 是reachable，Prioritize satisfiability使用forward-backtrace方法，尽可能的满足 s .但是它们都可能在尝试优化多个路径条件的时候失败。这里文中通过对Angora的梯度下降算法再改造：

• f_i(x)\leq 0,\forall i \in [1,n] 表示 EPrior(s) 中每一个路径条件的黑盒抽象函数，同样使用和Angora一样的转换表：
  

  

• g(x) = \sum_{i=0}^{n}R(f_i(x))\ ,R(x) \equiv 0 \vee x

  其中 R(x) 相当于一个max函数， \vee 二元运算符表示取最大的那个操作数，并用 f_0(x) 表示 s 的抽象运算。观察这里转换表比Angora多了一个 \epsilon ,用于区别路径条件类型的最小正数。当 g(x)=0 的时候，必然有 \forall i\in[1,n],f_i(x)=0 , 在这里把 g(x)=0 作为预期最优解。（我觉得应该是 g(x)\le 0 ,如何保证每个 f_i(x)=0 这个事实？）。需要注意的是它这里要比Angora做的更好，因为Angora在计算偏导数的时候，并不能保证 s 是reachable，这样得到的结果没有意义，Angora面对这个问题，只是简单提到了通过改变单位分向量的值。这里Matryoshka可以强制保证previous分支选择，来保证计算过程。

  同样这样也用F2中的例子来说明问题，让 [x,y]=[1,3] 为初始 input ：

  g([x,y]) = R(x-2+\epsilon) +R(x+y-3+\epsilon) + R(1-y+\epsilon)

  通过梯度下降，最终会得到一个solution 为 g([0,2])=0

1.4 隐式条件路径

直接用例子来说明问题：

L6计算显式的 EPrior(s_{l6})=\emptyset ,很显然L3应该是属于 EPrior(s_{l6}) 的，但是现有的方法是无法把它区分出来的，针对这种类似隐式的污点传递，通常的做法是如果路径条件被污染，则把该分支下的所有赋值操作都视为污点传递。这种方法文中提到，可能会导致over taint 和 taint explosion 。（但是我认为这样做理论上并没有问题，例如L4中n也被tainted,作者认为是useless，就算它是useless也不会影响其他的东西，考虑到因为这些污点导致更深的传递过程，也是合乎情理的，这属于一种indirect tainted,我猜测处理它的难点在于与之关联的input bytes不好做对应，这个过程需要手工的添加一些额外的taint rule）

作者并不想按照通常的手法来操作，而是通过相关的策略把隐式污点过程筛出来：假设当前的 input 对 s 是reachable的，但是经过mutate以后变成unreachable了。再额外运行两次，第一次记录original input过程中经过的路径条件，第二次记录mutated input过程中经历的路径，但是这个过程强制进入original input的路径选择，使其变成reachable,这两次得到的路径条件序列应该是相同的，按时间倒序检查它们的路径条件序列。

如果存在一个 r \notin EPrior(s) ,并且 r 前后两次路径选择并不一样，则有可能存在与 s 的隐式路径依赖，需要进一步做验证，再跑一次mutated input，并且强制针对下面的路径条件和original input做到统一：

• 所有在r之前的条件路径

• 所有显式的effective prior conditional statements

• 所有已知的隐式的effective prior conditional statements

如果结果s是unreachable则 r 确定是存在的隐式路径依赖，我举个小例子，帮助理解和回忆：

y=0;
z=input();
if(z){
	y=1;
  x=2;
}

if(y){
	useless=1;
}

if(x==2){ 
	if(a==19970131){//target conditional statement
    //...
  }
}

假设original input对L13是reachable，但是mutated input是unreachable.两次的路径序列：

• L4:true;L8:true;L12:true
• L4:false;L8:false;L12:false

逆序比较:

• L12不属于 EPrior(s) ，按照验证算法，这里是L13是unreachable的，所以L12属于隐式的effective prior conditional statement

• L8不属于 EPrior(s) ，按照验证算法，这里L13还是reachable的，所以L8不属于隐式的effective prior conditional statement

• L3不属于 EPrior(s) ，按照验证算法，这里是L13是reachable的，所以L3不属于隐式的effective prior conditional statement

奇怪得到的结果却是L3不属于隐式的effective prior conditional statement,原文中的逆序比较似乎不合理？这个演算结果我没有想到。

0x01 Self Conclusion

在看Angora我就有一个疑问，关于梯度下降算法，因为无法保证目标路径分支是reachable的，所以计算梯度得到的结果是毫无意义的，在这篇文章里面给了我想要的答案，作者似乎修补了这个很重要的问题，用force的方法，保证两次走过的路径条件一样。疑问又来了，这样做的理论依据在哪呢？