一種基于Actor模型的并行動態符號執行方法

張曉文,賈向陽,常 亮,劉錢超,胡小輝

1(桂林電子科技大學 廣西可信軟件重點實驗室,廣西 桂林 541004) 2(武漢大學 軟件工程國家重點實驗室,武漢 430000)

1 引 言

符號執行技術是一種經典的程序分析技術.它使用符號值來代替具體的值來模擬執行程序,系統化地探索程序的可行的路徑,從而來發現難以發現的缺陷,以及為各個路徑生成測試用例[1-3].動態符號執行技術(如Concolic Testing[9-13]和Dart[5,8])在符號執行中引入了具體值,利用具體值執行程序,記錄程序中的符號值和各個分支的路徑條件(Path Condition).在一條路徑執行完成后,通過對其它分支的路徑條件進行約束求解,來生成針對新路徑的程序輸入,引導下一次執行.

動態符號執行相對靜態符號執行具有更高的效率,因此在目前得到了更廣泛的應用.然而,由于動態符號執行同樣需要探索大量的路徑,并進行耗時的約束求解,因此對于稍大規模的程序,效率往往難如人意[4].

將符號執行中耗時的工作并行化是提高效率的有效手段.目前國內外也有一些此類的探索工作[6,7].然而,符號執行的并行優化仍然面臨著一些挑戰性的問題:

1)任務的動態迭代式產生問題:在動態符號執行中,路徑探索和約束求解這些耗時的工作是動態迭代式產生的:每求解路徑條件并探索完一條路徑后,都會產生一組新路徑需要進行約束求解和路徑探索.這種動態迭代式的任務,很難通過靜態任務分配方式來實現并行化.

2)大規模任務的通信代價問題:動態符號執行中路徑探索和約束求解的任務數據巨大,單個任務則一般執行時間并不長.這種大規模的小任務對任務調度的通信代價具有很高的敏感性.

本文針對上述問題,提出了一種基于Actor并行模型的動態符號執行并行優化方法.該方法將符號執行中的任務按照符號執行樹的子樹方式分配到多個獨立運行的Actor工作節點中.各個Actor工作節點負責對該子樹的路徑條件進行求解,對可行路徑進行探索.每條路徑探索完然后發現新路徑時,將新增加的路徑數目通知調度中心.調度中心監控各個節點的路徑數目,如果某個節點處于空閑狀態時,則從最多路徑的節點“拆借”一個子樹分配給該節點,從而實現了任務的動態負載均衡.工作節點向調度中心發送路徑數時采用異步方式,并且數據量很小,通信代價基本可以忽略.由于各個工作節點只探索相對獨立的路徑子樹,基本兼容了之前的符號執行工作模式,因此已有的優化機制仍然可以很方便地整合使用.

2 基于Actor模型的并行符號執行方法

2.1 Actor模型

Actor模型是一種經典的并行計算模型,在Actor模型中,Actor是一種可以響應外部消息的計算實體[19].異步消息是Actor之間唯一的通信方式.Actor模型中各個Actor可以并行執行計算任務,但各個Actor又相互獨立運行,沒有鎖機制等依賴關系.

Actor模型等這些特點非常符合并行符號執行的特定需求.各個并行計算節點做為Actor可以不依賴其他節點、相對獨立地執行局部任務.而異步消息保證了通信不會影響本節點的計算工作.

2.2 方法概述

總體框架設計如圖1所示,由Master和多個Worker組成.方法使用了兩種類型的Actor:MasterActor和WorkerActor.主要功能是:

1)MasterActor:負責負載均衡和任務分配.該部分維護一個負載表,記錄每個Worker發送來的負載消息.任務中心會根據負載表判斷是否需要啟動負載均衡工作(負載值超過負載表中任務的負載最大值),若需要則會給負載大的Worker節點發送任務轉移消息,收到相應消息后會將任務發送給給空閑的工作節點,以此實現多個節點的任務均衡分配.

2)WorkerActor:負責對程序某個特定的路徑子樹進行符號執行.節點維護一個維護待求解路徑棧和一個待探索路徑棧.該部分實現了worker內部約束求解和路徑探索的并行工作:worker節點響應MasterActor提供的任務,放入待求解路徑棧中,約束求解器從棧中讀取任務,進行求解,求解后的路徑放入待探索路徑棧中.路徑探索模塊從待探索路徑棧中讀取路徑進行探索,探索完成后,又會產生新的一組路徑,放入待求解路徑棧中.依次迭代直到所有的路徑都探索完成,或者找到滿足目標的路徑.

