一種基于程序功能標(biāo)簽切片的制導(dǎo)符號執(zhí)行分析方法?

甘水滔 , 王林章 , 謝向輝 , 秦曉軍 , 周 林 , 陳左寧

1(數(shù)學(xué)工程與先進(jìn)計(jì)算國家重點(diǎn)實(shí)驗(yàn)室,江蘇 無錫 214083)

2(計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué)),江蘇 南京 210023)

大多數(shù)應(yīng)用軟件中存在多個(gè)功能選項(xiàng).在Linux 系統(tǒng)下,目錄“/bin”和“/usr/bin”下的絕大多數(shù)應(yīng)用程序包含多個(gè)功能選項(xiàng),表 1 中列舉了從Linux 系統(tǒng)下隨機(jī)挑選的應(yīng)用程序,并且統(tǒng)計(jì)了各自的功能選項(xiàng)數(shù)量,如coreutils8.22 中的ls 程序包含54 個(gè)選項(xiàng),who 程序中包含14 個(gè)選項(xiàng),mkdir 程序中包含6 個(gè)選項(xiàng),diffutils3.2 中diff 程序包含46 個(gè)選項(xiàng)等.可以發(fā)現(xiàn),每個(gè)功能選項(xiàng)或幾個(gè)功能選項(xiàng)組合,對應(yīng)程序中一部分獨(dú)立的執(zhí)行路徑.圖1 給出了一個(gè)典型的示例程序.該程序從命令行可輸入a,b,c,d,e,f等選項(xiàng),每個(gè)選項(xiàng)的輸入將執(zhí)行其對應(yīng)的功能函數(shù),如a選項(xiàng)對應(yīng)exe_a函數(shù)等,選項(xiàng)e和選項(xiàng)f必須在選項(xiàng)c使用之后有效.本文把程序的命令行選項(xiàng)開關(guān)稱為功能標(biāo)簽.

Table 1 Parts of applications containing function label random relected in Linux system表1 Linux 系統(tǒng)下的隨機(jī)挑選的部分包含功能標(biāo)簽的應(yīng)用程序

Fig.1 Sample program圖1 示例程序

針對這種帶功能標(biāo)簽的應(yīng)用軟件,其測試手段主要依賴于靜態(tài)分析和動(dòng)態(tài)分析兩大類方法.靜態(tài)分析可以通過控制流、數(shù)據(jù)流分析等方法[1]獲取功能標(biāo)簽、程序路徑及程序缺陷的相關(guān)信息,但由于不能構(gòu)造測試用例,無法驗(yàn)證其分析結(jié)果的真實(shí)性.動(dòng)態(tài)分析方法主要分為基于輸入數(shù)據(jù)變異的動(dòng)態(tài)分析方法[2]和符號執(zhí)行分析方法[3]:基于輸入數(shù)據(jù)變異的動(dòng)態(tài)分析方法在不知道功能標(biāo)簽信息的情況下,難以自動(dòng)生成功能標(biāo)簽信息,因而在測試的過程中極其容易陷入只對部分或極少數(shù)的功能路徑進(jìn)行分析,具有很強(qiáng)的隨機(jī)性;符號執(zhí)行方法把程序的外部輸入數(shù)據(jù)視為符號變量,運(yùn)行并分析程序路徑上的所有語句,對數(shù)據(jù)依賴于外部輸入的變量進(jìn)行符號化,不斷收集條件分支語句的條件約束建立相應(yīng)的約束系統(tǒng),再利用約束求解器判定并求解執(zhí)行路徑對應(yīng)的約束集,能夠自動(dòng)生成可行路徑的測試?yán)?通過精確地模擬程序的執(zhí)行、跟蹤變量的所有取值,理論上,符號執(zhí)行可以做到對任意可執(zhí)行路徑的覆蓋,實(shí)現(xiàn)對所有功能標(biāo)簽相關(guān)路徑的測試?yán)蠼?因此,與其他測試方法相比,在功能覆蓋及全局路徑的覆蓋效果上,符號執(zhí)行方法更能適應(yīng)于該類帶功能標(biāo)簽的應(yīng)用軟件.但程序路徑爆炸和求解開銷過大,一直是限制符號執(zhí)行分析效率的主要難題,尤其是在不知道程序執(zhí)行路徑片段和各個(gè)功能標(biāo)簽關(guān)系的前提下,利用符號執(zhí)行進(jìn)行程序分析會面臨以下3 個(gè)問題.

?問題1:對于給定的可能存在缺陷的執(zhí)行路徑片段,難以確定較優(yōu)的路徑搜索策略進(jìn)行動(dòng)態(tài)目標(biāo)制導(dǎo).

如圖1 和后文圖3,假設(shè)需要制導(dǎo)的路徑位置處于功能標(biāo)簽c和e的相關(guān)路徑中,當(dāng)選擇采用深度優(yōu)先搜索策略(DFS)時(shí),必須遍歷所有和功能標(biāo)簽a和b相關(guān)的路徑;當(dāng)采用廣度優(yōu)先搜索策略(BFS)進(jìn)行路徑制導(dǎo)時(shí),如果目標(biāo)點(diǎn)較深,也將遍歷與功能標(biāo)簽c和e之外的功能標(biāo)簽相關(guān)路徑;當(dāng)選擇采用隨機(jī)搜索策略時(shí),將會以極小的概率制導(dǎo)該路徑片段.

?問題2:難以對某功能標(biāo)簽的所有相關(guān)路徑進(jìn)行正確性驗(yàn)證.

如圖1 和后文圖3,假設(shè)只需要驗(yàn)證功能標(biāo)簽e相關(guān)的執(zhí)行路徑,和問題1 類似,在不知道功能標(biāo)簽信息前提下,不論采用何種路徑搜索策略,無法只選擇某功能標(biāo)簽相關(guān)路徑.如果采取種子模式,即構(gòu)造一個(gè)帶選項(xiàng)e的測試?yán)M(jìn)行混合執(zhí)行,由于不知道功能標(biāo)簽之間的關(guān)系,難以構(gòu)造測試?yán)晒Φ竭_(dá)功能標(biāo)簽e相關(guān)的執(zhí)行路徑中.

?問題3:容易卡在某個(gè)包含多層循環(huán)的功能標(biāo)簽代碼片段上.

如果某塊功能代碼中包含多層循環(huán)結(jié)構(gòu),一旦符號執(zhí)行分析進(jìn)入該代碼中,容易導(dǎo)致過度的時(shí)間消耗,難以執(zhí)行到其他的功能代碼上,這樣不利于對程序的全局覆蓋測試.

針對以上3 個(gè)問題,本文提出一種基于程序功能標(biāo)簽切片的制導(dǎo)符號執(zhí)行分析方法(OPT-SSE),根據(jù)程序的功能文檔建立相應(yīng)的功能標(biāo)簽集合,利用靜態(tài)分析方法對程序進(jìn)行不同功能劃分,在程序依賴圖上生成不同功能標(biāo)簽的切片,把執(zhí)行路徑有序的映射到不同功能上,對于給定需要制導(dǎo)的目標(biāo)點(diǎn),提取與目標(biāo)點(diǎn)相關(guān)的切片,通過對切片相關(guān)節(jié)點(diǎn)進(jìn)行標(biāo)記,為符號執(zhí)行的路徑選擇提供制導(dǎo)信息.利用預(yù)定義的功能標(biāo)簽流制導(dǎo)規(guī)則裁剪無關(guān)路徑,不僅可以加速目標(biāo)點(diǎn)制導(dǎo)過程以及提升特定功能模塊的覆蓋率,通過功能切片的制導(dǎo)信息分離,還提升了對整個(gè)程序的覆蓋率.

