孫盼盼,董威(國防科技大學 計算機學院,長沙 410073)

?

分布式符號執(zhí)行平臺①

孫盼盼,董威
(國防科技大學 計算機學院,長沙 410073)

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

關鍵詞:并行符號執(zhí)行; 分布式系統(tǒng); WEB平臺; 缺陷檢測; KLEE

1　引言

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

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

圖1　符號執(zhí)行系統(tǒng)整體結構圖

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

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

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

2　分布式符號執(zhí)行平的設計與實現(xiàn)

2.1分布式符號執(zhí)行平臺架構與功能

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

從平臺的具體實現(xiàn)上來說,其技術難點在于如何實現(xiàn)相應的算法分別對待檢測任務隊列、Slave集合隊列及待處理檢測結果隊列的管理,如何提高平臺的健壯性及防止非授權操作等.本研究通過設置相應的定時調度器、相應的監(jiān)聽器及相應的授權攔截器的策略來應對上述問題.概括起來,本研究共設置了三個定時調度器分別對應管理Slave集合隊列、待檢測任務隊列及待處理檢測結果隊列,設置了一個監(jiān)聽器用以提高平臺的健壯性,設置了一個授權攔截器以防止非授權操作,下面對其一一進行介紹.

圖2　分布式符號執(zhí)行平臺系統(tǒng)架構圖

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

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

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

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

出于安全性的考慮,本研究還設置了一個授權攔截器防止用戶直接通過URL訪問平臺中的頁面.

2.2分布式符號執(zhí)行平臺實現(xiàn)

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

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

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

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

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

圖4　核心調度器處理過程圖

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

3　實驗與分析

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

3.1分布式符號執(zhí)行平臺分析效率評價

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

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

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

設節(jié)點數(shù)為N,任務總數(shù)為n,每個任務的平均分析時間為t,使用本研究開發(fā)的分布式平臺進行分析所花費的總時間為Tds,使用單個節(jié)點依次對測試對象進行分析所花費的總時間為Ts,則

相應的

將R定義為使用本研究的平臺相對于使用單個節(jié)點進行分析所帶來的效率提升的倍數(shù),則由(1)與(2)得

公式(3)反映出使用本研究的平臺可以大幅度提升程序的分析效率,當然,這種分析效率的提升是以增加硬件的花費為代價換來的,是一種以空間換時間的策略.顯然,實際情況下公式(3)是很難成立的,其中一部分原因我們在前面已經討論過,還有一部分原因是在實際測試中可能會出現(xiàn)因參數(shù)設置不當如執(zhí)行時間過長或其他原因導致某些任務執(zhí)行失敗的情況.針對這種情況,有時我們就需要將失敗的任務提取出來重新打包成一批新的任務調整參數(shù)后再次進行檢測,這也會影響到平臺的分析效率.

3.2分布式符號執(zhí)行平臺案例分析

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

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

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

將KLEE的最大執(zhí)行時間設置為15分鐘,符號化參數(shù)個數(shù)設置為0到3個且最大長度為10的情況下進行分析,執(zhí)行結束后平臺共報出了10個與內存相關的錯誤,檢測結果頁面如圖6所示.

圖6　檢測結果頁面圖

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

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

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

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

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

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

4　結語

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

參考文獻

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董齊興.基于動態(tài)符號執(zhí)行的測試用例生成技術研究[碩士學位論文].合肥:中國科技大學,2014.

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

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

7張羽豐.符號執(zhí)行可擴展性及可行性關鍵技術研究[博士學位論文].長沙:國防科學技術大學,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

基金項目:①國家自然科學基金(91118007)

收稿時間:2015-08-09;收到修改稿時間:2015-09-17