分布式符號(hào)執(zhí)行平臺(tái)①

孫盼盼,董威(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院,長(zhǎng)沙 410073)

?

分布式符號(hào)執(zhí)行平臺(tái)①

孫盼盼,董威
(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院,長(zhǎng)沙 410073)

摘 要:在軟件工程學(xué)中,符號(hào)執(zhí)行技術(shù)是一門(mén)高效的程序缺陷檢測(cè)技術(shù).符號(hào)執(zhí)行使用符號(hào)值作為程序的輸入,將程序的執(zhí)行轉(zhuǎn)變?yōu)橄鄳?yīng)符號(hào)表達(dá)式的操作,通過(guò)系統(tǒng)地遍歷程序的路徑空間,實(shí)現(xiàn)對(duì)程序行為的精確分析.然而,因受路徑爆炸問(wèn)題與約束求解問(wèn)題的制約,符號(hào)執(zhí)行技術(shù)也面臨著可擴(kuò)展性差的問(wèn)題.為了在一定程度上緩解該問(wèn)題,本文實(shí)現(xiàn)了一個(gè)分布式符號(hào)執(zhí)行平臺(tái),該平臺(tái)在調(diào)度算法的調(diào)度下將任務(wù)從主節(jié)點(diǎn)分發(fā)給多個(gè)工作節(jié)點(diǎn),進(jìn)而實(shí)現(xiàn)了任務(wù)的并行執(zhí)行,降低了符號(hào)執(zhí)行的時(shí)間開(kāi)銷(xiāo).

關(guān)鍵詞:并行符號(hào)執(zhí)行; 分布式系統(tǒng); WEB平臺(tái); 缺陷檢測(cè); KLEE

1　引言

程序缺陷檢測(cè)技術(shù)保證了程序質(zhì)量、提高了程序可靠性,長(zhǎng)期以來(lái)都受到學(xué)術(shù)界與工業(yè)界的關(guān)注.目前,針對(duì)程序缺陷檢測(cè)技術(shù)的研究主要包括靜態(tài)源代碼檢測(cè)、黑盒模糊測(cè)試、污點(diǎn)分析及符號(hào)執(zhí)行等.符號(hào)執(zhí)行技術(shù)(Symbolic Execution)是一種程序分析技術(shù),它通過(guò)分析程序得到讓特定代碼區(qū)域執(zhí)行的輸入.使用符號(hào)執(zhí)行技術(shù)分析程序時(shí),該程序會(huì)使用符號(hào)值而非具體值作為輸入,在達(dá)到目標(biāo)代碼時(shí),分析器可以得到相應(yīng)的路徑約束,然后通過(guò)約束求解器得到觸發(fā)目標(biāo)代碼的具體值[1].符號(hào)執(zhí)行技術(shù)相對(duì)于其他程序分析技術(shù)而言具有程序執(zhí)行覆蓋率高、檢測(cè)結(jié)果無(wú)誤報(bào)及低漏報(bào)等優(yōu)點(diǎn),因此逐漸成為近年來(lái)學(xué)術(shù)研究的熱點(diǎn),同時(shí)也產(chǎn)生了一批優(yōu)秀的符號(hào)執(zhí)行工具,如微軟公司研發(fā)的SAGE、PEX[2]等工具,斯坦福大學(xué)于2008年發(fā)布的KLEE[3],以及NASA針對(duì)Java語(yǔ)言開(kāi)發(fā)的JPF[4]等,都是符號(hào)執(zhí)行領(lǐng)域具有代表性的成果.

符號(hào)執(zhí)行過(guò)程大致可以分為以下幾個(gè)模塊,如圖1所示.其原理為,在不實(shí)際執(zhí)行程序的前提下,把源程序翻譯為一種中間語(yǔ)言,用符號(hào)值表示程序變量的值,然后基于中間語(yǔ)言模擬程序執(zhí)行來(lái)進(jìn)行相關(guān)的分析[5].其中,約束求解模塊是符號(hào)執(zhí)行系統(tǒng)的核心模塊之一,它的主要任務(wù)是根據(jù)程序執(zhí)行過(guò)程中產(chǎn)生的路徑約束計(jì)算出所對(duì)應(yīng)的路徑條件PC(Path Condition),將PC作為新的具體輸入,利用符號(hào)執(zhí)行引擎對(duì)新輸入值進(jìn)行新一輪的分析.符號(hào)執(zhí)行技術(shù)正是通過(guò)使用這種迭代產(chǎn)生輸入的做法,在理論上達(dá)到了遍歷分析所有可行路徑的效果.