本文第1 節(jié)描述OPT-SSE 的基本實(shí)現(xiàn)框架和流程,簡要分析該模型如何對圖1 給出的示例程序進(jìn)行制導(dǎo)加速及全局覆蓋率提升,并給出模型后面算法和規(guī)則描述的基本定義.第2 節(jié)描述功能標(biāo)簽流排序算法.第3 節(jié)描述基于符號執(zhí)行的功能標(biāo)簽流制導(dǎo)規(guī)則.第4 節(jié)描述測試與分析.第5 節(jié)對符號執(zhí)行相關(guān)工作進(jìn)行總結(jié).第6節(jié)對本文主要工作進(jìn)行總結(jié).

1 基于程序功能標(biāo)簽切片的制導(dǎo)符號執(zhí)行分析模型

1.1 模型概述

圖2 給出了功能切片符號執(zhí)行模型OPT-SSE(OPT-sliced symbolic execution)的主要執(zhí)行流程,具體如下.

(1)獲取功能標(biāo)簽.分析軟件的功能文檔,獲取功能標(biāo)簽集合,如命令行功能選項(xiàng)集合.

(2)靜態(tài)控制流分析與制導(dǎo)規(guī)則生成.首先,生成軟件代碼的中間代碼,生成每個(gè)基本塊的相關(guān)信息,再利用控制流分析生成控制流圖CFG;其次,遍歷該程序控制流圖,確定每個(gè)和功能標(biāo)簽相關(guān)的基本塊,生成功能標(biāo)簽控制流圖OPT-CFG;最后,在功能標(biāo)簽控制流圖基礎(chǔ)上,遍歷生成功能標(biāo)簽路徑OPT-Path,并利用排序規(guī)則進(jìn)行排序.

(3)制導(dǎo)符號執(zhí)行.

?將特定功能或特定代碼目標(biāo)點(diǎn)映射到對應(yīng)的一條或多條功能標(biāo)簽路徑.

?在符號執(zhí)行分析過程中,引入針對功能標(biāo)簽路徑的制導(dǎo)規(guī)則.制導(dǎo)規(guī)則包括兩種:一種為不帶功能標(biāo)簽路徑排序信息的制導(dǎo)規(guī)則,另一種是帶功能標(biāo)簽路徑排序信息的制導(dǎo)規(guī)則.

?針對特定功能對應(yīng)的功能標(biāo)簽路徑,生成相應(yīng)的測試?yán)?并進(jìn)行缺陷分析.

?針對特定代碼目標(biāo)點(diǎn)進(jìn)行制導(dǎo)分析,需要生成相應(yīng)的可達(dá)測試?yán)?

Fig.2 Guided symbolic execution model based on program function label slice (OPT-SSE)圖2 基于程序功能標(biāo)簽切片的制導(dǎo)符號執(zhí)行模型(OPT-SSE)

以圖1 的程序?yàn)槭纠?圖3 和圖4 展示了OPT-SSE 模型的優(yōu)化思想.

Fig.3 OPT-SSESpeeding up goal-guided process圖3 OPT-SSE加速目標(biāo)點(diǎn)制導(dǎo)

Fig.4 OPT-SSEImproving whole coverage圖4 OPT-SSE提升全局覆蓋率

圖3 描述了OPT-SSE 模型加速目標(biāo)點(diǎn)制導(dǎo)過程:通過靜態(tài)分析目標(biāo)點(diǎn)和各個(gè)功能標(biāo)簽的隸屬關(guān)系,為符號執(zhí)行過程提供特定功能代碼分析的制導(dǎo)信息,在符號執(zhí)行框架下,定義針對不同指令的制導(dǎo)語義規(guī)則,盡早地裁剪無關(guān)的路徑分支,以加速動(dòng)態(tài)符號執(zhí)行的目標(biāo)制導(dǎo)過程.其中,實(shí)線箭頭指向的路徑是需要制導(dǎo)的目標(biāo)路徑,斜杠表示的是分支裁剪操作.圖4 描述了OPT-SSE 模型提升全局覆蓋率過程:通過對不同的功能代碼進(jìn)行有效分割,可對整個(gè)程序進(jìn)行并行化符號執(zhí)行;同時(shí),采用多個(gè)客戶端對不同的功能代碼塊進(jìn)行分析,可避免卡在對某個(gè)功能代碼塊的分析上,以提升全局覆蓋率.即同時(shí)采用多個(gè)符號,執(zhí)行客戶端對不同的實(shí)線箭頭指向的路徑進(jìn)行制導(dǎo)分析.

1.2 模型基本定義

定義1(程序功能標(biāo)簽).一個(gè)測試程序的功能文檔中可獲取有限個(gè)功能標(biāo)簽,構(gòu)成一張功能標(biāo)簽符號表OPT={option0,option1,…,optionnum},num為功能標(biāo)簽的個(gè)數(shù),optioni表示為程序的第i個(gè)功能標(biāo)簽(0＜i＜num).

定義2(功能類型分支判定條件).對于功能標(biāo)簽符號表OPT={option0,option1,…,optionnum}的程序,其功能類型分支判定條件集用OPTcondition描述.用樹結(jié)構(gòu)描述程序中任一分支判定條件condition對應(yīng)的表達(dá)式,操作符operators為中間節(jié)點(diǎn),操作數(shù)operands為葉子節(jié)點(diǎn),判定分支判定條件condition是否為功能類型分支判定條件,根據(jù)以下等價(jià)關(guān)系:

定義3(程序控制流圖).程序控制流圖CFG用四元組〈N,E,entry,exit〉表示,其中,N表示該過程的節(jié)點(diǎn)集合,E是邊的集合,entry表示入口節(jié)點(diǎn),exit表示退出節(jié)點(diǎn).任一節(jié)點(diǎn)表示為一組連續(xù)順序執(zhí)行語句的基本塊,其中,N和entry節(jié)點(diǎn)包含的最后一條語句為分支語句.每條邊是一個(gè)表示從節(jié)點(diǎn)ni到節(jié)點(diǎn)nj可能存在控制流轉(zhuǎn)移的有序節(jié)點(diǎn)對〈ni,nj〉,并滿足:ni是nj的直接前驅(qū),nj是ni的直接后繼.每個(gè)節(jié)點(diǎn)可以有多個(gè)直接前驅(qū)節(jié)點(diǎn),但至多有兩個(gè)直接后繼節(jié)點(diǎn).entry是一個(gè)沒有前驅(qū)的節(jié)點(diǎn),exit出是一個(gè)沒有后繼的節(jié)點(diǎn).

定義4(程序執(zhí)行路徑).對于一個(gè)程序控制流圖CFG,任意存在控制流轉(zhuǎn)移的有序節(jié)點(diǎn)對〈ni,ni+1〉,從節(jié)點(diǎn)ni執(zhí)行到節(jié)點(diǎn)ni+1必須滿足分支條件conditioni,定義為,那么對于程序執(zhí)行路徑集合Path,其任一條路徑用有限個(gè)有序節(jié)點(diǎn)〈n1,…,nj〉表示,定義為,并滿足:

定義5(程序執(zhí)行路徑片段).對于一個(gè)程序控制流圖CFG,其生成的路徑片段集合為PathSeg,一條執(zhí)行路徑片段用有限個(gè)有序節(jié)點(diǎn)〈n1,…,nj〉表示,定義為

