基于求解開銷預測的符號執(zhí)行搜索策略研究

劉經(jīng)德　陳振邦　王　戟,2

1(國防科學技術(shù)大學計算機學院　長沙　410073)2(并行與分布處理國防科技重點實驗室(國防科學技術(shù)大學計算機學院)　長沙　410073)3(95835部隊　新疆巴音郭楞　841700)(liujingde@nudt.edu.cn)

基于求解開銷預測的符號執(zhí)行搜索策略研究

劉經(jīng)德1,3陳振邦1王戟1,2

1(國防科學技術(shù)大學計算機學院長沙410073)2(并行與分布處理國防科技重點實驗室(國防科學技術(shù)大學計算機學院)長沙410073)3(95835部隊新疆巴音郭楞841700)(liujingde@nudt.edu.cn)

摘要符號執(zhí)行中約束求解所占的時間比例非常高.同時,不同復雜度約束的求解時間開銷差距懸殊,這一現(xiàn)象在對包含復雜數(shù)值計算的程序進行符號執(zhí)行時尤為明顯.在指定時間內(nèi)求解更多約束有利于覆蓋更多語句和探索更多路徑.為此,提出了基于求解開銷預測的符號執(zhí)行搜索策略.基于實驗總結(jié)出了度量約束復雜度的經(jīng)驗公式,并結(jié)合約束的歷史求解開銷來預測當前的求解開銷,從而在符號執(zhí)行過程中優(yōu)先探索求解開銷較小的路徑.在KLEE中實現(xiàn)了上述搜索策略,并對GNU科學計算庫(GSL)中的12個模塊進行了實驗.實驗結(jié)果表明,相比現(xiàn)有搜索策略,提出的搜索策略在保證語句覆蓋率的同時,可以探索更多的路徑(平均24.34%提高);而且,在相同時間內(nèi),可以查找出更多的軟件缺陷,同時查找出相同缺陷的時間開銷平均降低了44.43%.

關(guān)鍵詞符號執(zhí)行;約束求解;加權(quán)隨機搜索;缺陷查找;語句覆蓋

符號執(zhí)行是一種相對精確的程序分析技術(shù)[1],由King[2]于1976年提出.符號執(zhí)行可以系統(tǒng)地遍歷程序的路徑空間;現(xiàn)階段符號執(zhí)行技術(shù)主要用于軟件測試[3]、查找程序缺陷[4]和程序驗證[5].

在程序符號執(zhí)行過程中,路徑空間隨著程序中分支語句的數(shù)量增加呈指數(shù)級增長;同時,某些程序的路徑空間還可能是無窮的.因此,符號執(zhí)行面臨根本性的路徑爆炸問題,如何在有限時間內(nèi)更加高效地探索程序路徑空間成為了研究的熱點.1)符號執(zhí)行中的通用搜索策略希望在有限資源內(nèi)覆蓋更多的程序語句或路徑,包括深度優(yōu)先搜索(depth-first search, DFS)、隨機狀態(tài)搜索(random state search, RSS)、隨機路徑搜索(random path search, RPS)以及覆蓋率優(yōu)化搜索(coverage-optimized search, COS)等;2)也有一些工作針對某個具體目標研究高效的路徑空間搜索策略,包括提高程序語句覆蓋率[6]、面向可達性的搜索策略[7]、面向程序不同版本差異的搜索策略[8]等.

然而,符號執(zhí)行中現(xiàn)有搜索策略在約束求解方面的考慮不夠,而符號執(zhí)行中很大一部分時間開銷花在約束求解上.例如使用符號執(zhí)行工具KLEE[4]對Coreutils中的89個程序進行符號執(zhí)行,其中求解時間占總時間的41%[4].同時,由于程序中不同路徑的路徑條件(path condition, PC)復雜度的差別可能很大,從而導致其求解開銷相差懸殊,使得小部分路徑的求解可能在符號執(zhí)行中占用了大部分的求解時間.對于包含復雜數(shù)值運算的程序,比如科學計算程序,由于涉及不同規(guī)模的線性及非線性運算,其中的約束求解開銷相差非常懸殊,從而造成的上述特征更為明顯.現(xiàn)有的符號執(zhí)行搜索策略在進行路徑選擇時都沒有考慮到這一點,導致符號執(zhí)行在分析復雜運算程序時無法在有限的時間內(nèi)探索更多的程序路徑,從而制約了符號執(zhí)行探索路徑空間的能力.