工作節點在每次路徑探索結束后,會將當前的兩個棧中的任務數作為結點的負載發給MasterActor.而MasterActor如果需要負載均衡的時候,忙節點的WorkerActor會將當前未探索的子樹轉移到空閑節點上,來實現負載均衡.

2.3 基于子樹轉移的動態負載均衡方法

由于在動態符號執行中,待探索的路徑是動態迭代式產生的,因此很難準確評估各個節點的負載,從而實現精確的負載均衡.本文中采取了動態負載均衡方法,只有存在空閑節點時,才從繁忙的節點處拆借任務到空閑節點上.這樣保證各個節點都處于工作狀態,達到一定程度上的負載均衡.

在本文中,節點的負載表示為待求解路徑棧和待探索路徑棧中的總路徑數目.每一條路徑探索完成后,可能會產生新路徑,放入待求解路徑棧中,從而使節點的負載發生變化.這時,工作節點會將新的負載發送到Master節點.當子樹的最后一條路徑探索完成,沒有新路徑產生時,節點的負載變為0.

當負載為0的節點出現后,Master節點會啟動負載均衡,查找負載最大的節點,進行路徑轉移.為了避免分析后期階段少量任務的多次轉移.我們為節點設置了一個最少負載,只有超過這個最少負載的節點才會拆借出子樹給空閑節點.

在工作節點中,取待求解路徑棧和待探索路徑棧中的路徑實際上代表了一個未展開的子樹.在進行子樹轉移時,實際上就是取路徑棧中的某個路徑轉移給其他節點.然而,具體選擇哪個子樹進行轉移,需要根據分析的目標和算法,設定不同的策略來確定.例如,為了避免轉移了過小子樹造成過于頻繁的負載均衡,我們可以取待求解路徑棧中長度最短的路徑進行轉移.在深度優先搜索中,長度最短路徑就是棧底的路徑.或者,為了在啟發式搜索中更快地找到目標,我們可以將接近棧頂的路徑進行轉移,因為這些路徑找到目標的可能性較大.

圖2 子樹轉移Fig.2 Subtree shifting

如圖2所示,當左邊節點需要轉移任務到右邊節點時.由于路徑樹中A是根節點,A的左子樹正在探索,而右子樹(節點B是根節點)是未探索的子樹.該節點代表的路徑目前存放在待求解路徑棧中.于是B開始的子樹將被轉移到右邊的空閑節點上,進行約束求解和生成待探索路徑.轉移后,左節點將不再探索B節點代表的子樹.

空閑節點會出現在兩個時間點:

1)并行符號執行剛最開始啟動時,路徑樹的根節點被分配給一個工作節點進行分析,其他節點處于空閑狀態.

2)某個節點分析的子樹的所有路徑都探索完成時,當前節點的負載為0,稱為空閑節點.

2.4 路徑探索與約束求解的并行

原始符號執行是路徑探索和約束求解分別執行,當程序執行時將所有的待求解的路徑探索出來,然后使用約束求解器將探索路徑進行求解,但是這樣的模式對于大規模程序而言,耗時較長,嚴重浪費系統資源.針對上述問題,提出路徑探索和約束求解并行執行,這樣可以節省程序執行時間.

圖3 并行路徑探索與約束求解Fig.3 Parallel path exploration and constraint solving

如圖3所示，包含兩個棧:待求解路徑棧和待探索路徑棧;節點A為路徑的根節點;節點B為未展開節點;P1、P2等是待求解路徑棧;P7、P8等是待探索路徑棧;并行路徑探索和約束求解是通過該棧相互操作,實現任務的并行操作.當執行路徑操作時,首先將待求解的路徑存入待求解路徑棧,空閑節點從該棧中取相應任務,然后通過約束求解器Z3將待求解路徑進行求解操作,同時生成待探索路徑,存入待探索路徑棧,進行路徑探索,探索完成后,產生的新路徑又會存放到待求解任務棧中,這樣遞歸完成對所有路徑的探索和求解.待探索任務棧中會不停的存和取任務,而待探索任務棧會根據求解結果存放路徑,這樣,可以并行完成任務操作.

3 實驗與評估

我們基于動態符號執行工具Jdart和Jdart Actor框架,實現了一個并行動態符號執行原型工具Jdart-parallel.我們將Jdart-parallel較原來Jdart符號執行效率進行對比,來評估本文方法的有效性.同時,對Jdart-parallel符號執行工具在不同節點數下的執行效率進行了評估,分析并行的規模對效率的作用效果.