圖1　符號(hào)執(zhí)行系統(tǒng)整體結(jié)構(gòu)圖

符號(hào)執(zhí)行技術(shù)的發(fā)展也面臨著諸多問(wèn)題,其中,可擴(kuò)展性是符號(hào)執(zhí)行技術(shù)面臨的主要問(wèn)題之一.符號(hào)執(zhí)行的可擴(kuò)展性問(wèn)題主要是由路徑爆炸問(wèn)題與約束求解問(wèn)題引起的.路徑爆炸問(wèn)題是動(dòng)態(tài)符號(hào)執(zhí)行所面臨的主要問(wèn)題,已成為符號(hào)執(zhí)行實(shí)際應(yīng)用于大中型軟件系統(tǒng)的瓶頸,原因在于程序所包含的路徑數(shù)在最糟糕的情況下隨程序中分支數(shù)的增長(zhǎng)而呈指數(shù)級(jí)增長(zhǎng),因此,符號(hào)執(zhí)行雖然在理論上可以遍歷程序中每一條可達(dá)路徑并生成測(cè)試用例,但在實(shí)際執(zhí)行過(guò)程中這一目標(biāo)往往難以達(dá)到.約束求解問(wèn)題與軟件規(guī)模及軟件結(jié)構(gòu)的復(fù)雜性緊密相關(guān).實(shí)際上,隨著軟件規(guī)模的增大以及軟件結(jié)構(gòu)復(fù)雜性的提升,約束表達(dá)式將變得愈加復(fù)雜,使得求解器的求解變得極為困難.另一方面,實(shí)際程序也可能會(huì)包含各種各樣的操作,如非線(xiàn)性運(yùn)算、移位等.有研究指出,含有復(fù)雜非線(xiàn)性運(yùn)算的邏輯系統(tǒng)是不可判定的,當(dāng)約束求解器不能判定某一約束條件是否可滿(mǎn)足時(shí),其相應(yīng)的路徑也就無(wú)法進(jìn)行符號(hào)執(zhí)行[6].此外,現(xiàn)在的大多數(shù)求解器也都存在著對(duì)浮點(diǎn)操作支持不足的問(wèn)題.針對(duì)路徑爆炸問(wèn)題,研究人員提出了使用狀態(tài)合并、抽象、組合化思想、基于啟發(fā)式策略的搜索、目標(biāo)引導(dǎo)的搜索、并行化等技術(shù)來(lái)提高符號(hào)執(zhí)行的效率.這些技術(shù)從不同的角度出發(fā),試圖減少符號(hào)執(zhí)行需要探索的路徑數(shù)或者減少探索路徑空間所需的時(shí)間和空間資源消耗.在約束求解方面的研究,主要包括約束查詢(xún)的優(yōu)化技術(shù)以及特定應(yīng)用領(lǐng)域的約束求解等[7].

并行化方法即所謂的并行符號(hào)執(zhí)行[8]是符號(hào)執(zhí)行技術(shù)發(fā)展的另一個(gè)趨勢(shì),很大一部分原因在于近年來(lái)多核技術(shù)與“云計(jì)算”技術(shù)的快速發(fā)展所引起的計(jì)算方式的變革[9].常規(guī)上,并行化方法根據(jù)相應(yīng)的算法將程序的路徑空間進(jìn)行劃分,使用不同的計(jì)算單元來(lái)同時(shí)對(duì)路徑空間的不同部分進(jìn)行探索,同時(shí)又考慮了多個(gè)計(jì)算單元之間的交互和負(fù)載均衡的問(wèn)題[7].實(shí)際上,并行化方法是一種典型的以空間和計(jì)算資源換時(shí)間的例子.基于該理念已有研究者開(kāi)發(fā)出了相應(yīng)的工具,如Cloud9[10]與MergePoint[11],均取得了很好的效果.