定義6(功能標(biāo)簽控制流圖).一個(gè)功能標(biāo)簽控制流圖OPT-CFG可由程序控制流圖CFG遍歷生成,用四元組〈N′,E′,entry,exit〉表示,其中:N′表示該過程的節(jié)點(diǎn)集合,每個(gè)過程節(jié)點(diǎn)表示某個(gè)功能標(biāo)簽激活后直接到達(dá)的基本塊;E′是邊的集合;entry表示入口節(jié)點(diǎn);exit表示退出節(jié)點(diǎn).每條邊用有序節(jié)點(diǎn)對描述,表示從節(jié)點(diǎn)到節(jié)點(diǎn)之間存在并且只存在一條功能標(biāo)簽控制流.節(jié)點(diǎn)到節(jié)點(diǎn)之間存在一條功能標(biāo)簽控制流邊的充要條件為:程序存在一條從的語句到達(dá)的語句的執(zhí)行路徑

定義7(功能標(biāo)簽執(zhí)行流).對于一個(gè)功能標(biāo)簽控制流圖OPT-CFG,功能標(biāo)簽執(zhí)行路徑集合用OPT-Path表示,對于任意控制流,從節(jié)點(diǎn)執(zhí)行到節(jié)點(diǎn)必須滿足約束集合constrainti定義為,其任一條路徑用有限個(gè)有序節(jié)點(diǎn)表示,并滿足:

性質(zhì)1(功能標(biāo)簽執(zhí)行流約束集).對于節(jié)點(diǎn)執(zhí)行到節(jié)點(diǎn)的約束集合constrainti,一定滿足:

性質(zhì)2(用OPT-Path 對Path 進(jìn)行分類).存在一個(gè)函數(shù)Ψ,實(shí)現(xiàn)Path到OPT-Path的映射關(guān)系:

證明:由定義可知:對于給定的程序,其程序控制流圖CFG生成執(zhí)行路徑集合Path;功能標(biāo)簽控制流圖OPTCFG生成功能標(biāo)簽執(zhí)行路徑集合OPT-Path.對于任意一條可執(zhí)行路徑X=〈n1,…,nj〉∈Path,通過刪除其中的與功能類型分支判定條件語句無關(guān)的過程節(jié)點(diǎn),得到節(jié)點(diǎn)有序序列,一定滿足:,由根據(jù)定義6 可知,.因此,任意一條可執(zhí)行路徑X可通過函數(shù)Ψ映射到唯一的一條功能標(biāo)簽執(zhí)行流Y.□

定義8(偏序關(guān)系算子).偏序算子⊙={?,?}用來描述分支節(jié)點(diǎn)的后續(xù)節(jié)點(diǎn)的大小關(guān)系或者同一程序下任一兩條執(zhí)行路徑的大小關(guān)系,對于節(jié)點(diǎn)n(分支條件為condition)的true 后續(xù)節(jié)點(diǎn)nt和false 后續(xù)節(jié)點(diǎn)nf,則定義為或者〈n,nt〉?〈n,nf〉.

定義9(程序控制流執(zhí)行路徑的偏序關(guān)系).程序控制流中兩條不同執(zhí)行路徑〈n11,…,n1i〉和〈n21,…,n2j〉,偏序關(guān)系的判定定義如下:

定義9 表明,對于一個(gè)程序中任意兩條不同路徑,一定存在某個(gè)分叉節(jié)點(diǎn),使得一條路徑執(zhí)行true 分支,另一條路徑執(zhí)行false 分支.那么執(zhí)行true 分支的路徑大于執(zhí)行false 分支的路徑,這樣可對一個(gè)程序中所有不同的可執(zhí)行路徑進(jìn)行大小關(guān)系排序.

定義10(功能標(biāo)簽執(zhí)行流的偏序關(guān)系).如果程序中任意映射到兩條功能標(biāo)簽執(zhí)行流〈〈n11,…,n1i〉〉,〈〈n21,…,n2j〉〉的執(zhí)行路徑存在相同的偏序關(guān)系,那么這兩條功能標(biāo)簽執(zhí)行流也存在類似的偏序關(guān)系,即滿足:

性質(zhì)3.同一程序下,任意不同功能標(biāo)簽執(zhí)行流存在偏序關(guān)系:

證明:設(shè)存在〈n1,…,nk〉,〈nx1,…,nxp〉,,滿足:當(dāng)時(shí),根據(jù)假設(shè),一定存在n2y(1＜y≤j)或者n1d(1＜d≤i),n2y和n1d其中至少有一個(gè)節(jié)點(diǎn)具有兩個(gè)相同的功能標(biāo)簽控制流前驅(qū)節(jié)點(diǎn),這樣與定義6 相矛盾,假設(shè)不成立.所以,任意不同功能標(biāo)簽執(zhí)行流之間存在偏序關(guān)系.□

定義11(帶制導(dǎo)信息的符號執(zhí)行狀態(tài)).符號執(zhí)行環(huán)境下生成的程序狀態(tài)集合為S,任一狀態(tài)S∈S用五元組〈s,ρ,σ,g,f〉表示,其中,s表示狀態(tài)S下一步執(zhí)行的語句序列,ρ表示狀態(tài)S的約束條件集合,σ表示狀態(tài)S的符號變量到符號值的映射關(guān)系,g表示狀態(tài)S下一步需要制導(dǎo)的基本塊信息,f表示狀態(tài)S需要制導(dǎo)的功能標(biāo)簽流.

2 功能標(biāo)簽流排序算法

功能標(biāo)簽路徑生成和排序算法OptPathGenerationAndSorting第1 行～第8 行通過對每個(gè)過程內(nèi)控制流圖進(jìn)行線性掃描,獲取包含功能標(biāo)簽分支語句的基本塊,再通過控制流分析確定滿足功能標(biāo)簽分支條件的后繼基本塊,加入到功能標(biāo)簽節(jié)點(diǎn)集合OptNode中;第9 行通過調(diào)用OptCfgGeneration函數(shù)生成過程控制流圖對應(yīng)的功能標(biāo)簽控制流圖OptCfg;第10 行、第11 行對第1 條功能標(biāo)簽路徑的節(jié)點(diǎn)數(shù)量初始化;第12 行通過調(diào)用OptPathSorting生成排序好的功能標(biāo)簽路徑集合.

功能標(biāo)簽路徑生成和排序算法.OptPathGenerationAndSorting.

功能標(biāo)簽控制流圖生成算法OptCfgGeneration利用兩遍遍歷從程序控制流圖生成功能標(biāo)簽控制流圖,算法第1 行～第13 行第1 遍深度遍歷生成功能標(biāo)簽控制流圖的中間圖,該圖會出現(xiàn)某個(gè)功能標(biāo)簽節(jié)點(diǎn)可能出現(xiàn)多個(gè)相同的前驅(qū)節(jié)點(diǎn);算法第14 行～第23 行通過對每個(gè)功能標(biāo)簽節(jié)點(diǎn)進(jìn)行檢查,對于出現(xiàn)多個(gè)相同的前驅(qū)節(jié)點(diǎn)的功能標(biāo)簽節(jié)點(diǎn),復(fù)制一個(gè)別名功能標(biāo)簽節(jié)點(diǎn),并建立和功能標(biāo)簽節(jié)點(diǎn)的映射關(guān)系,這樣就能確立功能標(biāo)簽路徑的唯一性.圖5 給出了一個(gè)樣例.