針對這個問題,本文提出了一種基于求解開銷預測的符號執(zhí)行搜索(solving cost predication based search, SCPS)策略,通過對符號執(zhí)行中的求解開銷進行經(jīng)驗預測,在兼顧程序語句覆蓋率的前提下,優(yōu)先選擇求解開銷小的路徑進行探索,從而可在有限時間內(nèi)提高探索路徑的數(shù)量.本文在開源符號執(zhí)行器KLEE上實現(xiàn)了SCPS,并在開源程序上開展了實驗,實驗結(jié)果表明:在指定時間內(nèi),和已有搜索策略相比,本文提出的SCPS可在保持語句覆蓋率的同時探索更多路徑,查找出更多缺陷,并能夠在查找相同缺陷時需要更少的時間.

1背景介紹及示例

1.1符號執(zhí)行簡介

在符號執(zhí)行中,用符號值作為被分析程序的輸入,程序狀態(tài)中包含3個信息:1)變量的符號值或?qū)嶋H值；2)當前的路徑條件；3)程序計數(shù)器.

圖1是一個簡單的示例程序.函數(shù)foo()含有2個整型變量參數(shù)x和y.對foo()函數(shù)進行符號執(zhí)行過程如圖2所示.程序的初始狀態(tài)為state0,其中X和Y表示變量x和y的符號值,其路徑條件為true,表示沒有任何約束.當符號執(zhí)行到行②if (x>0)時,由于為分支語句,這時會對路徑進行分叉生成2條路徑,分別對應if (x>0)的真分支和假分支.在這2條不同的路徑上,相應的分支條件會加到所對應路徑的路徑條件中,然后調(diào)用求解器來判斷新的分支條件是否可滿足,以判斷路徑的可行性.圖2中左邊路徑的當前狀態(tài)用state1表示,其路徑條件為X>0;右邊路徑的當前狀態(tài)用state2表示,其路徑條件為X≤0.這2條路徑都存在使相應路徑條件為真的X和Y的取值,所以這2條路徑都可行.在接下來的執(zhí)行中,2條路徑分別執(zhí)行if語句對應的then塊和else塊,然后進行符號運算,變量y的取值最后分別為Y-X和Y+X.

Fig. 1The first program.
圖1示例程序1

Fig. 2　The execution tree of the first program.圖2　示例程序1的執(zhí)行樹

從上述介紹可知,符號執(zhí)行會生成被分析程序的路徑樹,樹中每個結(jié)點表示一個狀態(tài),每個葉結(jié)點都對應程序一條抽象路徑,表示滿足此路徑相應路徑約束的輸入會使程序執(zhí)行這條路徑.因此,符號執(zhí)行的過程也是對程序路徑樹的探索過程.一般而言,符號執(zhí)行的核心過程是一個由狀態(tài)選擇、指令執(zhí)行、狀態(tài)更新3部分構(gòu)成的循環(huán),其基本過程如下:1)從初始狀態(tài)開始,所有未探索的狀態(tài)構(gòu)成一個候選狀態(tài)集合;2)循環(huán)首先根據(jù)指定的搜索策略從候選狀態(tài)集合中選擇一個狀態(tài);3)執(zhí)行這個狀態(tài)中程序計數(shù)器所指向的指令,在執(zhí)行指令過程中如果需要判斷路徑可行性則對該路徑的路徑條件進行求解,在執(zhí)行分支指令時可能會加入新的狀態(tài);4)更新狀態(tài)信息,有時根據(jù)需要其他狀態(tài)的信息也將被更新.狀態(tài)選擇決定了符號執(zhí)行探索路徑空間的方式,通常的探索方式有DFS,RSS,RPS,COS等.同時,也可采用不同策略的組合,以同時發(fā)揮不同策略的特點.例如,符號執(zhí)行工具KLEE實現(xiàn)了10種搜索策略,并默認使用RPS+COS的策略組合.

1.2基于求解開銷預測的搜索策略示例

下面用1個例子介紹本文提出的SCPS搜索策略.

圖3中的程序,target的初始值為0,在每次執(zhí)行斷言“assert(target<2)”前都會執(zhí)行一次“target++”操作,可以發(fā)現(xiàn)在第2次執(zhí)行“assert(target<2)”時出現(xiàn)斷言違例錯誤.該程序的執(zhí)行樹如圖4所示,圖4中有5個狀態(tài)執(zhí)行了“assert(target<2)”語句,分別為:state4,state5,state7,state9和state11.為突出比較就本示例而言不同搜索策略在缺陷查找方面的能力,現(xiàn)忽略和觸發(fā)斷言違例無關(guān)的狀態(tài),僅考慮選擇上述5個狀態(tài)中的哪2個去觸發(fā)斷言違例開銷最小,即耗時最短.通過實驗我們統(tǒng)計了使用STP[9]對上述5個狀態(tài)的PC進行求解的求解時間(solving time, ST),求解時間按大小排序如下:

Fig. 3The second program.