3.1 實驗環境

本實驗主要是使用6個計算機節點操作,每一個節點的配置如下:Dell臺式電腦、Intel Core i7-4790、CPU:3.6GHz、8GB RAM 、Windows 操作系統、Sun JRE 1.8 (64-bit mode)、Eclipse(64-bit mode)、Ant 1.9.

實驗中待測試的程序包括:

1)Euclid:計算兩個整數之間的差值;

2)WBS:使用整數和布爾類型輸入來進行更新操作;

3)ArraysCh6、ArraysCh7、ArraysCh8、ArraysCh9、ArraysCh10、ArraysCh11:對數組進行的基本操作,其中程序名稱后面的6、7、8、9、10、11代表執行程序的參數的個數;

4)Double2Long:將雙精度類型數據轉換成長整形;CEV4、CEV5、CEV6、CEV7、CEV8、CEV9、CEV10:計算方差,其中程序名稱后面的4、5、6、7、8、9、10代表程序的執行個數.

3.2 實驗結果分析

實驗1.與JDart的對比分析

如表1,總的路徑數目對于不同數目節點是相同的,單節點的 JDart(動態符號執行)其執行時間相比于其它節點明顯長許多.如ArrayCh9,JDart的執行時間是1266323ms,而并行框架不同節點的運行時間相比其是大幅度減少:2節點運行時間20607ms,3節點運行時間為10734ms,如此,隨著節點數目的增加,程序執行時間在逐漸的縮短.相比JDart,2節點的執行時間相比單節點節省了將近62倍,節點規模的不斷擴大,該數字也在不斷增長.

表1 與單節點符號執行(Jdart)的運行時間對比
Table 1 Comparison run time with single node

程序名稱路徑數不同數目節點運行時間/ms單節點Jdart2節點3節點4節點5節點6節點Euclid5015338010481048104810481048WBS13824615350414238397129892799ArraysCh615625906763786061582350424969ArraysCh77812553998100326702597347024523ArraysCh8390625245512150609928822567274515ArraysCh9195312512663232060710734944477086500ArraysCh10#?25963138271030698458625ArraysCh11#?321191622011551102169009CEV465611094385476305504537032400CEV559049140876104768905603149123809CEV653144114065821563210248809565204325CEV7#?20449132211008587476645CEV8#?24082160471292397457566CEV9#?30566241941319498588656CEV10#?355792016911481108719658Double2Long400303310081008100810081008?：代表運行時間長于1h，#：代表路徑條數大于200萬條

從表1可以看出,JDart的執行效率相比于Jdart-parallel有明顯的差距,Jdart-parallel的執行效率明顯優于JDart.隨著節點數目的增加,Jdart-parallel的執行效率在不斷的提高,從本質上證明了Jdart-parallel并行符號執行的優勢.

實驗2.節點規模對符號執行的性能影響

從實驗中可以看出,隨著節點數目的不斷增加,程序的執行效率在明顯提升,并且隨著節點數目的逐漸增多,程序的執行效率越高,能更好的體現出并行符號執行的優勢.此外,隨著節點數目的增加,程序的執行時間在逐漸的縮短,從執行時間上可以對比分析出并行符號執行的優勢,具體影響如下圖標所示:

本實驗主要對照的是節點數目對實驗的影響,擬使用6個實驗節點來檢測,檢測每個節點具體運行對實驗結果的影響,然后對比最初始的程序運行時間,對比判斷出隨著節點數目的增多,實驗結果的最終變化,以此來預測節點規模對實驗的影響.

圖4 不同節點規模下的符號執行運行時間Fig.4 Symbolic Execution Runtime at Different Node Scales

圖4描述了在Jdart-parallel執行工具下,對于待測程序,在不同工作節點下的執行時間,其中對每一個待測程序而言,從左到右節點數目在逐漸的增加.從圖中可以看出,對于每一個待測程序,隨著節點數目的增加,執行時間在逐漸的縮短,對于程序Double2Long和Euclid,由于程序結構比較簡單、規模較小,所以在執行的過程中只用到了其中某一個節點,因此執行時間基本上是相同的.

圖4橫軸表示待測程序的名稱,縱軸表示待測程序的執行時間,柱狀圖的高度表示程序的具體執行時間,不同的顏色代表不同的節點數目執行待測程序的時間,圖中可以看出:隨著節點數目的增加,執行相同待測程序的時間在減少.