功能標(biāo)簽控制流圖生成算法.OptCfgGeneration.

Fig.5 Uniqueness generation for function label path圖5 功能標(biāo)簽路徑唯一性確立

功能標(biāo)簽流排序算法OptPathSorting對功能標(biāo)簽控制流圖深度遍歷生成功能標(biāo)簽路徑集合,根據(jù)路徑生成的先后次序正好確定了功能標(biāo)簽路徑的偏序關(guān)系.

功能標(biāo)簽流排序.OptPathSorting.

3 基于符號執(zhí)行的功能標(biāo)簽流制導(dǎo)規(guī)則

以下定義了兩種功能標(biāo)簽流制導(dǎo)規(guī)則:無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則和帶序信息的功能標(biāo)簽流制導(dǎo)規(guī)則.每種制導(dǎo)規(guī)則都實(shí)現(xiàn)了3 種指令處理語義規(guī)則:調(diào)用指令處理語義規(guī)則、分支指令處理語義規(guī)則、其他指令處理語義規(guī)則.由于分支指令處理語義涉及的情況多,表2 定義了規(guī)則中使用的部分基本符號,作為任意語義描述的前提條件,使用真值表(表3 和表4)對前置條件的取值進(jìn)行描述,并對應(yīng)不同的語義情況,表5 為表3、表4 中前置條件對應(yīng)的輸出集合.

Table 2 Basic symbol definition of rule (as precondition for any semantic description)表2 規(guī)則基本符號定義(作為任意語義描述的前提條件)

Table 3 Precondition truth Table 2 on branch instruction processing semantics of function label flow guided rule without ordering information表3 無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中分支指令處理相關(guān)語義前置條件真值表2

Table 4 Precondition truth Table 3 on branch instruction processing semantics of function label flow guided rule without ordering information表4 無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中分支指令處理相關(guān)語義前置條件真值表3

Table 5 Precondition and related output assemble表5 前置條件和對應(yīng)的輸出集合

Fig.6 Finite state machine model for guided symbolic state information conversion圖6 符號狀態(tài)制導(dǎo)信息轉(zhuǎn)換的有限狀態(tài)機(jī)模型

無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則：

調(diào)用指令處理語義規(guī)則：

調(diào)用指令處理語義1 描述的是當(dāng)調(diào)用一個(gè)函數(shù)時(shí)的制導(dǎo)符號狀態(tài)的變化情況,調(diào)用指令處理語義2 描述的是當(dāng)從一個(gè)函數(shù)返回時(shí)的制導(dǎo)符號狀態(tài)的變化情況.

分支指令處理語義規(guī)則：

圖7 對應(yīng)了分支指令處理語義規(guī)則的各種語義:語義1 和語義2 表示只有一個(gè)條件分支可滿足,并且直接跳轉(zhuǎn)到目標(biāo)功能標(biāo)簽流對應(yīng)的相關(guān)節(jié)點(diǎn);語義3 和語義4 表示只有一個(gè)條件分支可滿足,并且直接跳轉(zhuǎn)到非功能標(biāo)簽節(jié)點(diǎn);語義5 和語義6 表示只有一個(gè)條件分支可滿足,并且直接跳轉(zhuǎn)到與目標(biāo)功能標(biāo)簽流不相關(guān)的功能標(biāo)簽節(jié)點(diǎn);語義7～語義19 表示兩個(gè)條件分支均可滿足,分別跳轉(zhuǎn)到與目標(biāo)功能標(biāo)簽流不相關(guān)的功能標(biāo)簽節(jié)點(diǎn)、與目標(biāo)功能標(biāo)簽流相關(guān)的功能標(biāo)簽節(jié)點(diǎn)、非功能標(biāo)簽節(jié)點(diǎn)的各種組合情況;語義20 表示當(dāng)制導(dǎo)符號狀態(tài)下一步需要制導(dǎo)的基本塊信息g=ε時(shí),直接刪除該制導(dǎo)符號狀態(tài).

Fig.7 Branch instruction processing semantics of function label flow guided rule without ordering information圖7 無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中分支指令處理相關(guān)語義

其他指令處理語義規(guī)則:

調(diào)用指令處理語義規(guī)則和其他指令處理語義規(guī)則與無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中各條語義的前置條件、輸入、輸出完全一樣;分支指令處理語義規(guī)則與無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則下第1 條～第7 條和第10 條～第20 條共18 條語義的前置條件、輸入、輸出完全一樣;第8 條和第9 條語義更改為以下4 條語義操作:前兩條語義實(shí)現(xiàn)圖8 中的裁剪策略1,后兩條語義實(shí)現(xiàn)了圖8 中的裁剪策略2.裁剪策略1 表示當(dāng)制導(dǎo)的兩個(gè)分支中,其中一個(gè)基本塊屬于制導(dǎo)的特定功能標(biāo)簽之外的功能標(biāo)簽時(shí),另一個(gè)基本塊屬于非特定功能標(biāo)簽,并滿足屬于制導(dǎo)的特定功能標(biāo)簽之外的功能標(biāo)簽的基本塊在外側(cè).由于內(nèi)側(cè)的基本塊或后續(xù)基本塊仍然可能屬于特定功能標(biāo)簽,所以只能裁剪掉包含屬于制導(dǎo)的特定功能標(biāo)簽之外的功能標(biāo)簽的分支.裁剪策略2 表示當(dāng)制導(dǎo)的兩個(gè)分支中的一個(gè)基本塊屬于制導(dǎo)的特定功能標(biāo)簽之外的功能標(biāo)簽時(shí),另一個(gè)基本塊屬于制導(dǎo)的特定功能標(biāo)簽,并且屬于制導(dǎo)的特定功能標(biāo)簽之外的功能標(biāo)簽基本塊處于內(nèi)側(cè).如果根據(jù)排序信息知道特定功能標(biāo)簽流處于這兩側(cè)功能標(biāo)簽流之間,那么可以裁剪掉這兩個(gè)分支.

Fig.8 Differece between branch instruction processing semantics of function label flow guided rule without ordering information and that with ordering information圖8 有排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中分支指令處理語義規(guī)則與無排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則中分支指令處理語義規(guī)則區(qū)別

有排序信息的功能標(biāo)簽流制導(dǎo)規(guī)則:

根據(jù)上述對各種指令的制導(dǎo)語義規(guī)則的描述,相對于KLEE 而言,OPT-SSE 在整個(gè)符號執(zhí)行過程中只會增加分支指令解釋執(zhí)行時(shí)的時(shí)間開銷,這個(gè)時(shí)間開銷主要是判定跳轉(zhuǎn)到的下一個(gè)基本塊是否包含特定功能標(biāo)簽的分支語句帶來的,OPT-SSE 在靜態(tài)分析環(huán)節(jié)可以標(biāo)記任意基本塊是否包含功能標(biāo)簽類分支,因此在制導(dǎo)過程中可直接判定某節(jié)點(diǎn)是否為功能標(biāo)簽相關(guān)節(jié)點(diǎn),不會有額外的時(shí)間開銷,但需要判定某功能標(biāo)簽節(jié)點(diǎn)是否為特定功能標(biāo)簽相關(guān)節(jié)點(diǎn)的時(shí)間開銷上限為|f|倍(即功能標(biāo)簽流f包含功能標(biāo)簽的個(gè)數(shù)).對于整個(gè)程序而言,功能標(biāo)簽相關(guān)節(jié)點(diǎn)數(shù)量只占所有節(jié)點(diǎn)數(shù)量的極小比例,因此對比KLEE,OPT-SSE 制導(dǎo)時(shí)間增加的時(shí)間開銷可以忽略.