圖3示例程序2

Fig. 4　The execution tree of the second program.圖4　示例程序2的執(zhí)行樹

ST{X<0,Y≥5}

ST{X<0,Y<5,X×Y<100,X×(Y+1)<100}.

觸發(fā)斷言違例的狀態(tài)組合有5種: ①〈state4,state7〉;②〈state4,state5〉;③〈state5,state7〉;④〈state5,state9〉;⑤〈state7,state11〉.理想情況下這5種組合的求解時間開銷按大小排序為:ST2

2基于求解開銷預測的加權(quán)隨機搜索策略

2.1基于約束復雜度的求解開銷預測

在符號執(zhí)行中,每條路徑的PC形如C1∧C2∧…∧Ci∧…∧Cn,其中Ci(1≤i≤n)表示一個分支條件.分支條件是一些常量和變量的表達式,其中的運算和操作主要包括:位操作、字符串操作、數(shù)值運算和比較操作等.PC的復雜度和其表達式長度、包含運算類型以及運算中所涉及的變量和常量中的數(shù)據(jù)個數(shù)等因素有關(guān).

針對同一約束條件進行求解,不同求解器的求解開銷不一樣.對于同一個求解器,不同約束的求解開銷也可能相差懸殊;同時,由于求解器的能力有限,有些復雜的約束(比如包含復雜的高階運算)甚至求解器無法及時地得到結(jié)果.雖然對約束進行求解前我們無法預知其準確的求解開銷,但約束的求解開銷與約束復雜度具有直接的聯(lián)系;因此,通過評估約束的復雜度,可以對約束的求解開銷進行預測.為了評估約束的復雜度,根據(jù)不同操作的復雜性,我們將PC中涉及的操作進行了分類,如表1所示.其中,C-E是字符串操作類,Casting是位擴展操作類,S-A是簡單的算術(shù)運算、邏輯運算及位操作類,C-A是復雜的算術(shù)運算類,Cmp是比較操作類.

另外,PC中常量和變量的個數(shù)分別用NCon和NVar表示,PC中操作類型A中所包含的操作出現(xiàn)的次數(shù)為NA.例如C-E類型中所包含的操作個數(shù)記為NC-E.為通過收集實驗數(shù)據(jù)總結(jié)約束求解開銷的經(jīng)驗公式,我們使用KLEE對GNU Scientific Library (GSL)[10]中的gsl_sf_bessel_I_CF1_ser和conicalP_negmu_xlt1_CF1這2個模塊進行了符號執(zhí)行,并在執(zhí)行時記錄了所有約束的邏輯表達式及對其求解的時間開銷,然后從這2個模塊的求解記錄中各隨機選取15條未被KLEE中的求解優(yōu)化方法命中的約束,對每條約束的邏輯表達式進行解析,統(tǒng)計出各表達式中不同操作類型的操作出現(xiàn)次數(shù)、不同操作數(shù)出現(xiàn)次數(shù)以及變量和常量的個數(shù),最后使用多元線性回歸分析方法對30組數(shù)據(jù)進行分析,最終得到約束求解復雜度的經(jīng)驗公式:

Table 1　The Operation Type in Logical Expressions

(1)

另一方面,因為當前路徑的歷史求解開銷總和比上歷史PC復雜度總和反映了在該路徑上單位復雜度所對應的求解開銷均值,為了提高求解開銷預測的準確性,可以用歷史單位復雜度的求解開銷均值乘以當前的求解復雜度來預測其求解開銷.

假設(shè)當前狀態(tài)對應所在路徑的第n+1個結(jié)點,其路徑條件PCn+1的邏輯表達式為C1∧C2∧…∧Ci∧…∧Cn∧Cn+1,(1≤i≤n).在當前路徑的第i個結(jié)點處的路徑條件PCi的約束復雜度記為Si,求解實際開銷記為Ti,則PCn+1的求解開銷預測值PTn+1可表示為

(2)

2.2加權(quán)隨機搜索

在進行狀態(tài)選擇時,如果嚴格選擇所有候選狀態(tài)中PC求解開銷預測值最小的進行執(zhí)行,將可能使符號執(zhí)行局限于某些簡單的循環(huán)中,并且在每次進行狀態(tài)選擇時都會帶來較大的選擇開銷.為了在優(yōu)先選擇求解開銷更小的狀態(tài)的同時,提高符號執(zhí)行對程序的覆蓋率,我們參考KLEE中實現(xiàn)的加權(quán)隨機搜索(weighted random search)算法,對基于求解開銷預測的搜索策略進行優(yōu)化.通過優(yōu)化降低了狀態(tài)選擇開銷,并提高了語句覆蓋率.