為了在一定程度上緩解符號(hào)執(zhí)行技術(shù)的可擴(kuò)展性問(wèn)題,本研究基于開(kāi)源的符號(hào)執(zhí)行工具KLEE實(shí)現(xiàn)了一個(gè)B/S結(jié)構(gòu)的分布式符號(hào)執(zhí)行平臺(tái).該平臺(tái)通過(guò)使用多臺(tái)虛擬機(jī)并行執(zhí)行任務(wù)的方式,大幅度降低了多任務(wù)情況下符號(hào)執(zhí)行的總體求解時(shí)間開(kāi)銷(xiāo).本研究選用了開(kāi)源的KLEE作為符號(hào)執(zhí)行工具,但相關(guān)工具的選擇并不局限于KLEE,實(shí)際上,將其他符號(hào)執(zhí)行工具集成到該平臺(tái)中也非常容易.

2　分布式符號(hào)執(zhí)行平的設(shè)計(jì)與實(shí)現(xiàn)

2.1分布式符號(hào)執(zhí)行平臺(tái)架構(gòu)與功能

如圖2所示,本研究實(shí)現(xiàn)的分布式符號(hào)執(zhí)行平臺(tái)屬于明顯的B/S結(jié)構(gòu)與Master/Slave架構(gòu)相結(jié)合的產(chǎn)物,主要分為客戶(hù)端模塊、Master模塊及檢測(cè)模塊.該平臺(tái)通過(guò)設(shè)置一個(gè)待檢測(cè)隊(duì)列,一個(gè)Slave集合可用狀態(tài)隊(duì)列,一個(gè)待解析檢測(cè)結(jié)果隊(duì)列,在調(diào)度算法的調(diào)度下將任務(wù)從Master節(jié)點(diǎn)分發(fā)給Slave節(jié)點(diǎn),執(zhí)行結(jié)束后,再將產(chǎn)生的結(jié)果從Slave節(jié)點(diǎn)回傳給Master節(jié)點(diǎn),進(jìn)而實(shí)現(xiàn)了任務(wù)的并行執(zhí)行.具體說(shuō)來(lái),系統(tǒng)中Master節(jié)點(diǎn)負(fù)責(zé)對(duì)整個(gè)系統(tǒng)的管理,包括任務(wù)的分發(fā)與檢測(cè)結(jié)果的回收,對(duì)檢測(cè)結(jié)果的進(jìn)一步處理以及對(duì)Slave集合的管理等,Slave則只負(fù)責(zé)處理從Master接收到的任務(wù)并將檢測(cè)結(jié)果回傳給Master.

從平臺(tái)的具體實(shí)現(xiàn)上來(lái)說(shuō),其技術(shù)難點(diǎn)在于如何實(shí)現(xiàn)相應(yīng)的算法分別對(duì)待檢測(cè)任務(wù)隊(duì)列、Slave集合隊(duì)列及待處理檢測(cè)結(jié)果隊(duì)列的管理,如何提高平臺(tái)的健壯性及防止非授權(quán)操作等.本研究通過(guò)設(shè)置相應(yīng)的定時(shí)調(diào)度器、相應(yīng)的監(jiān)聽(tīng)器及相應(yīng)的授權(quán)攔截器的策略來(lái)應(yīng)對(duì)上述問(wèn)題.概括起來(lái),本研究共設(shè)置了三個(gè)定時(shí)調(diào)度器分別對(duì)應(yīng)管理Slave集合隊(duì)列、待檢測(cè)任務(wù)隊(duì)列及待處理檢測(cè)結(jié)果隊(duì)列,設(shè)置了一個(gè)監(jiān)聽(tīng)器用以提高平臺(tái)的健壯性,設(shè)置了一個(gè)授權(quán)攔截器以防止非授權(quán)操作,下面對(duì)其一一進(jìn)行介紹.

圖2　分布式符號(hào)執(zhí)行平臺(tái)系統(tǒng)架構(gòu)圖