4 測試與分析

OPT-SSE 實(shí)驗(yàn)平臺在以下環(huán)境實(shí)現(xiàn):處理器:Intel(R)Xeon(R)CPU E7-4830 2.13GHz;內(nèi)存:64GB;操作系統(tǒng):Ubuntu 12.04.

OPT-SSE 包括靜態(tài)分析和動(dòng)態(tài)分析兩個(gè)模塊:原型系統(tǒng)在llvm 上實(shí)現(xiàn)靜態(tài)分析環(huán)節(jié),包括生成控制流圖、標(biāo)記關(guān)鍵指令、生成程序功能標(biāo)簽流等工作,為動(dòng)態(tài)分析提供輔助信息;整個(gè)動(dòng)態(tài)分析環(huán)節(jié)在klee 上實(shí)現(xiàn),包括對上述各條制導(dǎo)規(guī)則的實(shí)現(xiàn).

本文從開源庫中選擇了wla_dx、Vim、Unrtf、Binutils、Sed、Wdiff、which、Findutils、Gzip、Coreutils這10 個(gè)不同的開源軟件作為測試對象,并挑選這些軟件中的20 個(gè)不同目標(biāo)進(jìn)行測試,基本信息見表6.

表6 描述了各個(gè)軟件對象的版本和功能、測試目標(biāo)以及對應(yīng)llvm IR 靜態(tài)指令數(shù)量等信息.實(shí)驗(yàn)主要針對OPT-SSE 的指令覆蓋率、分支覆蓋率、代碼目標(biāo)制導(dǎo)效率等方面的性能進(jìn)行測試,并且將其與klee 進(jìn)行橫向比較,體現(xiàn)本文工作的優(yōu)化能力.

表7 給出了wla-gb 等20 個(gè)軟件目標(biāo)的詳細(xì)實(shí)驗(yàn)數(shù)據(jù),實(shí)驗(yàn)設(shè)置每次對目標(biāo)的測試時(shí)間上限為10h.在OPT-SSE 上設(shè)置程序功能標(biāo)簽流的最大數(shù)量為8;在klee 上對每個(gè)目標(biāo)分別進(jìn)行寬度、深度、隨機(jī)這3 種路徑搜索策略的測試,選取其中覆蓋率最優(yōu)的一組數(shù)據(jù).

Table 6 Basic information of subjects表6 測試軟件對象基本信息

Table 7 Experimental data for each subject表7 對各個(gè)軟件目標(biāo)測試的實(shí)驗(yàn)數(shù)據(jù)

表7 分別統(tǒng)計(jì)了各個(gè)目標(biāo)在KLEE 和OPT-SSE 上的MinTestCaseNum、MinExeInstrNum、MaxInstrCoverage、MaxBrCoverage等指標(biāo)數(shù)據(jù),其中,

?MaxInstrCoverage表示測試10h 中取得的最大指令覆蓋率.

?MaxBrCoverage表示測試10h 中取得的最大分支覆蓋率.

?MinTestCaseNum表示測試的10h 中,達(dá)到最大指令覆蓋率和最大分支覆蓋率的最小測試?yán)蓴?shù)量.

?MinExeInstrNum表示測試10h 中,達(dá)到最大指令覆蓋率和最大分支覆蓋率的最小執(zhí)行指令數(shù)量.

圖9 描述了各個(gè)測試目標(biāo)KLEE 和OPT-SSE 的MaxInstrCoverage指標(biāo)對比情況,圖10 描述了各個(gè)測試目標(biāo)KLEE 和OPT-SSE 的MaxBrCoverage指標(biāo)對比情況.

Fig.9 Instruction coverage comparison between OPT-SSE and KLEE on different subjects圖9 OPT-SSE 和KLEE 對不同目標(biāo)的指令覆蓋率比較

Fig.10 Comparison of branch coverage between OPT-SSE and KLEE on different subjects圖10 OPT-SSE 和KLEE 對不同目標(biāo)的分支覆蓋率比較

可以發(fā)現(xiàn),與KLEE 相比,OPT-SSE 在指令覆蓋率和分支覆蓋率上得到了一定程度的優(yōu)化,其中,expr、unrtf、locate、vim 等目標(biāo)在指令覆蓋率和分支覆蓋率提升最為顯著,大約為KLEE 的1.5 倍～3.5 倍.另外可以發(fā)現(xiàn),在wdiff、which、dircolors 等多個(gè)目標(biāo)上,出現(xiàn)了OPT-SSE 的MinExeInstrNum指標(biāo)比KLEE 要小的情況.其原因可能是,OPT-SSE 在不同程序功能標(biāo)簽流上更早遇見較深的循環(huán)結(jié)構(gòu),使得MaxInstrCoverage和MaxBrCoverage兩個(gè)指標(biāo)一直得不到改善.但在整體覆蓋率上,仍然比KLEE 有所提升.

圖11 和圖12 分別給出了wla-gb 在測試過程中指令覆蓋率和分支覆蓋率的實(shí)時(shí)變化情況.可以發(fā)現(xiàn),指令覆蓋率和分支覆蓋率從測試開始到最后,OPT-SSE 比KLEE 的優(yōu)化效果明顯.

Fig.11 Comparison of instruction coverage and time overhead between OPT-SSE and KLEE when analyzing wla-gb圖11 OPT-SSE 和KLEE 分析wla-gb 時(shí)的指令覆蓋率和執(zhí)行時(shí)間對比

Fig.12 Comparison of branch coverage and time overhead between OPT-SSE and KLEE when analyzing wla-gb圖12 OPT-SSE 和KLEE 分析wla-gb 時(shí)的分支覆蓋率和執(zhí)行時(shí)間對比

表8 給出了OPT-SSE 和KLEE 在代碼目標(biāo)制導(dǎo)能力方面的對比情況.

Table 8 Comparison between OPT-SSE and KLEE on code goal-guided capability表8 OPT-SSE 和KLEE 在代碼目標(biāo)制導(dǎo)能力上的對比

圖13 描述了OPT-SSE 與KLEE 相比,在代碼目標(biāo)制導(dǎo)速度和成功率上的提升情況.針對各個(gè)測試目標(biāo),本文利用靜態(tài)分析[4-6]獲取初步脆弱性可疑點(diǎn)集合,然后從集合中篩選20 個(gè)脆弱點(diǎn)作為代碼目標(biāo)集,分別利用OPT-SSE 和KLEE 進(jìn)行1h 的制導(dǎo)分析.設(shè)置1h 的時(shí)間上限,是考慮多個(gè)目標(biāo)在1h 后指令覆蓋率變化很小.表中統(tǒng)計(jì)了各個(gè)目標(biāo)分別在KLEE 和OPT-SSE 上的代碼目標(biāo)制導(dǎo)時(shí)間開銷、代碼目標(biāo)制導(dǎo)加速比、制導(dǎo)成功數(shù)量以及成功率提升等指標(biāo)的詳細(xì)數(shù)據(jù),其中,代碼目標(biāo)制導(dǎo)時(shí)間開銷為KLEE 和OPT-SSE 都能成功制導(dǎo)的代碼目標(biāo)時(shí)間開銷平均值.選擇KLEE 和OPT-SSE 都能成功制導(dǎo)的代碼目標(biāo),是為了更好地比較代碼目標(biāo)制導(dǎo)加速情況.本文設(shè)定:代碼目標(biāo)制導(dǎo)加速比=KLEE 的代碼目標(biāo)制導(dǎo)時(shí)間開銷/OPT-SSE 的代碼目標(biāo)制導(dǎo)時(shí)間開銷,成功率提升比例=(OPT-SSE 的制導(dǎo)成功數(shù)量-KLEE 的制導(dǎo)成功數(shù)量)/20.通過數(shù)據(jù)觀察可以發(fā)現(xiàn),在代碼目標(biāo)制導(dǎo)加速比方面,OPT-SSE 在每個(gè)目標(biāo)上都有所提升;在成功率提升比例方面,除which 外,其他目標(biāo)都有顯著的提升.

