论文分享_06_24

Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation.

背景知识

最基础的符号执行是将输入映射为符号值,对不同的程序路径维护路径条件以及变量的映射关系,最后利用约束求解来确定在不同的程序路径上是否存在满足违反assert条件的具体值输入。

最基础的符号执行在函数输入是对象或者指向对象的指针时无法对内存有一个好的建模,因此在符号执行对内存建模中有一个方法是lazy initialization(延迟初始化),即推迟对指向值及其field的初始化,直到它们被第一次访问。如测试下图中的add函数所示(该函数的作用是在输入值node结点所在链表的结尾插入一个value为v的结点),在最开始不对输入值Node l做刻画,而是在执行到语句A时,需要判断L是不是null,因此要对L做初始化,延迟初始化将L初始化为三种情况,一是初始化为null,二是初始化为一个新创建的堆对象,三是初始化为一个已经分配过内存的对象,分别考虑这三种情况对L做初始化。

如果考虑程序的执行路径为A ① B(圈1表示选择第一种情况做初始化),则对应的对应输入l=null

如果考虑程序的执行路径为A ② C→A ① B,则对应的输入为l=o1(o1=Node(l,_) 下划线表示我们不关心这个field的具体值)

但这样生成测试输入是有缺陷的,因为延迟初始化的第三种情况是将对象初始化为一个已经分配过内存的对象,随着符号执行在程序上运行,这样被分配过内存的对象越来越多,因此会导致状态爆炸的问题。

目前解决状态爆炸问题的方法有两种,一是状态融合,考虑将若干个状态做合并,将问题抛给约束求解的求解器。二是减枝,删掉无效的输入情况的探索。上图反映的是利用程序的前条件(precondition)来约束输入情况,从而做到剪枝。具体来说,上图给出了数据结构无环的前条件,因此当考虑程序执行路径为A ② C→A ③ C,这种情况生成的输入是不满足前条件的,因此该分支被剪掉,不需要对这类输入情况做进一步探索。

然而之前提出的利用前条件来减枝的方法是先生成对应输入,再用模型检测工具检查生成的输入是否满足precondition,而且之前工作的precondition描述能力有限。

基本思路

a) 利用分离逻辑公式作为precondition

b) 只生成有效的(满足precondition)输入

c) 使用上下文敏感的延迟初始化

具体实现

01 分离逻辑

本文使用的分离逻辑如下图所示,Δ表示一个符号化的堆,它是被存在量化的,κ描述堆的空间结构,emp表示堆是空的,v↦c(f’:v’)表示v指向一个c类型的对象,对象的field f’的值分别为v’,P()表示谓词的一个实例,*表示分离与;ɑ和Φ分别表示指针(不)等式和算术公式。在分离逻辑中支持归纳谓词,用pred来标识。例如

pred pre(a, b) ≡ (emp ∧ a = null ∧ b = null) ∨(∃n1, n2. a↦ node( _ , n1) * b↦ node( _ , n2) * pre(n1 , n2))

表示a和b同时为空,或者同时指向不相交的两个结点n1 n2 ,且这两个结点满足pre(n1 ,n2)

02 实现思路

         在符号执行的过程中利用符号执行的指称(语义)规则维护路径条件Δ(分离逻辑公式表示)和符号栈(将变量映射为符号值或具体值)。初始化的路径条件为函数的precondition,符号栈为将输入映为一个符号值,通过探索不同的程序路径,根据指称(语义)规则计算最强后条件。到达结束状态时,根据对结束状态的路径条件的约束求解生成符合precondition的输入。上下文敏感的延迟初始化体现在在对变量初始化时,如果当前路径条件不存在对变量的约束,则同一般的延迟初始化一样分为三种情况,若存在对变量的约束,则通过对谓词展开的方式,只生成满足路径条件的输入。具体来说,考虑对下面函数add进行测试。

该函数的输入为两个链表,输出为一个链表,两输入链表对应结点的值的和为输出链表对应结点的值,即记x链表结点的值依次为2,3,5;y链表结点的值为1,4,3,则输出链表结点的值为3,7,8。若设置precondition为pre(x,y) (该pre可以保证x和y链表长度相等且不会发生重叠)

pre(a, b) ≡ (emp ∧ a = null ∧ b = null) ∨(∃n1, n2. a↦ node( _ , n1) * b↦ node( _ , n2) * pre(n1 , n2))

执行符号执行的过程如下:

首先是初始化符号栈,将x初始化为符号值X,y初始化为符号值Y,路径条件初始化为pre(X,Y)

当执行到第(3)行时,发现没有对X做初始化,而此时路径条件中包括pre(X,Y),因此对pre(X,Y)进行展开(这里使用了最小不动点分析的方法,由于该公式比较简单,因此展开之后还是两个公式的析取)。首先选择探索第一种情况,即X=null ∧ Y =null,将该公式替换路径条件中的pre(X,Y)。这种情况下发现程序直接返回,因此调用约束求解器求解该路径条件是否满足,并生成第一种测试输入。

探索完第一种情况后,探索第二种情况,即使用(∃n1, n2. X↦ node( _ , n1) * Y↦ node( _ , n2) * pre(n1 , n2))替换路径条件中的pre(X,Y),在循环进行到第(5)行时,x.next被引用(即n1被访问),因为n1也被pre所约束,因此对pre(n1 , n2)进行展开,还是展开成两种情况,当pre(n1 , n2)被展开成基础情况,则路径条件为∃n1, n2.  X↦ node( _ , n1) * Y↦ node( _ , n2) ∧ n1 = null ∧ n2 = null 。这种情况对应的输入是X和Y只包括一个结点。而将pre(n1 , n2)展开成另一种情况会导致程序继续在循环内执行,类似的可以生成X和Y含有两个结点,含有三个结点的输入……对于循环的展开也有一个上界,保证探索的终止性。

实验分析

        作者将算法实现在JSF工具上,并与JBSE,BBE工具进行比对。测试的程序集包括SLL(单向链表)、DLL(双向链表)、AVL树以及一些其它数据结构的相关函数。precondition是一些对对应数据类型基本情况做限制的分离逻辑公式。#Tests表示生成有效测试输入(即满足程序集中的repOK函数)和生成总的测试输入的比,Cov为生成的有效输入的代码覆盖率,NCov表示生成的所有输入的代码覆盖率,#Call表示调用约束求解器的次数,T表示花费的时间。该实验反映的结果是该算法可以避免无效的测试输入,且生成的测试输入可以保证较高的代码覆盖率(TSAFE程序集上代码覆盖率低的原因是因为程序中有native method,即嵌入了C/C++语言,这是该工具目前不支持的)。此外,作者指出了该工具一定程度上增加了调用求解器的次数,而这是因为求解带有归纳谓词的路径条件更困难,这相当于生成测试输入的有效性和调用求解器次数间的一个trade off。

总结

这篇文章的主要贡献是提出利用带归纳谓词的分离逻辑公式作为路径条件,使用上下文敏感的延迟初始化策略引导输入状态空间搜索来生成测试输入的符号执行方法。该方法可以确保生成的测试输入的有效性,且有较高的代码覆盖率。

目前该工作并没有具体到找bug上,但作者也提到未来他们会结合bi-abduction和frame inference 工具来验证安全性同时生成测试样例来定位(确认)具体的bug。