(1)Slave集合隊(duì)列定時(shí)調(diào)度器用于周期性的獲取每個(gè)Slave的“心跳”.該調(diào)度器按照一定的時(shí)間間隔對(duì)整個(gè)Slave集合IP列表進(jìn)行掃描,根據(jù)IP地址向每個(gè)Slave發(fā)送一條消息,按照相應(yīng)的返回值更新該Slave的狀態(tài).

(2)待檢測(cè)任務(wù)隊(duì)列定時(shí)調(diào)度器的功能是調(diào)度分發(fā)任務(wù).該調(diào)度器也是按照一定的時(shí)間間隔掃描整個(gè)任務(wù)列表,并將狀態(tài)為“待檢測(cè)”的任務(wù)分發(fā)給一個(gè)空閑的Slave執(zhí)行.

(3)對(duì)于初步檢測(cè)結(jié)果,本研究所采取的策略是不立即進(jìn)行解析而是先將其放入對(duì)應(yīng)的隊(duì)列,等相應(yīng)的調(diào)度器觸發(fā)后統(tǒng)一進(jìn)行處理.因此,待處理檢測(cè)結(jié)果隊(duì)列定時(shí)調(diào)度器的作用是定時(shí)觸發(fā)相應(yīng)的算法對(duì)檢測(cè)結(jié)果進(jìn)行處理.

(4)為了提高平臺(tái)的健壯性,本研究在系統(tǒng)啟動(dòng)時(shí)配置了一個(gè)監(jiān)聽(tīng)器,該監(jiān)聽(tīng)器用于將處于異常狀態(tài)的任務(wù)或Slave重置為正常狀態(tài),比如系統(tǒng)重啟時(shí)發(fā)現(xiàn)某個(gè)任務(wù)的狀態(tài)是“正在執(zhí)行”狀態(tài),則應(yīng)將其置為“檢測(cè)失敗”狀態(tài).

出于安全性的考慮,本研究還設(shè)置了一個(gè)授權(quán)攔截器防止用戶(hù)直接通過(guò)URL訪(fǎng)問(wèn)平臺(tái)中的頁(yè)面.

2.2分布式符號(hào)執(zhí)行平臺(tái)實(shí)現(xiàn)

在平臺(tái)的具體實(shí)現(xiàn)過(guò)程中,本研究結(jié)合使用了多種技術(shù).其中,使用了開(kāi)源的符號(hào)執(zhí)行工具KLEE作為符號(hào)執(zhí)行器,使用了輕量級(jí)的struts + spring + hibernate作為Web框架,使用了SSH(Secure Shell)+SCP(Security Copy)技術(shù)負(fù)責(zé)Master與Slave之間的通信,使用了開(kāi)源的作業(yè)調(diào)度框架Quartz負(fù)責(zé)任務(wù)的調(diào)度,此外,還使用到了tcping、putty等軟件,整個(gè)系統(tǒng)使用JSP與Java語(yǔ)言完成.下面將分模塊對(duì)其實(shí)現(xiàn)進(jìn)行介紹.

客戶(hù)端瀏覽器.用戶(hù)通過(guò)其完成注冊(cè)、任務(wù)提交、任務(wù)修改及任務(wù)查詢(xún)等功能.本研究所開(kāi)發(fā)的平臺(tái)支持兩種方式的任務(wù)提交,分別為基于源代碼的單任務(wù)提交與基于字節(jié)碼的批量任務(wù)提交.本研究中符號(hào)執(zhí)行環(huán)境的初始化工作也是在這部分完成的,初始化界面如圖3所示.

如圖3所示,本研究在任務(wù)創(chuàng)建時(shí)可以指定符號(hào)執(zhí)行的搜索策略、建模使用到的外部函數(shù)庫(kù)、最大執(zhí)行時(shí)間以及符號(hào)化的參數(shù)個(gè)數(shù)及長(zhǎng)度等.