Fig.13 Improvement of OPT-SSE on code goal-guided speed and success rate compared with KLEE圖13 OPT-SSE 與KLEE 相比在代碼目標(biāo)制導(dǎo)速度和成功率上的提升情況

5 相關(guān)工作

近年來,符號執(zhí)行在程序的正確性驗(yàn)證、缺陷的發(fā)現(xiàn)和重現(xiàn)、復(fù)用代碼的檢測、自動(dòng)調(diào)試能力增強(qiáng)等方向產(chǎn)生了良好的應(yīng)用,但由于存在程序路徑爆炸增長和約束求解時(shí)間開銷過大問題,制約其通用能力的發(fā)展.學(xué)術(shù)界和工業(yè)界一直把如何拓展符號執(zhí)行的應(yīng)用面和提升符號執(zhí)行效率作為軟件程序分析領(lǐng)域的基礎(chǔ)性課題[7].符號執(zhí)行在程序分析上的應(yīng)用能力主要體現(xiàn)在以下幾點(diǎn).

(1)不同程序語言上的應(yīng)用

陸續(xù)產(chǎn)生了具備分析c/c++、JAVA、JAVAscript、python 等語言能力的符號執(zhí)行原型系統(tǒng).如,斯坦福大學(xué)Cadar 等人先后開發(fā)了EXE[8]和KLEE[9],這兩個(gè)系統(tǒng)都應(yīng)用于c/c++程序?qū)ο?KLEE 重寫了EXE 的符號執(zhí)行分析引擎,通過分析c/c++程序目標(biāo)的llvm 字節(jié)碼,提升了路徑覆蓋率和缺陷發(fā)現(xiàn)能力.NASA 的Robust 軟件工程開發(fā)小組開發(fā)了JAVA pathfinder[10,11],通過分析JAVA 程序的字節(jié)碼,具備應(yīng)用于并發(fā)性JAVA 程序分析的能力.伯克利大學(xué)的Saxena 等人設(shè)計(jì)了一種適用于字符串求解的約束語言Kaluza[12],適用于求解各種事件空間以及數(shù)值空間,在此基礎(chǔ)上,構(gòu)建一個(gè)適用于JAVAscript 語言的符號執(zhí)行框架,具備檢測命令注入缺陷的能力.洛桑聯(lián)邦理工大學(xué)的Bucur 等人開發(fā)了Chef[13],通過對python 解釋器的相關(guān)包裹函數(shù)進(jìn)行符號插樁處理,對python 語言對象和解釋器進(jìn)行不同層次的符號執(zhí)行,構(gòu)建了適應(yīng)于python 語言的符號執(zhí)行引擎.

(2)不同系統(tǒng)平臺上的應(yīng)用

主要是針對Linux 平臺及windows 平臺,直接對二進(jìn)制程序進(jìn)行分析,通過把二進(jìn)制翻譯成符號執(zhí)行引擎可識別的中間語言,可以消除不同程序語言的影響,并且適應(yīng)于閉源程序?qū)ο?如,微軟研究院的Godefroid 等人開發(fā)了DART[14]和SAGE[15],專門用于windows 平臺的應(yīng)用程序分析,展現(xiàn)了顯著的效果.洛桑聯(lián)邦理工大學(xué)的Vitaly 等人開發(fā)了S2E[16,17].該系統(tǒng)利用qemu translator[18]將Linux 二進(jìn)制程序翻譯成llvm 字節(jié)碼,再結(jié)合KLEE實(shí)現(xiàn)對Linux 二進(jìn)制程序的分析.卡耐基梅隆大學(xué)的Sang 等人開發(fā)了Mayhem[19],通過使用Bap 平臺[20],將Linux二進(jìn)制轉(zhuǎn)換成BIL 語言,再結(jié)合符號執(zhí)行引擎后端進(jìn)行分析,在debian 系統(tǒng)上發(fā)現(xiàn)大量的缺陷.

(3)不同功能程序?qū)ο笊系膽?yīng)用

包括對應(yīng)用級程序、內(nèi)核級程序、設(shè)備驅(qū)動(dòng)級程序、固件級程序等不同功能程序的符號執(zhí)行分析.如,經(jīng)典符號執(zhí)行引擎[4,5,10,14,21-23]只適應(yīng)于應(yīng)用級程序分析,S2E 通過對操作系統(tǒng)插樁處理并添加特權(quán)指令的支持,具備分析內(nèi)核級程序的能力.洛桑聯(lián)邦理工大學(xué)的Kuznetsov 等人在S2E 基礎(chǔ)上構(gòu)建了DDT[24],通過對設(shè)備驅(qū)動(dòng)程序相關(guān)接口進(jìn)行有效配置,成功應(yīng)用于設(shè)備驅(qū)動(dòng)程序的分析.后來,康斯威星大學(xué)的Matthew 等人開發(fā)了symdrive[25].該系統(tǒng)對分析的設(shè)備中各種I/O 操作、DMA 操作、中斷操作進(jìn)行符號化,并結(jié)合靜態(tài)分析裁剪設(shè)備驅(qū)動(dòng)程序的無關(guān)路徑,提升了設(shè)備驅(qū)動(dòng)級程序分析的有效路徑覆蓋能力.康斯威星大學(xué)Davidson 等人開發(fā)的FIE[26]以及EURECOM 大學(xué)Zaddach 等人開發(fā)的Avatar[27],這些系統(tǒng)通過對符號執(zhí)行引擎支持的運(yùn)行環(huán)境對固件代碼建模,成功地用于嵌入式系統(tǒng)上的固件代碼的缺陷分析.

從符號執(zhí)行技術(shù)應(yīng)用發(fā)展趨勢[28]可看出,符號執(zhí)行應(yīng)用的程序語言對象多元化,從支持高級語言到二進(jìn)制語言,再到解釋型語言,中間語言翻譯平臺[20,29-34]的不斷發(fā)展,逐漸加強(qiáng)了符號執(zhí)行在程序語言上的通用性.但是符號執(zhí)行對于各種程序語言的分析效率仍然具有較大的提升空間,尤其是復(fù)雜、大規(guī)模程序?qū)ο蟮膽?yīng)用效果一直受制于路徑空間爆炸和約束求解開銷過大,在一定程度上,通過以下方法得以優(yōu)化或緩解.

(1)路徑搜索策略的提升