圖5和圖6描述了待測程序CEV、Arrays和其變化程序在不同節點下的運行時間.從圖中可以看出,隨著節點數目的不斷增加,每個待測程序的執行時間在逐漸的減少,說明了并行符號執行的執行效率隨著節點數目的增加在提升,同時執行程序的規模隨著節點數目的增加在增大.

圖7描述了在并行框架下,部分程序的加速比(加速比=單節點/n節點,其中n:2,3,4,5,6),隨著節點數目的逐漸增加,加速比在逐漸的提升,程序的運行效率在逐漸提升,其中程序Euclid和Double2Long由于程序規模較小,只使用一個節點,所以加速比沒變化.

實驗分析:

執行時間:隨著程序規模逐漸增加,Jdart(單節點)的執行時間在逐漸增加,但是Jdart-parallel的執行時間相比Jdart執行時間明顯減少.Jdart執行時間比并行時間多,如表1中單節點和2 節點最為明顯,原因是Jdart的執行沒使用到多核技術,執行的過程中隨著內存的逐漸消耗程序會出現卡頓等現象,卡頓期間的時間消耗比較高.并行執行時每個節點都使用較小的路徑樹,占用資源較少,減輕了卡頓現象.

圖5 CVE在不同節點下運行時間Fig.5 CVE run time at different nodes

圖6 Arrays在不同節點下運行時間Fig.6 Arrays run time at different nodes

圖7 加速比Fig.7 Speedup ratio

執行大規模程序能力:隨著程序規模的逐漸增加,Jdart-parallel隨著節點數目的增加,程序的執行效率在不斷的增強,體現了Jdart-parallel執行大規模程序的能力.

從上述的實驗結果可以看出,Jdart-parallel并行符號執行在執行程序方面的優勢:首先并行符號執行在執行程序的過程中相比于非并行執行時間明顯縮短;其次是隨著節點數目的不斷增多,執行相同的程序,并行方式明顯比非并行執行能力強;隨著程序規模的逐漸增加,并行符號執行執行時間比非并行節省許多,說明了并行符號執行可以執行較大規模程序的能力.

與動態符號執行相比,并行動態符號執行使用多個節點,在多節點上分別執行路徑探索任務.由以上實驗結果可以看出,并行動態符號執行工具相比于原來的動態符號執行工具而言測試相同的程序能有效地縮短執行時間,并行符號執行使用多個節點測試相應程序比原始動態符號執行測試相同的程序提高時間效率,同時加速比在逐漸增加(加速比=單節點/n節點,其中n:2,3,4,5,6),實驗結果證明并行動態符號執行工具Jdart-parallel在提高符號執行效率方面具有良好的效果.

4 相關工作

為了解決并行符號執中面臨的效率問題,學術界提出了一些基于并行技術的優化方法.

ParSym[14]是一種并行動態符號執行,通過一個Symbolic Execution Monitor對整個符號執行進行控制和任務分配,符號執行中的每條路徑被當作一個獨立的任務.在符號執行中產生的新任務被動態地分配到各個節點進行執行.ParSym采用了集中式的任務調度方法,涉及到較多的任務分配和回收等操作,當路徑比較龐大時會耗費較多的通信代價.

靜態分區技術[15]使用一系列的前置條件來對符號執行樹進行分區,這樣做的目的是允許我們可以高效的分布執行符號執行,減少搜索的時間,它們在執行的過程中每一個并行實例執行各自的運行框架,相互之間很少有交互,節省時間,但是使用這些先決條件可能使得不同的節點搜索相同的路徑,搜索的重復率較高,浪費時間,同時靜態分區不能實現節點之間的負載均衡.

Cloud9[16,17]是第一個使用大規模集群的符號執行系統可以線性的擴展許多的節點,是一個請求式的測試軟件,它主要的功能結構包括工作節點和負載均衡器,主要依賴均衡器來分配相應的搜索任務,并把搜索進行并行化操作,它可以自動化的測試現實世界中的軟件,節省了很多時間.Cloud9提供了一個系統的寫符號測試的接口,只需要輸入測試數據和測試行為,可以提升測試的效率.Cloud9有許多自身的優勢:不僅可以處理單線程的程序,還可以處理多線程的程序和分布式系統,在多路徑、多任務同時進行時,Cloud9通過均衡器來實現對于負載的均衡.但是Cloud9在執行的過程中需要維護整棵符號執行樹,路徑搜索消耗大量多余時間.而本文需要維護的只是個子樹,節省了存儲空間和搜索時間.此外,Cloud9是針對經典的符號執行工具而非動態符號執行,在任務的產生和分配機制上與本文是不同的.