根據(jù)PC的求解開銷預測值PT對相應狀態(tài)賦予一個權(quán)值weight(記為W),PT越大,W越小,即在狀態(tài)選擇中被選擇的概率越小.對于求解開銷預測值在1 s內(nèi)的我們將其權(quán)值統(tǒng)一設(shè)為1,對于預測值超過最大求解時間TMST(max solving time, MST),我們也將它們的權(quán)值設(shè)為相同,這樣有助于避免某些狀態(tài)“餓死”.W與PT的對應關(guān)系如下:

(3)

加權(quán)隨機搜索算法該使用一棵二叉執(zhí)行樹維護當前所有候選狀態(tài)的信息,葉結(jié)點就是候選狀態(tài),內(nèi)部結(jié)點就是路徑分叉點,路徑分叉點處的W值為0,它還記錄了以該結(jié)點為根結(jié)點的二叉樹的所有葉結(jié)點的權(quán)值之和Wsum,算法1描述了加權(quán)隨機搜索算法.該算法的核心思想是首先產(chǎn)生一個(0,1]的隨機數(shù)p,從左往右累加二叉樹各葉結(jié)點的W值,直到加上某個葉結(jié)點的W值之前累加之和小于p×Wsum,而加上該葉結(jié)點的W值之后累加之和大于或等于p×Wsum時,則結(jié)束搜索,選擇該葉結(jié)點對應的state.

算法1. 加權(quán)隨機搜索算法.

輸入:記錄所有當前候選狀態(tài)信息的二叉樹,(0,1]內(nèi)的隨機數(shù)p;

輸出:接下來執(zhí)行的state.

① 置隨機權(quán)值Wrandom為二叉樹根結(jié)點的Wsum值乘以p;

② 令當前結(jié)點為二叉樹的根結(jié)點;

③ 如果當前結(jié)點存在左子結(jié)點,轉(zhuǎn)步驟④;否則,轉(zhuǎn)步驟⑦;

④ 如果Wrandom小于當前結(jié)點的左子結(jié)點的Wsum值,轉(zhuǎn)步驟⑤;否則,轉(zhuǎn)步驟⑥;

⑤ 令當前結(jié)點為它的左子結(jié)點,返回步驟③;

⑥ 置Wrandom為其原值減去當前結(jié)點的左子結(jié)點的Wsum值;

⑦ 如果Wrandom小于當前結(jié)點的W值,則轉(zhuǎn)步驟⑩;否則,轉(zhuǎn)步驟⑧;

⑧ 置Wrandom為其原值減去當前結(jié)點的W值.

⑨ 令當前結(jié)點為它的右子結(jié)點,返回步驟③.

⑩ 輸出當前結(jié)點對應的state.

3實驗與分析

我們基于符號執(zhí)行工具KLEE實現(xiàn)了SCPS策略.KLEE是基于LLVM平臺的C程序符號執(zhí)行工具,使用STP作為約束求解器.基于實現(xiàn)的搜索策略和KLEE已有搜索策略,我們開展了一系列的實驗,實驗想回答3個問題:1)和RPS+COS策略組合相比,SCPS+COS能否提高語句覆蓋率;2)和RPS+COS策略組合相比,SCPS+COS能否探索更多路徑;3)和RPS+COS策略組合相比,SCPS+COS是否具有更強的缺陷查找能力.

在實驗對象上,我們隨機選擇了GSL(version 1.16)中的12個模塊.GSL是一個應用廣泛的數(shù)值計算C和C++程序庫,提供如隨機數(shù)產(chǎn)生器、特殊函數(shù)和最小二乘擬合等功能.經(jīng)過長期的維護和深度測試,GSL目前已相當成熟.另外,由于目前KLEE無法直接對浮點程序進行符號執(zhí)行[11],我們引入SoftFloat把12個GSL模塊中的浮點運算手工替換成了SoftFloat中提供的操作.SoftFloat是一個高質(zhì)量的符合IECIEEE標準的整數(shù)實現(xiàn)浮點庫,支持4種最常見的浮點精度的運算:單精度(32 b)、雙精度(64 b)、擴展雙精度(80 b)以及4倍精度(128 b)[12].使用SoftFloat中的函數(shù)替換GSL程序中的基本運算后我們把這12個模塊改編成了12個獨立程序,這12個程序及其規(guī)模如表2所示,ELOC表示經(jīng)優(yōu)化后可在KLEE上執(zhí)行的測試集程序的可執(zhí)行代碼行數(shù),所有程序的規(guī)模在2 700～2 900行之間.