Master模塊又分為任務(wù)調(diào)度器模塊及交互管理兩大子模塊.任務(wù)調(diào)度器模塊負(fù)責(zé)界面展示及收集用戶(hù)請(qǐng)求,并將用戶(hù)提交的任務(wù)放入待檢測(cè)隊(duì)列,將返回的檢測(cè)結(jié)果進(jìn)一步處理后存入數(shù)據(jù)庫(kù).交互管理模塊負(fù)責(zé)對(duì)Slave集群與Job隊(duì)列的管理.它通過(guò)Slave Manager子模塊負(fù)責(zé)對(duì)Slave的添加、刪除及狀態(tài)的查詢(xún),通過(guò)Job Manager子模塊負(fù)責(zé)從待檢測(cè)隊(duì)列取出任務(wù)并根據(jù)從Slave Manager獲得的Slave集合的忙閑狀態(tài)將任務(wù)分發(fā)下去.該模塊使用到了三個(gè)核心調(diào)度器,分別為Slave集合隊(duì)列定時(shí)調(diào)度器、待檢測(cè)任務(wù)隊(duì)列定時(shí)調(diào)度器以及待處理檢測(cè)結(jié)果隊(duì)列定時(shí)調(diào)度器.其中,Slave集合隊(duì)列定時(shí)調(diào)度器對(duì)應(yīng)平臺(tái)的Slave Manager模塊,它使用tcping工具定時(shí)的對(duì)Slave節(jié)點(diǎn)中部署的SSH服務(wù)端口進(jìn)行探測(cè),完成Master節(jié)點(diǎn)對(duì)Slave節(jié)點(diǎn)的監(jiān)控管理; 待檢測(cè)任務(wù)隊(duì)列定時(shí)調(diào)度器與待處理檢測(cè)結(jié)果隊(duì)列定時(shí)調(diào)度器則均使用Quartz框架的作業(yè)調(diào)度功能來(lái)完成任務(wù)的定時(shí)分發(fā)(通過(guò)putty工具的pscp功能)與檢測(cè)結(jié)果的定時(shí)處理,它們分別對(duì)應(yīng)平臺(tái)中的Job Manager模塊與檢測(cè)報(bào)告處理模塊.三個(gè)核心調(diào)度器的處理過(guò)程如圖4所示.

圖3　符號(hào)執(zhí)行環(huán)境初始化界面圖

圖4　核心調(diào)度器處理過(guò)程圖

檢測(cè)模塊.該模塊由多個(gè)Slave組成的集合,其中每個(gè)Slave均配置了KLEE執(zhí)行環(huán)境,負(fù)責(zé)將接收到的任務(wù)進(jìn)行檢測(cè)并將檢測(cè)結(jié)果返回.這里用到了putty工具的plink功能與pscp功能.

3　實(shí)驗(yàn)與分析

本研究中KLEE的執(zhí)行環(huán)境部署在了Ubuntu 14.04 64位的系統(tǒng)中,作為一個(gè)Slave節(jié)點(diǎn).基于此,本研究以虛擬機(jī)的形式在開(kāi)源的云計(jì)算平臺(tái)CloudStack上創(chuàng)建了120個(gè)Slave節(jié)點(diǎn),每個(gè)節(jié)點(diǎn)均分配了2GHZ的處理器資源及2GB 的RAM資源,Web服務(wù)器即Master節(jié)點(diǎn)則又單獨(dú)為其在CloudStack創(chuàng)建了一個(gè)節(jié)點(diǎn),該節(jié)點(diǎn)具有16核共16GHZ的處理器資源及32GB的RAM資源.

3.1分布式符號(hào)執(zhí)行平臺(tái)分析效率評(píng)價(jià)

為了對(duì)平臺(tái)所能帶來(lái)的分析效率的提升進(jìn)行評(píng)價(jià),本研究對(duì)比分析了四組實(shí)驗(yàn).四組實(shí)驗(yàn)分別選取5、10、20、30個(gè)程序作為四批任務(wù)分別使用本研究實(shí)現(xiàn)的平臺(tái)與單個(gè)節(jié)點(diǎn)進(jìn)行處理,結(jié)束后統(tǒng)計(jì)執(zhí)行時(shí)間.對(duì)于本研究的平臺(tái),由于各批任務(wù)中的程序是并行執(zhí)行的,因此我們選取了每批任務(wù)中執(zhí)行時(shí)間最長(zhǎng)的程序作為基準(zhǔn),取其執(zhí)行時(shí)間為相應(yīng)組的執(zhí)行時(shí)間 .對(duì)于單節(jié)點(diǎn),我們則選取了每批任務(wù)的總執(zhí)行時(shí)間作為其執(zhí)行時(shí)間.同時(shí),作為對(duì)比分析之用,我們還定義了理想情況下平臺(tái)的執(zhí)行時(shí)間,該時(shí)間是以單節(jié)點(diǎn)執(zhí)行每批任務(wù)的總時(shí)間為基礎(chǔ)的,將其定義為該批任務(wù)中每個(gè)程序的平均執(zhí)行時(shí)間,即用執(zhí)行總時(shí)間除以程序個(gè)數(shù).使用分布式符號(hào)執(zhí)行平臺(tái)并行處理各批任務(wù)與使用單節(jié)點(diǎn)串行處理各批任務(wù)所用時(shí)間的對(duì)照如圖5所示.