Quoc-Sang Phan等人提出了一種Concurrent Bounded Model Checking(CBMC)方法[18].該方法基于經典的符號執行工具Symbolic PathFinder進行并行的模型檢測.它首先通過路徑探索,搜索到特定路徑的所有可行路徑,然后將這些路徑進行合并成一個大的約束進行求解.求解時采用并行技術,將各條路徑的約束分配到多個節點進行求解.該方法只針對的是模型檢測的應用場景,只對約束求解過程進行并行,與本文的動態符號執行在應用場景和并行模式上是不同的.

5 總 結

本文基于Actor并行模型,提出了一種并行動態符號執行方法,它實現了兩個層面上的并行.首先可以在多個節點上并行分析程序的路徑子樹,并通過子樹轉移實現動態的負載均衡.另一方面在節點內部,將約束求解和路徑探索兩項耗時的工作并行,來進一步提高效率.

通過原型工具Jdart-parallel做的相關對比試驗結果表明,相比于原來的動態符號執行工具,測試相同的程序,能在時間效率上得到很大提升,證明了并行化符號執行在提高效率方面的有效性,同時也體現出并行符號執行工具Jdart-parallel在提高符號執行效率方面的優勢,在處理較大規模程序中效果也比較明顯.

未來的工作主要考慮能否在約束求解任務分配支持啟發式地搜索分配方式,能更加準確快速地搜索到與上一條相似度最高的那條路徑分配,充分利用上一條已保存的求解結果,可以進一步地提高效率,此外還希望該模型可以支持規模更大的程序,結合已有的各種優化機制,期望能夠在實際的項目得到應用.

[1] Bezier B.Software testing techniques,2nd edition[M].Van Nostrand Reinhold,New York,1990.

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

[3] Li Zhou-jun,Zhang Jun-xian,Liao Xiang-ke.Survey of software vulnerabllity detection techniques[J].Journal of Computer,2015,38(4):717-732.

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

[5] Sen K.DART:directed automated random testing[J].Acm Sigplan Notices,2005,40(6):213-223.

[6] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing[C].Conference on Computer Systems,ACM,2011:183-198.

[7] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[8] Kasper Luckow,Marko Dimjasevic,Dimitra Giannako poulou,et al.JDart:a dynamic symbolic analysis framework[C].International Confercence on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016:442-459.

[9] Dong Qi-xing,Zeng Fan-ping,Yan Jun.Improve the solving of non-linear arithmetic constraints in dynamic symbolic execution[J].Journal of Chinese Computer System,2014,35(11):2396-2401.

[10] Cadar C,Dunbar D,Engler D.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,USE-NIX Association,2008:209-224.

[11] Gupta A.Feedback-directed unit test generation for C /C ++ using concolic execution[C].International Conference on Software Engineering,IEEE,2013:132-141.

[12] Godefroid P,Levin M Y,Molnar D.SAGE:whitebox fuzzing for security testing[J].Queue,2012,10(1):40-44.

[13] An Jing.A research on key technologies of dynamic symbolic[D].Beijing:Beijing University of Posts and Telecommunications,2014.

[14] Siddiqui J H,Khurshid S.ParSym:parallel symbolic execution[C].International Conference on Software Technology and Engineering,2010:V1-405-V1-409.

[15] Staats M,Pǎsǎreanu C.Parallel symbolic execution for structural test generation[C].Nineteenth International Symposium on Software Testing and Analysis,ISSTA 2010,Trento,Italy,2010:183-194.

[16] Ciortea L,Zamfir C,Bucur S,et al.Cloud9:a software testing service.[J].Acm Sigops Operating Systems Review,2009,43(4):5-10.

[17] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing [C].Conference on Computer Systems,ACM,2011:183-198.

[18] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[19] Cassar I,Francalanza A.On implementing a monitor oriented programming framework for actor systems[J].Lecture Notes in Computer Science,2016.

附中文參考文獻：

[3] 李舟軍,張俊賢,廖湘科,等.軟件安全漏洞檢測技術[J].計算機學報,2015,38(4):717-732.

[10] 董齊興,曾凡平,嚴 俊,等.改進動態符號執行中的非線性約束求解過程[J].小型微型計算機系統,2014,35(11):2396-2401.

[12] 安 靖.動態符號執行關鍵技術研究[D].北京:北京郵電大學,2014.