在實驗中我們比較了SCPS+COS(我們的方法)和RPS+COS(KLEE已有的效果較好策略)2種策略組合在語句覆蓋、探索路徑數(shù)量以及缺陷查找上的能力.所有實驗都是在處理器為Intel?Xeon?X5675 CPU(24 cores,3.07 GHz)、內(nèi)存為94 GB的服務器上進行的,操作系統(tǒng)是64位的Ubuntu 12.04.1 LTS.使用KLEE對每個程序進行分析時主要設(shè)置了以下3個參數(shù)∶--max-time=1 800(最大執(zhí)行時間為1 800 s,即30 min),--max-solver-time=50(最大求解時間為50 s),--search(設(shè)置搜索策略).由于對每個搜索策略組合來說都有部分程序無法在到達指定時間時及時終止,且它們超時時長大小不一,為公平起見,我們忽略超時后探索的路徑,僅僅比較在指定最大執(zhí)行時間30 min內(nèi)生成的路徑[13].

Table 2　Executable Line of Code (ELOC) of Test Benchmarks

3.1語句覆蓋

語句覆蓋就是度量被分析代碼中每個可執(zhí)行語句是否被執(zhí)行到了.雖然語句覆蓋常常被指責為“最弱的覆蓋”,但它仍然是最常用也是最常見的一種代碼覆蓋準則,實驗中我們使用gcov統(tǒng)計語句覆蓋率信息.統(tǒng)計語句覆蓋率時我們只考慮程序自身的可執(zhí)行代碼行數(shù),而不考慮各程序調(diào)用的庫中的代碼.使用不同策略組合分析每個程序時的語句覆蓋率如表3所示:

Table 3The Statement Coverage of Test Benchmarks Using Different Strategies

表3　使用不同策略組合時的語句覆蓋率　%

由于被分析程序中包含大量SoftFloat中的代碼,且有的路徑約束條件中包含大量復雜運算,在指定最大求解時間內(nèi)無法對這些約束進行求解,導致語句覆蓋率較低.使用SCPS+COS搜索策略時的語句覆蓋率均值為12.44%,使用RPS+COS時的語句覆蓋率均值為12.62%.雖然SCPS+COS策略組合無法提高語句覆蓋率,但我們可以認為SCPS+COS和RPS+COS的語句覆蓋能力相當.

3.2路徑數(shù)

我們統(tǒng)計了使用不同策略組合分析每個程序所探索的路徑數(shù)(記為N).實驗中發(fā)現(xiàn)不同被分析的程序所產(chǎn)生的路徑數(shù)相差特別大,為公平起見,采用路徑數(shù)提高率(記為I)來統(tǒng)計實驗結(jié)果,提高率的計算方法為

(4)

圖5顯示了對12個被分析程序采用SCPS+COS策略組合進行分析時在所探索的路徑數(shù)量上相對于RPS+COS的提高率,由低到高排列.數(shù)據(jù)顯示,對11個被分析程序進行分析時采用SCPS+COS策略組合在探索的路徑數(shù)量上要優(yōu)于RPS+COS,在1個程序上SCPS+COS要比RPS+COS稍差,這是因為該程序的執(zhí)行樹形態(tài)比較細長,采用2種策略組合最終所探索的路徑基本相同,而SCPS在狀態(tài)選擇時的開銷要比RPS稍大.平均而言,采用SCPS+COS策略組合所產(chǎn)生的路徑要比采用RPS+COS高出24.34%.

Fig. 5　The improved rate of explored paths by SCPS+COS compared with RPS+COS.圖5　SCPS+COS相對RPS+COS探索路徑提高率

同時,我們統(tǒng)計了探索路徑數(shù)量隨時間的變化情況(對每個被分析程序均以采用RPS+COS策略組合在30 min內(nèi)所覆蓋的路徑的總量為100%),圖6顯示了探索路徑數(shù)量相對均值隨時間變化情況.

Fig. 6　The time-dependent change of the relative mean number of explored paths using different strategy combinations.圖6　不同策略組合探索的路徑數(shù)相對均值隨時間的變化

可以看出在程序執(zhí)行初期，使用RPS+COS策略組合所探索的路徑數(shù)要比SCPS+COS策略多,這是因為剛開始時PC都比較簡單,求解開銷相差不大,且求解開銷和PC復雜度的歷史信息較少,求解開銷預測準確性不高.隨著PC復雜度增加及歷史信息積累,求解開銷分化越來越大,SCPS的優(yōu)勢逐漸體現(xiàn),能夠在相同時間內(nèi)探索更多路徑.因此,當執(zhí)行時間夠長時,和RPS+COS策略組合相比,SCPS+COS能夠探索更多路徑.

3.3缺陷查找

進一步,我們希望比較RPS+COS(簡稱R+C)和SCPS+COS(簡稱S+C)這2種搜索策略組合在缺陷查找方面的能力.我們使用程序變異工具Milu[14]對被分析的12個程序進行變異,變異后生成的程序叫變異體(mutant).