圖5　各批任務(wù)執(zhí)行時(shí)間圖

如圖5所示,橫坐標(biāo)對(duì)應(yīng)的是實(shí)驗(yàn)組別,縱坐標(biāo)對(duì)應(yīng)的是執(zhí)行時(shí)間,實(shí)線(xiàn)對(duì)應(yīng)的是使用本研究的平臺(tái)并行處理各批任務(wù)所用時(shí)間,虛線(xiàn)對(duì)應(yīng)的是使用單節(jié)點(diǎn)順序處理各批任務(wù)所用時(shí)間,間斷的虛線(xiàn)對(duì)應(yīng)的是平臺(tái)理想情況下的執(zhí)行時(shí)間.可以看出我們的平臺(tái)可以在很大程度上提升程序的分析效率,但與理想情況還有一定的差距,主要原因是,一方面我們選取了各批任務(wù)中執(zhí)行時(shí)間最長(zhǎng)的程序作為基準(zhǔn),將其執(zhí)行時(shí)間作為平臺(tái)的執(zhí)行時(shí)間,另一方面,使用平臺(tái)進(jìn)行任務(wù)處理時(shí)與單節(jié)點(diǎn)或理想情況相比,還要考慮其他方面的時(shí)間開(kāi)銷(xiāo).因此,圖5只能在一定程度上反映出平臺(tái)分析效率的提升程度.為了更全面的對(duì)平臺(tái)所能帶來(lái)的分析效率的提升進(jìn)行評(píng)價(jià),本研究在下文討論了理想情況下平臺(tái)分析效率提升的上限值.

設(shè)節(jié)點(diǎn)數(shù)為N,任務(wù)總數(shù)為n,每個(gè)任務(wù)的平均分析時(shí)間為t,使用本研究開(kāi)發(fā)的分布式平臺(tái)進(jìn)行分析所花費(fèi)的總時(shí)間為T(mén)ds,使用單個(gè)節(jié)點(diǎn)依次對(duì)測(cè)試對(duì)象進(jìn)行分析所花費(fèi)的總時(shí)間為T(mén)s,則

相應(yīng)的

將R定義為使用本研究的平臺(tái)相對(duì)于使用單個(gè)節(jié)點(diǎn)進(jìn)行分析所帶來(lái)的效率提升的倍數(shù),則由(1)與(2)得

公式(3)反映出使用本研究的平臺(tái)可以大幅度提升程序的分析效率,當(dāng)然,這種分析效率的提升是以增加硬件的花費(fèi)為代價(jià)換來(lái)的,是一種以空間換時(shí)間的策略.顯然,實(shí)際情況下公式(3)是很難成立的,其中一部分原因我們?cè)谇懊嬉呀?jīng)討論過(guò),還有一部分原因是在實(shí)際測(cè)試中可能會(huì)出現(xiàn)因參數(shù)設(shè)置不當(dāng)如執(zhí)行時(shí)間過(guò)長(zhǎng)或其他原因?qū)е履承┤蝿?wù)執(zhí)行失敗的情況.針對(duì)這種情況,有時(shí)我們就需要將失敗的任務(wù)提取出來(lái)重新打包成一批新的任務(wù)調(diào)整參數(shù)后再次進(jìn)行檢測(cè),這也會(huì)影響到平臺(tái)的分析效率.

3.2分布式符號(hào)執(zhí)行平臺(tái)案例分析