符號執(zhí)行需要采用特定的路徑搜索策略進(jìn)行狀態(tài)遍歷,一般經(jīng)典符號執(zhí)行引擎集成多個(gè)路徑搜索策略.如,KLEE[9]中實(shí)現(xiàn)了深度優(yōu)先、寬度優(yōu)先、隨機(jī)選擇、多策略交替選擇等路徑搜索策略.深度優(yōu)先選擇策略容易搜索到完整的執(zhí)行路徑,但對程序的整體覆蓋率較低;寬度優(yōu)先選擇策略會產(chǎn)生很多路徑片斷,很難分析到較深的路徑;隨機(jī)選擇選擇策略可以避免類似動(dòng)態(tài)分析過程中由于碰見復(fù)雜外部庫無法跳出來的情況;多策略交替選擇策略通過采用交替地采用深度優(yōu)先、寬度優(yōu)先、隨機(jī)選擇策略分析一段固定的時(shí)間,結(jié)合了各自的優(yōu)勢.PEX 定義了一種適應(yīng)度函數(shù),用來評估待選擇的分支離未覆蓋過分支的距離,通過這個(gè)度量值選擇最佳分支,取得的較高的覆蓋率[35].SAGE 中采用一種約束產(chǎn)生式的狀態(tài)遍歷方法(generational-based),先否定所有的路徑條件,然后逐漸將最深的路徑條件反轉(zhuǎn)回來,可以優(yōu)先遍歷到不同的深度路徑[21].Li 等人[36]提出了優(yōu)先選擇路徑分支執(zhí)行重復(fù)頻率最低的分支,可以在某些代碼場景產(chǎn)生更高的覆蓋率.

(2)約束求解優(yōu)化

KLEE 在求解模塊采用路徑預(yù)判斷、約束表達(dá)式簡化、約束集簡化、反例緩存機(jī)制等技術(shù)降低求解開銷.Romano 等人[37]建立了表達(dá)式匹配規(guī)則系統(tǒng),盡量利用歷史約束集信息確定新約束集是否可解,在一定程度上降低了對求解器的查詢次數(shù).S2PF[38]提出,避免一遇見條件分支就調(diào)用約束求解器,而是通過累積多個(gè)條件分支后再進(jìn)行求解:如果約束集可解,則說明該執(zhí)行路徑上之前的約束集都可解,避免了之前的求解開銷;如果約束集不可解,則回溯到之前沒有求解的條件分支再次執(zhí)行,從一定概率上節(jié)省了總的約束求解開銷.秦曉軍等人[39]提出了一種基于懶符號執(zhí)行的約束求解算法,自動(dòng)識別循環(huán)結(jié)構(gòu).通過推遲變量實(shí)例化等方法,有效地緩解了循環(huán)結(jié)構(gòu)的路徑組合爆炸問題,降低了求解次數(shù).

(3)冗余狀態(tài)歸約

Li 等人針對符號狀態(tài)定義弱等價(jià)關(guān)系[40],如果一組狀態(tài)滿足該關(guān)系,那么可以用一個(gè)狀態(tài)替代該組狀態(tài).例如,某循環(huán)體中的判定條件與符號變量有關(guān),并且某個(gè)變量依賴于外部庫的符號返回值,那么對于每次循環(huán),都會產(chǎn)生一個(gè)新的符號變量,這樣會出現(xiàn)大量呈弱等價(jià)關(guān)系的狀態(tài).這種方法在一定程度上加速了符號執(zhí)行過程.Bugrara 等人[41]提出,如果一組約束覆蓋的代碼行和另一組約束相同,則認(rèn)為這組約束對應(yīng)的狀態(tài)是多余的,可以消除,并利用動(dòng)態(tài)切片方法[42]確定不同約束集是否覆蓋相同代碼行.該方法提升了代碼覆蓋率.

(4)狀態(tài)合并方法

如果兩條路徑在某個(gè)代碼點(diǎn)交匯,那么可以把兩個(gè)狀態(tài)的約束集合并成一個(gè)狀態(tài)的約束集.這樣可以大量削減狀態(tài)的總數(shù)量,但有可能出現(xiàn)對合并后約束集的求解開銷大于合并之前分別求解的總開銷,尤其容易發(fā)生在大規(guī)模程序中[43].針對這一情況,出現(xiàn)了相應(yīng)的折中方法,如,

?Boonstoppel 等人[44]提出,如果兩個(gè)狀態(tài)效果相同,并且約束集中取值不同的變量與的后續(xù)路徑選擇無關(guān),那么這兩個(gè)狀態(tài)合并后約束集在后續(xù)求解中帶來的額外開銷會降低,可以選擇合并符合該條件的狀態(tài)集合.

?Kuznetsov 等人[45]提出,針對每次狀態(tài)合并之前,評估合并后約束集中新增符號變量所增加的求解器查詢次數(shù),以此確定潛在的合并點(diǎn).

(5)執(zhí)行分段和合成方法

Le 利用靜態(tài)分析根據(jù)循環(huán)體、外部庫等代碼特征將程序片段化,再通過動(dòng)態(tài)執(zhí)行獲取各個(gè)片段的相關(guān)接口信息以及自動(dòng)合成各個(gè)片段,可以更好地處理程序循環(huán)結(jié)構(gòu)和動(dòng)態(tài)庫帶來的符號化問題[46].Ramos 等人[47,48]提出,分別對各個(gè)用戶定義函數(shù)體進(jìn)行符號執(zhí)行,再對觸發(fā)函數(shù)體缺陷的輸入進(jìn)行合成,避免直接從主函數(shù)分析時(shí)出現(xiàn)的深度路徑不可達(dá)情況,可產(chǎn)生更高的語句覆蓋率.Sinha 等人[49]提出,通過對并發(fā)性程序進(jìn)行分階段執(zhí)行,有效分離線程的過程內(nèi)和過程間操作.第1 階段獲取線程全局變量信息,對線程序列進(jìn)行有效分割;第2 階段利用執(zhí)行序列的一致性把路徑片段組合成完整線程,具備并發(fā)性缺陷發(fā)現(xiàn)能力.Zamfir 等人[50]提出,對并發(fā)性程序的序列路徑合成和線程調(diào)度合成,可準(zhǔn)確地重現(xiàn)并發(fā)性缺陷.

(6)Concolic 執(zhí)行方法

該方法需要使用種子數(shù)據(jù),即初始測試?yán)?在對種子數(shù)據(jù)進(jìn)行具體執(zhí)行的過程中,收集執(zhí)行路徑的其他分支相關(guān)符號約束,構(gòu)造后續(xù)狀態(tài)集合,并在具體執(zhí)行完種子數(shù)據(jù)后,采用特定狀態(tài)選擇策略進(jìn)行符號執(zhí)行.Concolic執(zhí)行方法可以借助具體執(zhí)行特定的測試?yán)焖僦茖?dǎo)具有一定深度的代碼,可解決純符號執(zhí)行不適應(yīng)復(fù)雜目標(biāo)的深度路徑可達(dá)問題,在多個(gè)符號執(zhí)行引擎[8,9,14,15]中得到了體現(xiàn).如,KLEE 中利用種子數(shù)據(jù)進(jìn)行符號執(zhí)行,一旦執(zhí)行完種子數(shù)據(jù),就利用特定搜索策略對種子數(shù)據(jù)的分支狀態(tài)進(jìn)行遍歷;CUTE 采用不斷隨機(jī)生成測試?yán)M(jìn)行具體執(zhí)行,一旦生成的測試?yán)荒芨采w新的分支,將切換到符號執(zhí)行[51],這種Concolic 執(zhí)行方法提升了4 倍以上的覆蓋能力;DASE[52]構(gòu)造特定輸入種子,并確定其中固定字段,在種子模式執(zhí)行分析過程中,可避免對這些固定數(shù)據(jù)的約束求解,提高了分析效率.