我們使用Milu共產(chǎn)生了3 639個變異體,然后用KLEE來分析變異后的程序,希望能夠發(fā)現(xiàn)變異點.在實驗中我們使用KLEE對每個變異體進行2次符號執(zhí)行,分別使用上述2種策略組合,執(zhí)行時設(shè)置最大執(zhí)行時間為600 s、單次最大求解時間為30 s.表4給出了實驗結(jié)果.

Table 4　The Experimental Results of Bug Finding in Mutants

Notes： R+C is short of RPS+COS, and S+C is short of SCPS+COS.

實驗共查找出361個缺陷,RPS+COS策略組合能找出其中的346個,SCPS+COS能找出其中的356個,2種策略組合都能查找出的缺陷有341個.對比這2種策略組合查找這341個相同bug的時間開銷發(fā)現(xiàn)SCPS+COS策略組合查找出其中的215個耗時更短,41個持平,只有81個耗時更長.平均而言,查找相同缺陷時,SCPS+COS策略組合要比RPS+COS減少44.43%,計算方法如式(5)所示,其中STR+C和STS+C是分別使用RPS+COS策略和SCPS+COS策略查找所有相同缺陷時的總時間開銷.

davg=(STR+C-STS+C)STR+C×100.00%.

(5)

從上述實驗結(jié)果可以看出,對于實驗中變異后的程序,SCPS+COS策略組合在相同時間內(nèi)能夠找出更多的缺陷,并且找出相同缺陷需要的時間更短.

3.4有效性

實驗中我們從GSL中隨機選取了12個模塊作為被分析程序,具有一定的代表性.由于GSL本身很成熟,存在的缺陷較少,我們只在變異程序及而非實際程序中找到了更多缺陷.從實驗數(shù)據(jù)可以看出采用SCPS+COS策略組合時查找相同缺陷時間開銷的平均減少率(44.43%)要比其探索的路徑數(shù)量相對提高率(24.34%)高,主要原因如下:1)開銷的平均減小率統(tǒng)計的是查找341個相同bug的平均耗時減少水平,探索的路徑數(shù)量相對提高率在統(tǒng)計時因為不同程序的被探索路徑數(shù)量相差很大,為公平起見統(tǒng)計的是這12個程序的平均提高率,不是所有路徑總和的提高率(37.82%);2)SCPS策略優(yōu)先探索求解開銷較小的路徑,隨著后續(xù)簡單路徑越來越少,將不得不探索一些更為復雜的路徑,和RPS相比的優(yōu)勢也將減弱.

4相關(guān)工作

為緩解符號執(zhí)行的路徑爆炸問題,提高語句覆蓋率及缺陷查找能力,研究者們提出了很多搜索策略、查詢優(yōu)化方法及并行優(yōu)化技術(shù).

在搜索策略方面,Cadar等人[15]開發(fā)的工具EXE中采用了一種最佳優(yōu)先搜索策略(best-first search),根據(jù)相應的目標采用啟發(fā)式搜索算法選擇所有候選執(zhí)行狀態(tài)中最符合該目標的一個執(zhí)行狀態(tài).Burnim等人[16]也使用啟發(fā)式信息引導動態(tài)符號執(zhí)行的搜索過程,他們構(gòu)建了一個被分析程序的加權(quán)控制流圖,通過比較控制流圖中各未覆蓋過的語句和當前位置的距離優(yōu)先探索最近的程序塊.為了查找特定的語句中是否存在缺陷,Ma等人[7]提出了面向程序中某個位置的符號執(zhí)行搜索策略,基于在過程間控制流圖上到目標語句的最短路徑進行探索.面向目標的符號執(zhí)行方法[7]在指定的搜索目標的引導下,交替使用后向和前向的搜索方式,能夠快速地查找出覆蓋目標程序點的路徑.相比而言,本文提出的搜索策略是從符號執(zhí)行中約束求解的角度來提高符號執(zhí)行的搜索能力,與上述一些策略是互補的關(guān)系,可以組合使用.