本研究考慮到平臺(tái)提供了兩種任務(wù)提交方式的特點(diǎn),分別從基于源代碼的單任務(wù)提交方式與基于LLVM字節(jié)碼的批量任務(wù)提交方式兩部分進(jìn)行了實(shí)驗(yàn)方案的設(shè)計(jì),從平臺(tái)的實(shí)用性、易用性、界面友好性及實(shí)際發(fā)現(xiàn)軟件缺陷的能力等方面對(duì)其進(jìn)行評(píng)價(jià).

3.2.1基于源代碼的單任務(wù)提交方式案例分析

為了對(duì)平臺(tái)的實(shí)用性、易用性及界面友好性做出評(píng)價(jià),本文選取了coreutils-6.10中的paste程序作為實(shí)驗(yàn)對(duì)象進(jìn)行分析,該程序的C代碼行數(shù)共有496行.如前所述,本研究中KLEE執(zhí)行環(huán)境的初始化是在任務(wù)提交時(shí)進(jìn)行的,這一過(guò)程通過(guò)平臺(tái)的可視化界面來(lái)做是一件很方便的事情,這特別適用于對(duì)KLEE不是很熟悉的研究者,當(dāng)然,對(duì)于專(zhuān)業(yè)人員來(lái)說(shuō)這樣做也可以節(jié)省時(shí)間,從這點(diǎn)來(lái)說(shuō),本研究所開(kāi)發(fā)的平臺(tái)具有較好的實(shí)用性與易用性.

將KLEE的最大執(zhí)行時(shí)間設(shè)置為15分鐘,符號(hào)化參數(shù)個(gè)數(shù)設(shè)置為0到3個(gè)且最大長(zhǎng)度為10的情況下進(jìn)行分析,執(zhí)行結(jié)束后平臺(tái)共報(bào)出了10個(gè)與內(nèi)存相關(guān)的錯(cuò)誤,檢測(cè)結(jié)果頁(yè)面如圖6所示.

圖6　檢測(cè)結(jié)果頁(yè)面圖

圖6所示的是任務(wù)執(zhí)行結(jié)束后檢測(cè)結(jié)果的詳細(xì)情況,其中,上半部分顯示出了任務(wù)執(zhí)行結(jié)束后的統(tǒng)計(jì)信息,包括指令數(shù)、指令覆蓋率、分支覆蓋率、代碼覆蓋率及執(zhí)行時(shí)間等信息,可以看到,該任務(wù)的代碼覆蓋率達(dá)到了90.66%.下半部分則對(duì)應(yīng)的是錯(cuò)誤的具體情況,包括錯(cuò)誤類(lèi)型、錯(cuò)誤級(jí)別、錯(cuò)誤內(nèi)容、錯(cuò)誤所在文件以及錯(cuò)誤行號(hào).本研究所開(kāi)發(fā)的平臺(tái)經(jīng)過(guò)對(duì)檢測(cè)結(jié)果的解析與封裝,以相當(dāng)友好的可視化界面將檢測(cè)結(jié)果呈現(xiàn)了出來(lái),這為我們后續(xù)更大規(guī)模的分析程序提供了方便.

3.2.2基于字節(jié)碼的批量任務(wù)提交方式案例分析

同樣的,為了對(duì)平臺(tái)實(shí)際發(fā)現(xiàn)軟件缺陷的能力做出評(píng)價(jià),本研究選取了40個(gè)測(cè)試包共計(jì)575個(gè)字節(jié)碼文件超過(guò)2000K的C代碼進(jìn)行了分析,其中,每個(gè)字節(jié)碼文件作為一個(gè)任務(wù),共有575個(gè)任務(wù).

將初始分析參數(shù)設(shè)置為最大執(zhí)行時(shí)間1小時(shí),符號(hào)化參數(shù)個(gè)數(shù)從0到3且最大長(zhǎng)度為10的情況下,檢測(cè)結(jié)果如表1所示.

表1　測(cè)試包及發(fā)現(xiàn)缺陷數(shù)

如上表所示,通過(guò)對(duì)超過(guò)2000K的C代碼進(jìn)行檢測(cè),本研究共發(fā)現(xiàn)了56個(gè)錯(cuò)誤.