(7)并行化方法

Cloud9[53]在KLEE 的基礎(chǔ)上、MergePoint[54]在Mayhem 的基礎(chǔ)上分別構(gòu)建了并行符號執(zhí)行框架.他們采用在集群的某個(gè)節(jié)點(diǎn)上啟動(dòng)符號執(zhí)行,動(dòng)態(tài)地選擇當(dāng)前節(jié)點(diǎn)上產(chǎn)生的不同狀態(tài),并分離到集群上的其個(gè)節(jié)點(diǎn)上繼續(xù)執(zhí)行,實(shí)時(shí)保持不同節(jié)點(diǎn)上的負(fù)載均衡,取得了良好的效果.Junaid 等人[55]提出利用不同測試?yán)齽澐殖绦蚵窂椒秶?對不同程序路徑范圍進(jìn)行并行性測試,大幅度提升覆蓋率.

大部分符號執(zhí)行性能優(yōu)化方法只適應(yīng)于特定的程序場景,需要結(jié)合多種優(yōu)勢才能應(yīng)對程序?qū)ο蠖鄻有浴?fù)雜性的通用測試需求.針對一個(gè)路徑數(shù)量過多的程序,不管采用何種路徑選擇策略,如果要做到全局覆蓋,很難達(dá)到理想的效果,需要其他優(yōu)化能力的不斷提升.基于符號執(zhí)行面臨的現(xiàn)狀,近幾年出現(xiàn)了一種實(shí)用性較強(qiáng)的應(yīng)用——制導(dǎo)符號執(zhí)行分析方法.該方法不以程序的全局覆蓋為目標(biāo),只對程序中感興趣的程序片段或性質(zhì)進(jìn)行驗(yàn)證,適用于補(bǔ)丁程序的可靠性分析、特定場景的測試?yán)伞⑻囟ㄈ毕莅l(fā)現(xiàn)等應(yīng)用方向.制導(dǎo)符號執(zhí)行一般通過靜態(tài)分析或附加的限制條件信息增強(qiáng)其分析的導(dǎo)向性,利用預(yù)定義好的制導(dǎo)規(guī)則指導(dǎo)符號執(zhí)行如何進(jìn)行更好的路徑搜索達(dá)到制導(dǎo)目的,其效果更易于提升不同代碼規(guī)模程序?qū)ο蟮膽?yīng)用.制導(dǎo)符號執(zhí)行分析方法出現(xiàn)了一系列應(yīng)用,如,Kin 等人[56]提出一種快速的程序行可達(dá)性判定和測試?yán)伤惴?在靜態(tài)控制流圖上計(jì)算每個(gè)程序分支和目標(biāo)代碼行的距離值,每執(zhí)行分支時(shí),選擇離目標(biāo)代碼最近的程序分支,能夠快速到達(dá)目標(biāo)代碼行;Paul 等人[57]通過優(yōu)先選擇程序分支到敏感指令(讀和寫)的距離最近的分支進(jìn)行制導(dǎo)分析,發(fā)現(xiàn)很多讀寫相關(guān)的缺陷;Zhang 等人[58]提出通過有限狀態(tài)機(jī)模型對正規(guī)性質(zhì)進(jìn)行定義,利用符號執(zhí)行對程序正規(guī)性質(zhì)進(jìn)行制導(dǎo)分析,有效地驗(yàn)證程序中內(nèi)存泄漏等路徑敏感缺陷;DiSE[59]先通過靜態(tài)分析檢查某軟件系統(tǒng)不同版本間的差異,并利用制導(dǎo)符號執(zhí)行產(chǎn)生差異代碼可達(dá)路徑條件,可以檢查程序更改后帶來的影響;Taneja 等人[60]通過構(gòu)建程序控制流圖,確定與修改代碼區(qū)域無關(guān)的條件分支,在符號執(zhí)行過程中裁剪這些無關(guān)分支,能夠更快地產(chǎn)生回歸測試?yán)?已驗(yàn)證程序修補(bǔ)后的正確性;Marinescu 等人[61,62]利用制導(dǎo)符號執(zhí)行實(shí)現(xiàn)對已知補(bǔ)丁集合的進(jìn)行覆蓋測試,通過計(jì)算每條指令到補(bǔ)丁代碼的條件數(shù)量作為度量距離值,采用最弱前置條件分析[63]確定目標(biāo)不可達(dá)的基本塊,最后對多個(gè)初始種子中選擇出離補(bǔ)丁代碼最近的種子數(shù)據(jù),可以為后續(xù)符號執(zhí)行制導(dǎo)補(bǔ)丁代碼提供距離最近的狀態(tài);Domagoj 等人[64]先運(yùn)用靜態(tài)分析確定二進(jìn)制程序中的脆弱點(diǎn),再借助事先在控制流邊上標(biāo)記到達(dá)脆弱點(diǎn)的靜態(tài)跳轉(zhuǎn)次數(shù)信息對這些脆弱點(diǎn)集合進(jìn)行制導(dǎo)符號執(zhí)行分析;Ge 等人[65]利用制導(dǎo)符號執(zhí)行分析方法對靜態(tài)分析得到的缺陷報(bào)告進(jìn)行動(dòng)態(tài)驗(yàn)證,提高了靜態(tài)分析的準(zhǔn)確性;Guo 等人[66]通過靜態(tài)分析確定程序正確的部分,在符號執(zhí)行過程中對這些不包含缺陷的路徑分支進(jìn)行實(shí)時(shí)的裁剪,提升了分析速度.

6 結(jié) 論

本文提出了一種基于程序功能切片的符號執(zhí)行制導(dǎo)分析方法OPT-SSE.該方法參考程序的功能文檔,在控制流圖上把提取控制功能執(zhí)行路徑的關(guān)鍵基本塊,并標(biāo)識成相應(yīng)的功能標(biāo)簽.OPT-SSE 利用功能標(biāo)簽流對程序進(jìn)行有序劃分,對于給定的代碼目標(biāo)點(diǎn),提取與之相關(guān)的功能標(biāo)簽切片,然后根據(jù)預(yù)定義的制導(dǎo)規(guī)則對該切片進(jìn)行制導(dǎo)分析.實(shí)驗(yàn)結(jié)果表明,該方法能夠顯著加速代碼目標(biāo)制導(dǎo)速度和成功率;并且通過并行的方式制導(dǎo)分析不同的程序功能切片,能夠避免符號執(zhí)行卡在某個(gè)循環(huán)結(jié)構(gòu)體上,從而提升對整個(gè)程序的分支和指令覆蓋率.

OPT-SSE 在下一步工作中需要對以下不足進(jìn)行優(yōu)化.

(1)采取靜態(tài)切片提取功能標(biāo)簽受影響的基本塊.可能會分析出部分可能執(zhí)行不到的代碼片段,從而影響后續(xù)的符號執(zhí)行制導(dǎo)效果,在下一步工作中需要借助動(dòng)態(tài)切片進(jìn)一步優(yōu)化.

(2)本文把程序的選項(xiàng)定義為功能標(biāo)簽,在今后的工作中,可以對功能標(biāo)簽進(jìn)行更寬泛的應(yīng)用,例如,把程序中所有不可變性質(zhì)歸納為相應(yīng)的功能標(biāo)簽,如固定輸入格式和結(jié)構(gòu).利用更多的功能標(biāo)簽信息,可以進(jìn)一步提升符號執(zhí)行制導(dǎo)效率.