在查詢優(yōu)化方面,KLEE實現(xiàn)了以下優(yōu)化方法[4]:通過重寫簡化表達式、進行獨立性檢查以消除無關(guān)約束以及通過反例緩存獲取求解結(jié)果,取得了不錯的效果.文獻[17]中提出了猜測符號執(zhí)行方法,將現(xiàn)代處理器流水結(jié)構(gòu)中的猜測思想引入到符號執(zhí)行中,僅當路徑上未判定分支語句個數(shù)達到一定數(shù)量或到達葉結(jié)點時才對路徑的可行性進行判斷,從而可以減少約束求解的次數(shù).文獻[18]中設(shè)計了一種能夠自動選擇時機和方式進行狀態(tài)合并的動態(tài)優(yōu)化方法,通過狀態(tài)合并減少了待遍歷的路徑數(shù).Visser等人[19]提出了Green框架,Green獨立于符號執(zhí)行工具,它能夠?qū)⒅暗那蠼饨Y(jié)果存儲在內(nèi)存數(shù)據(jù)庫中.這種存儲方式使得同一程序的不同分析過程、不同求解器調(diào)用以及不同程序的分析過程、不同機器之間能夠共享緩存信息.相比而言,本文的工作是通過約束求解的開銷來引導符號執(zhí)行的搜索過程,上述一些工作可能會與我們提的搜索策略有沖突,比如文獻[18]中的方法會增加路徑條件的復雜度.因此,我們的策略如何與已有查詢優(yōu)化方法相結(jié)合是下一步需要研究的內(nèi)容.

并行優(yōu)化技術(shù)[20-22]是符號執(zhí)行技術(shù)研究的一個重要方向.并行優(yōu)化技術(shù)主要是采用不同的算法將程序的路徑空間進行劃分,同時使用不同的計算單元對劃分后的路徑空間不同部分進行探索；并行優(yōu)化技術(shù)還需要考慮不同計算單元之間的信息交互及負載均衡.目前,很多并行優(yōu)化算法在緩解符號執(zhí)行的路徑爆炸問題上取得了很好的效果.但是,理論上,并行優(yōu)化技術(shù)的最大收益與計算單元的數(shù)量呈線性關(guān)系,而路徑數(shù)卻與分支數(shù)呈指數(shù)關(guān)系,并行優(yōu)化技術(shù)并不能從根本上解決路徑爆炸問題.

5總結(jié)

提出并實現(xiàn)了一種基于求解開銷預測的符號執(zhí)行搜索策略.實驗表明,相比現(xiàn)有搜索策略,本文提出的策略可以在保證相當語句覆蓋率的前提下,探索更多的程序路徑(24.34%的提升);在缺陷查找方面,針對被分析程序的3 639個變異體進行分析,使用本文提出的策略多可多發(fā)現(xiàn)10個軟件缺陷,并且對于相同的程序缺陷,本文中策略發(fā)現(xiàn)這些缺陷需要的耗時平均減少了44.43%.后續(xù)研究將主要從3個方面開展:

1) 改進求解開銷預測算法;

2) 從基本路徑覆蓋率、平均代碼覆蓋率以及平均錯誤檢測率等方面上進一步比較SCPS+COS和其他搜索策略;

3) 對更多實際程序進行分析,進一步比較SCPS+COS和其他搜索策略在缺陷查找方面的能力.

參考文獻

[1]Zhang Jian. Sharp static analysis of programs [J]. Chinese Journal of Computers, 2008, 31(9): 1549-1553 (in Chinese)(張健. 精確的程序靜態(tài)分析[J]. 計算機學報, 2008, 31(9): 1549-1553)

[2]King J C. Symbolic execution and program testing [J]. Communications of the ACM, 1976, 19(7): 385-394

[3]Cadar C, Godefroid P, Khurshid S, et al. Symbolic execution for software testing in practice: preliminary assessment [C]Proc of the 33rd Int Conf on Software Engineering. New York: ACM, 2011: 1066-1071

[4]Cadar C, Dunbar D, Engler D R. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs [C]Proc of the 8th USENIX Symp on Operating Systems Design and Implementation. Berkeley, CA: USENIX Association, 2008: 209-224

[5]Jaffar J, Navas J A, Santosa A E. Unbounded symbolic execution for program verification [C]Proc of the 2nd Int Conf on Runtime verification. Berlin: Springer, 2012: 396-411

[6]Bugrara S, Engler D R. Redundant state detection for dynamic symbolic execution [C]Proc of the 2013 USENIX Annual Technical Conf. Berkeley, CA: USENIX Association, 2013: 199-211

[7]Ma K, Phang K, Foster J, et al. Directed symbolic execution [G]Static Analysis. Berlin: Springer, 2011: 95-111

[8]Person S, Yang G, Rungta N, et al. Directed incremental symbolic execution [J]. ACM SIGPLAN Notices, 2011, 46(6): 504-515

[9]Ganesh V, Dill D L. A decision procedure for bit-vectors and arrays [C]Proc of the 19th Int Conf on Computer aided verification. Berlin: Springer, 2007: 519-531

[10]Free Software Foundation (FSF). GSL: GNU scientific library [EBOL]. [2014-07-31]. http:www.gnu.orgsgsl