4　結(jié)語(yǔ)

本研究在開(kāi)源的符號(hào)執(zhí)行工具KLEE的基礎(chǔ)上實(shí)現(xiàn)了一個(gè)B/S結(jié)構(gòu)的分布式符號(hào)執(zhí)行平臺(tái).該平臺(tái)通過(guò)設(shè)置一個(gè)待檢測(cè)隊(duì)列,在調(diào)度算法的調(diào)度下將任務(wù)從主節(jié)點(diǎn)分發(fā)給工作節(jié)點(diǎn),進(jìn)而實(shí)現(xiàn)了任務(wù)的并行執(zhí)行,降低了符號(hào)執(zhí)行的時(shí)間開(kāi)銷(xiāo).基于該平臺(tái),首先,我們通過(guò)四組對(duì)比試驗(yàn)對(duì)平臺(tái)的分析效率進(jìn)行了評(píng)價(jià),然后,我們又對(duì)40個(gè)程序包超過(guò)2000K行的C代碼進(jìn)行了分析,共檢測(cè)出了56個(gè)程序缺陷,通過(guò)以空間換時(shí)間的方式,我們的分布式平臺(tái)大幅度的提高了程序的分析效率.

參考文獻(xiàn)

1 Schwartz EJ,Avgerinos T,Brumley D.All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask).2010 IEEE Symposium on Security and Privacy (SP).IEEE.2010.

2Tillmann N,De Halleux J.Pex-white box test generation for .NET.Tests and Proofs,2008: 134–153.

3Cadar C,Dunbar D,Engler DR.KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs.Symp.on Operating Systems Design and Implementation,2008.

4董齊興.基于動(dòng)態(tài)符號(hào)執(zhí)行的測(cè)試用例生成技術(shù)研究[碩士學(xué)位論文].合肥:中國(guó)科技大學(xué),2014.

5婁堅(jiān)波.面向宿主的嵌入式軟件符號(hào)執(zhí)行技術(shù)研究與實(shí)現(xiàn)[碩士學(xué)位論文].南京:南京航空航天大學(xué),2011.

6Enderton H.A Mathematical Introduction to Logic,second edition.Academic Press,2001.

7張羽豐.符號(hào)執(zhí)行可擴(kuò)展性及可行性關(guān)鍵技術(shù)研究[博士學(xué)位論文].長(zhǎng)沙:國(guó)防科學(xué)技術(shù)大學(xué),2013.

8Staats M,Pasareanu C.Parallel symbolic execution for structural test generation.ISSTA’10.Trento,Italy.July 12-16,2010.

9Armbrust M,Fox A,Griffith R,et al.A view of cloud computing.Communications of the ACM,2010,53(4): 50-58.

10Bucur S,Ureche V,Zamfir C,Candea G.Parallel symbolic execution for automated real-world software testing.Reprinted from EuroSys’11,Proc.of the 6th ACM SIGOPS/EuroSys Conference on Computer Systems.Salzburg,Austria.April 10-13,2011.1–15.

11Avgerinos T,Rebert A,Cha SK,Brumley D.Enhancing symbolic execution with veritesting.ICSE’14.Hyderabad,India.May 31-June 7,2014.

Distributed Symbolic Execution Platform

SUN Pan-Pan,DONG Wei
(School of Computer,National University of Defense Technology,Changsha 410073,China)

Abstract:In software engineering,symbolic execution technology is an efficient program defect detection technology.Symbolic execution uses symbolic values as the inputs,which transforms the execution of the program into the corresponding symbolic expressions,and the precise analysis of the program behaviors is realized by systematacially traversing routing space.However,due to the restriction of the path explosion and constraint solving problems,symbolic execution technology has poor scalability.In order to mitigate the problem,this paper implemented a distributed symbolic execution platform which realized tasks parallelly execute and reduced the symbolic execution time overhead through a scheduling algorithm distributes tasks from master to slaves.

Key words:parallel symbolic execution; distributed system; WEB platform; defect detection; KLEE

基金項(xiàng)目:①?lài)?guó)家自然科學(xué)基金(91118007)

收稿時(shí)間:2015-08-09;收到修改稿時(shí)間:2015-09-17