深入了解符号执行

符号执行分类之间的不同

静态分析方法是从语法或语义的层面分析程序文本(源代码或二进制) 动态分析方法是通过运行待测程序以获取和分析程序运行过程中产生的动态信息,以判断其运行时语义性质 二进制分析多采用动态分析方法,源代码分析多采用静态分析方法。

动态分析只获取程序的实际可行路径和可达状态,但由于其大多时候并不能便历程序的所有可行路径,因而可能错过了某些可以引发程序错误的执行路径,进而导致漏报。但这也保证分析结果没有误报的根本原因。(即动态分析方法对程序的实际可达做下进似处理)

大部分的静态分析方法为了建立用于分析的模型需要对程序的动态语义做某种形式的抽象,其抽象结果会引入实际不可行路径和不可达状态,而静态分析方法难以在有限时间内判定抽象路径的可行性,这是导致误报的主要原因。(即静态分析方法在对被分析程序的实际可达状态做上近似处理) 也有一些静态方法同时做上近似和下近似,同时引入了漏报和误报

图1,不同近似方式引起漏报和误报

1

自动化白盒模糊测试

1)对静态符号执行进行扩展,混合具体执行提出轻量级动态符号执行方法:Concolic执行;
2)借助于逐渐实用化的SMT求解器技术对路径约束求解。
3)使用新的启发式算法探索程序的路径空间(程序执行树)。

由于静态与动态分析方法在执行中只能达到近似而导致漏报和误报,Concolic执行对两种分析方法进行了混合,在具体执行的同时对所执行到的代码施行符号执行,这样一来,具体执行的特性决定了每次的Concolic执行获取的路径都是可行路径,因此避免了误报。这是Concolic执行对于静态分析方法的优势。 另一方面,对于某种超出了求解器的求解能力范围的代码,Concolic能够进行简化反还一个简化后的符号表达式。这个过程被称为路径约束的部分具体化

void f(int,int y){
  if(x>y){
    x = x+y;
    y = x-y:
    x = x-y;
    if(x-y>0)
      assert(false);
  }else{
    if(x*x*x==y)
      assert(false);
  }
}

对应代码的符号执行树

2

例入上述代码中,传入参数x=2,y=33,x^3==y为非线性约束,超出了求解器的求解能力范围,静态符号执行在这个时候就会丢弃掉这个分支,因而导致了漏报。 Concolic由于混合了具体执行,可以获取到x和y的上一次运行中的具体取值,然后得到部分具体化的路径约束为8==Y,即第二次运行时使用 x==2,y==8作为新的测试输入,使第13行得到运行。

路径空间启发式搜索算法和路径选择

由于路径爆炸问题的存在,完全遍历整个路径空间常常是不可能的。 1)对路径约束变异,Concolic执行在每次执行完毕一条程序路径后会得到一组路径约束,DART和CUTE对其中最后一个约束取反以产生新的路径约束,实际上是对符号执行树做深度优先搜索,这意味着对一条路径上非叶子节点的符号执行将会执行多次,同样,对相同的中间性路径约束需要多次求解,按代搜索算法,每得到一组路径约束后,按照不同组合对其中多个约束取反,得到多组新的路径约束。减少了重复计算,方便并行求解。 2)对基本块覆盖打分,程序在每个分支处使用打分函数给当前路径 已经执行的部分设定分值,打分的依据可以为:距离未覆盖指令的距离、调用栈高度或被调用符号进程的最近一次执行是否覆盖了新基本块.KLEE被设计为可以同时执行多条路径,可以视为对程序路的并发执行,每次使用调度算法在现存的路径集合中选取一条执行,其选取的标准就是路径集合中分值最高者.这种方法借鉴了贪心算法的思想,即最重要的应该被优先处理。

插装

实现对Concolic执行对程序的实际执行情况的观察。

1)基于源代码的手动和自动插装
2)基于中间代码的插装

先将源代码编译成某种中间语言代码,再针对每条中间语言指令插入调用指令。

3)动态二进制插装

在不能获取程序源代码的情况下,可以借助于动态插装工具对可执行程序做动态二进制插装。

4)二进制离线插装

①抓取二进制执行轨迹 ②对其静态插装 ③重放插装后轨迹并获取需要的约束条件。

路径爆炸

对于无限循环体可以采用类似于限界符号执行,对循环部分只做有限次数的搜索。 一种较新疑的方法是路径约束抽象方法,通过路径剪裁算法可较好的环节路径爆炸问题。 一种环节路径爆炸的动态符号执行方法

参考论文一 参考文章二 ‘smt相关

评论

Your browser is out-of-date!

Update your browser to view this website correctly. Update my browser now

×