[11]Romano A. Practical floating-point tests with integer code [C]Proc of the 15th Int Conf on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer, 2014: 337-356

[12]Hauser J. Berkeley SoftFloat [EBOL]. [2014-07-31]. http:www.jhauser.usarithmeticSoftFloat.html

[13]Li Y, Su Z, Wang L, et al. Steering symbolic execution to less traveled paths [J]. ACM SIGPLAN Notices, 2013, 48(10): 19-32

[14]Jia Y, Harman M. MILU: A customizable, runtime-optimized higher order mutation testing tool for the full C language [C]Proc of the 3rd Testing: Academic and Industrial Conf—Practice and Research Techniques. Piscataway, NJ: IEEE, 2008: 94-98

[15]Cadar C, Ganesh V, Pawlowski P M, et al. EXE: Automatically generating inputs of death [C]Proc of the 13th ACM Conf on Computer and Communications Security. New York: ACM, 2006: 332-335

[16]Burnim J, Sen K. Heuristics for scalable dynamic test generation [C]Proc of the 23rd Int Conf on Automated Software Engineering. Los Alamitos, CA: IEEE Computer Society, 2008: 443-446

[17]Zhang Y, Chen Z, Wang J. Speculative symbolic execution [C]Proc of the 23rd Int Symp on Software Reliability Engineering (ISSRE). Piscataway, NJ: IEEE, 2012: 101-110

[18]Kuznetsov V, Kinder J, Bucur S, et al. Efficient state merging in symbolic execution [J]. ACM SIGPLAN Notices, 2012, 47(6): 193-204

[19]Visser W, Geldenhuys J, Dwyer M B. Green: Reducing, reusing and recycling constraints in program analysis [C]Proc of the 20th ACM SIGSOFT Int Symp on the Foundations of Software Engineering. New York: ACM, 2012: 58-68

[20]King A. Distributed parallel symbolic execution [D]. Manhattan, Kansas: Kansas State University, 2009

[21]Ciortea L, Zamfir C, Bucur S, et al. Cloud9: A software testing service [J]. ACM SIGOPS Operating Systems Review, 2010, 43(4): 5-10

[22]Staats M, Pǎsǎreanu C. Parallel symbolic execution for structural test generation [C]Proc of the 19th Int Symp on Software Testing and Analysis. New York: ACM, 2010: 183-194

Liu Jingde, born in 1990. Master. Student member of China Computer Federation. His research interests include high confidence software and system, symbolic execution.

Chen Zhenbang, born in 1981. PhD and assistant professor. His current research interests include program analysis and verification, component-oriented software engineering.

Wang Ji, born in 1969. PhD. Professor and PhD supervisor. Senior member of China Computer Federation. His main research interests include high confidence software and system, software engineering and distributed computing.

Solving Cost Prediction Based Search in Symbolic Execution

Liu Jingde1,3, Chen Zhenbang1, and Wang Ji1,2

1(CollegeofComputer,NationalUniversityofDefenseTechnology,Changsha410073)2(ScienceandTechnologyonParallelandDistributedProcessingLaboratory(CollegeofComputer,NationalUniversityofDefenseTechnology),Changsha410073)3(95835PLATroops,Bayingolin,Xinjiang841700)

AbstractIn symbolic execution, constraint solving needs a large proportion of execution time. The solving time of a constraint differs a lot with respect to the complexity, which happens a lot when analyzing the programs with complex numerical calculations. Solving more constraints within a specified time contributes to covering more statements and exploring more paths. Considering this feature, we propose a solving cost prediction based search strategy for symbolic execution. Based on the experimental data of constraint solving, we conclude an empirical formula to evaluate the complexity of constraints, and predict the solving cost of a constraint combined with historical solving cost data. The formula is used in our strategy to explore the paths with a lower solving cost with a higher priority. We have implemented our strategy in KLEE, a state-of-art symbolic executor for C, and carried out the experiments on the randomly selected 12 modules in GNU Scientific Library (GSL). The experimental results indicate that: in a same period, compared with the existing strategy, our strategy can explore averagely 24.34% more paths, without sacrificing the statement coverage; and our strategy can find more bugs. In addition, the time of using our strategy for finding same bugs decreases 44.43% in average.

Key wordssymbolic execution; constraint solving; weighted random search; bug finding; statement covering

收稿日期：2014-12-08；修回日期：2015-03-26

基金項目：國家“九七三”重點基礎(chǔ)研究計劃基金項目(2014CB340703);國家自然科學基金項目(61120106006,61472440,61272140)

中圖法分類號TP311

This work was supported by the National Basic Research Program of China (973 Program) (2014CB340703) and the National Natural Science Foundation of China (61120106006,61472440,61272140).