遺傳算法輔助的動態符號執行測試方法

謝章偉，崔展齊，鄭麗偉，張志華

北京信息科技大學 計算機學院，北京 100101

1 引言

由于軟件缺陷的存在，程序在運行過程中可能會出現一些不正常的行為，輕則造成程序功能異常，重則導致系統崩潰。軟件測試作為檢測軟件缺陷的一種重要方法，能夠有效檢測出程序存在的缺陷，提升軟件的可靠性[1]。符號執行作為一種重要的軟件測試方法，能夠通過生成高覆蓋率的測試用例，檢測隱藏較深的程序錯誤。

King 等人[2]于1975 年提出使用符號執行進行軟件分析，其基本思想是使用符號值表示輸入變量，在運行程序的過程中逐語句轉換成符號表達式，收集相應的路徑約束條件，并通過約束求解器求得滿足路徑約束條件的測試用例。當時由于受制于約束求解器求解能力，導致符號執行的路徑覆蓋率遠小于程序分析方法，使得研究陷入了低谷。隨著現代計算機計算能力的增強，以及研究人員對于約束求解器的不斷優化和改進，例如Z3[3]、MathSAT4[4]等性能優秀的約束求解器的出現，使得符號執行技術重新引起研究人員的關注[5]。常見的符號執行工具有 Symbolic Pathfinder[6]、KLEE[7]、JDart[8]、jCUTE和CUTE[9]等。盡管約束求解器的相關研究取得了突破性的發展，但隨著程序規模和復雜程度的劇增，約束求解器依舊面臨路徑爆炸、求解能力不足等問題[5，10]。

為此，常亮等人[11]提出采用并行化方法減少符號執行中路徑探索和約束求解耗時問題，該方法基于Actor模型并行模式，將動態符號執行中的約束求解任務和路徑探索任務并行執行，減少耗時代價；Bryant[12]使用積極算法，將SMT公式轉換成一個CNF型的命題公式，然后使用SAT求解器進行求解，通過高效地利用SAT求解器提升SMT的求解效率；Nuzzo[13]則提出使用凸規劃求解非線性凸的約束條件的可滿足性。雖然上述工作能夠在一定程度上緩解約束求解器求解能力不足的問題，但動態符號執行的覆蓋率仍受限于約束求解器的求解能力。

針對上述問題，本文提出了一種遺傳算法輔助的動態符號執行測試方法。首先，通過動態符號執行工具收集約束條件，當約束求解器無法求解當前約束條件或者求解時間超時，使用遺傳算法生成測試輸入；然后，根據輸入變量的數據類型生成一定數量的初始種群，通過適應度函數計算每個個體的適應度，根據適應度大小剔除適應度低的個體，通過對篩選之后的個體進行交叉變異和隨機變異生成新的種群；不斷迭代上述過程，直到生成滿足約束條件的測試輸入為止。本文基于所提出的方法開發了原型工具JDart-Ga，并在JDart 提供的測試用例集上進行了實驗。實驗結果表明，對于存在JDart無法覆蓋路徑的3 個實驗對象，JDart-Ga 的路徑覆蓋率均取得了提升，路徑覆蓋率最低提升了16%，最高提升了23%，同時測試時間增加不超過10%。

本文的主要貢獻包括：

（1）提出了一種遺傳算法輔助的動態符號執行測試方法，為約束求解器不能有效求解的路徑生成測試輸入。

（2）基于所提出的方法實現了原型工具JDart-Ga，并在一組公開的示例程序上進行實驗，以驗證該方法的有效性。

2 研究背景

2.1 動態符號執行

動態符號執行[14]結合使用了具體執行和符號執行，不再靜態模擬程序執行，而是為程序提供具體的輸入，通過實際運行程序，在程序運行中對程序進行動態分析。在動態符號執行的過程中，對符號變量相關的代碼段進行符號執行，使用約束求解器求解路徑約束條件，為每條路徑生成一個測試用例，將測試用例輸入并執行程序。通常情況下約束求解器有三種返回結果：如果約束求解器求解返回值為sat，則表示當前約束條件有解并已經找到某個合適的解；返回值為unsat，則表示當前約束條件無解；但如果返回值為don’t know，則表示約束求解器無法判斷當前約束條件是否有解。動態符號執行根據約束求解器的返回結果來選擇是否應該沿著當前路徑繼續往下探索。

2.2 遺傳算法

遺傳算法由Holland 提出[15]，是一種模擬達爾文生物進化論的自然選擇和遺傳學機理的生物進化過程的計算模型，是一種通過模擬自然進化過程的全局最優搜索方法，近些年來被廣泛運用于信息安全[16]、軟件測試[17]等領域。在達爾文進化論中提到，生物是通過不斷的基因變異來實現物種的進化，而自然選擇主導著進化的方向。基因突變的方向是隨機性的，自然選擇通過不斷淘汰不適應環境的類型，從而定向地改變種群中的基因向適應環境的方向演化。遺傳算法正是以此為指導思想，通過對問題的解（稱為個體）進行編碼，表現成染色體形式，通過模擬基因的隨機突變和交叉變異的方式實現個體的進化，并使用適應度函數評估當前個體的適應度，根據適應度的高低衡量個體對目標問題的適應度，選擇使用具有高適應度的個體進行遺傳，從而增大產生滿足目標問題解的概率。

3 遺傳算法輔助的動態符號執行測試方法

本文提出的方法框架如圖1所示，該方法主要包括兩個階段，左邊的是動態符號執行階段，右邊是遺傳算法階段。給定一個程序，首先進行動態符號執行測試，使用動態符號執行工具收集一條路徑上的約束條件，將其傳遞給約束求解器，根據約束求解器的求解結果result選擇下一步操作。若求解結果result為sat或unsat，則直接將結果返回給動態符號執行工具，若求解結果result=don’t know或者求解時間超時，則嘗試使用遺傳算法生成測試用例。通過不斷迭代上述過程，以覆蓋更多程序路徑。

圖1 遺傳算法輔助的動態符號執行測試框架

3.1 動態符號執行

圖2 展示了本文所使用的動態符號執行方法流程。與傳統動態符號執行方法相比，增加了一個調用遺傳算法生成測試輸入的步驟。首先，選擇一個目標程序，收集目標程序中的輸入變量并將其符號化，給定一個初始輸入并運行程序，從而獲得一條路徑約束條件集合。然后按照深度優先調度策略將路徑中的約束取反，獲得一條未覆蓋路徑的約束條件集合，使用約束求解器對約束條件集合進行求解，若約束求解器求解的結果為don’t know或者求解時間超時，則使用遺傳算法嘗試生成下一條路徑的測試輸入，否則直接將約束求解器的求解結果傳遞給動態符號執行工具。不斷重復上述過程，直到所有路徑都遍歷完畢。

圖2 動態符號執行方法流程

3.2 遺傳算法

遺傳算法的優點是在搜索過程中不需要關注問題的內在性質，對于目標函數和約束條件，無論是線性的還是非線性的，離散的還是連續的都可處理。

本文使用遺傳算法對約束求解器無法求解的約束條件進求解，具體的求解過程如算法1所示。算法1的輸入為一條為約束求解器無法求解的路徑約束條件集合constraintsExpr={expr1，expr2，…，expri}，其中，expri表示路徑上的約束條件。輸出為求解結果result，輸出的求解結果有兩種，若生成了滿足約束條件集合constraintsExpr的測試用例，則result=sat和滿足約束條件的測試輸入，否則返回result=don’t know。在算法1 中，population表示包含一定數量個體的初始種群，num表示種群進化的最大次數，size表示每次變異后下一代生存的個體數量。

在算法1 中，首先根據傳入的約束條件集合con-straintsExpr獲取輸入變量的數據類型，然后根據輸入變量的數據類型生成一定數量的種群population，計算當前種群中每個個體的適應度Fitness，如果當前個體的適應度Fitness=0，則說明當前個體為路徑約束條件constraintsExpr中所有約束條件的解，將解返回并結束。如果不滿足，則根據適應度的大小從小到大進行排列，保留排序靠前size的個體，通過對個體染色體進行交叉變異和隨機變異操作，產生新的種群newPopulation，不斷重復上述過程，直到找到滿足路徑約束條件constraintsExpr的個體為止。但如果種群進化的次數大于num時，仍然沒有生成滿足路徑約束條件constraintsExpr的測試用例時，出于對時間成本的考慮，結束循環并返回result=don’t know。

算法1使用遺傳算法生成測試用例

input：constraintsExpr：路徑約束條件

output：result：求解結果

1.SymbolicPar=constraintsExpr.containsAl（l）；

2.population=createInitialPopulation（SymbolicPar）；

3.//生成初始種群

4.foreach（evolve（num）） do

5.//進化到第num代之后就結束

6.foreach（chromosome：population）do

7.Fitness=calculate（chromosome）；

8.//計算每個個體的適應度

9.i（fFitness==0）then

10.return result；

11.end

12.newPopulation.sortByFitness（population）；

13.//根據適應度大小排序

14.newPopulation.trim（size）；

15.//剔除第population個之后的所有個體

16.newPopulation.chromosome.crossove（r）；

17.//交叉變異

18.newPopulation.randomChromosome（）；

19.//隨機變異

20.population=newPopulation；

21.end

22.end

23.returnresult；

其中，適應度函數是決定是否能成功生成測試輸入的關鍵，適應度函數的合理性決定生成測試用例的效率[18]。由于本文使用遺傳算法求解滿足路徑約束條件的解，故使用公式（1）來評價當前個體的適應度：

其中，length表示當前路徑約束條件集合constraintsExpr中約束條件的個數，N表示當前個體滿足路徑約束條件中約束條件的個數，N越大，適應度的值Fitness越低，說明當前個體越接近滿足路徑約束條件的解。

3.3 示例

以圖3 所示的代碼片段為例，該段代碼來自JDart提供的示例程序double2long。若使用動態符號執行方法，假設當前輸入為x=10.0，則覆蓋路徑的約束條件集合為constraintsExpr={x≥0.0,(sint64)(x/10.0)＜100} ，根據深度優先遍歷策略，將當前路徑約束條件集合中的第2個約束條件取反，則獲得了一條新的路徑約束集合{x≥0.0,(sint64)(x/10.0)≥100} 。此時約束求解器無法求解該條路徑的約束條件集合，返回的求解結果為result=don’t know，動態符號執行工具無法覆蓋該條路徑。若使用本文所提出的方法，當約束求解器返回result=don’t know時，將使用遺傳算法生成滿足目標路徑約束條件的測試輸入，將約束條件constraintsExpr={x≥0.0,(sint64)(x/10.0)≥100} 作為參數傳遞給遺傳算法模塊，求得當x=1 000.1 時，該路徑約束條件有解，則返回result=sat和測試用例x=1 000.1，從而輔助動態符號執行工具覆蓋上述路徑。

圖3 代碼示例

4 實驗分析

基于上述方法，本文在Java符號執行工具JDart的基礎上，實現了符號執行工具JDart-Ga。運行實驗的軟硬件環境為Intel?Core?i7-7700HQ處理器，主頻為2.80 GHz，內存2 GB，操作系統為Ubuntu 14.04，Sun JRE 1.8（64 bit mode）。

JDart[19]是一個基于Java PathFinder 框架的符號執行工具。在檢測Java 程序的過程中，JDart 能夠同時進行具體執行和符號執行，并將路徑約束組合起來，形成約束樹。JDart 通過SMT 求解器生成測試用例，并且嘗試運行從而收集未探索分支的路徑，不斷增強約束樹。

在實驗分析中延用了JDart 的路徑分類方式，使用OK PATHS 統計測試用例能覆蓋并且不會觸發錯誤的路徑數量；使用ERROR PATHS統計檢測出存在錯誤的路徑數量，例如斷言或者未捕獲的異常，斷言違規或未捕獲的異常等；使用DON’T KNOW PATHS 統計未探索的路徑數量；使用TOTAL PATHS 統計總的路徑覆蓋情況，即 TOTAL PATHS 等于 OK PATHS、ERROR PATHS和DON’T KNOW PATHS之和。

4.1 實驗設計

為了驗證所提出方法的有效性，本文將JDart 所提供的17個測試示例全部作為實驗對象，實驗對象信息如表1所示。表1中測試對象的命名方法為“類名稱_類內被測試方法名稱”。17個測試對象的輸入變量包括int、char、double、long和boolean等數據類型。

表1 實驗對象基本情況

實驗沿用文獻[7]所使用的評價方法，使用覆蓋路徑數量、路徑覆蓋率和測試的時間開銷進行對比分析。其中，路徑覆蓋率Cov的計算公式如公式（2）所示：

在公式（2）中，okPaths和errorPaths分別表示OK PATHS和ERROR PATH 的值，兩者相加表示測試用例能夠覆蓋的路徑數量，max{totalPathsJDart,totalPathsJDart-Ga}表示JDart和JDart-Ga中TOTAL PATHS的最大值。

在統計時間開銷的過程中，本文規定測試單個程序的時間上限不超過30 min，超出30 min 則記為超時，時間開銷記為30 min，覆蓋的路徑數量記為30 min內覆蓋的路徑。在實驗過程中，本文將遺傳算法中的參數值分別設置為：初始種群中的個體數population=100，每次進化之后下一代生存的個體數量size=100，進化的次數num=1 000。

4.2 實驗結果及分析

在實驗過程中，使用JDart和JDart-Ga分別對表1中測試對象進行測試，并收集了相關的路徑覆蓋信息，實驗結果如表2和圖4所示。其中，表2為三種路徑的覆蓋情況，圖4為路徑覆蓋率。從表2中可以看出，當DON’T KNOW PATHS為零時，即表示不存在SMT求解器無法求解的約束條件，所以JDart-Ga 和JDart 覆蓋的OKPATHS、ERROR PATHS 和 TOTALS PATHS 都相等。在17個測試對象中，有11個測試對象不存在SMT求解器無法求解的路徑約束條件，剩余6個測試對象中存在無法探索的路徑。其中，對于solvers_foo、nested_bar 和double2long_foo 3 個測試對象，JDart-Ga 的路徑覆蓋數量高于JDart，路徑覆蓋率分別提升了20%、23%和16%。具體來說，OK PATHS 分別增加了 0、2 和 1 條，ERROR PATHS分別增加了1、1和0條，TOTALS PATHS分別增加了0、6和0條。

表2 不同路徑覆蓋情況對比

圖4 路徑覆蓋率對比

對JDart-Ga 提升上述3 個實驗對象路徑覆蓋率的原因進行分析發現：（1）如果路徑約束條件中涉及強制類型轉換，有可能會出現同一輸入變量在路徑約束條件中存在兩種不同的數據類型的情況，約束求解器求解此類約束條件時間開銷過大，導致超出規定的時間，nested_bar 和double2long_foo 中存在這種類型的約束條件，例如：nested_bar 中的路徑約束條件{d<3.141，（sint32）d+65>64，5×（（sint32）d+65）>325，（sint32）d+65!=66}；（2）當存在約束求解器不能求解的復雜約束條件時，可以利用遺傳算法優勢，根據測試用例的適應度不斷變異生成趨近于滿足路徑約束條件的解，例如：對于solvers_foo中的路徑約束條件{d≥ 0.0，d≤ 6.283 185 307 179 586，sin（d）<0.0，cos（d）>0.0}，JDart無法求解，而JDart-Ga可以成功生成測試輸入d=4.715 407 046 706 579。

表3對JDart和JDart-Ga測試17個實驗對象的時間開銷進行了統計。由于JDart-Ga相比于JDart增加了一個求解判斷模塊，所以測試實驗對象所需的時間花銷要比JDart略長。如表3所示，與JDart相比，JDart-Ga測試solvers_foo、nhandler_foo、functions_foo、fields_foo 和double2long_foo 5 個實驗對象的時間開銷增幅超過10%；測試nested_bar 的時間開銷減少了99.8%；測試剩余11 個實驗對象的時間開銷增幅低于10%，與預期相符。對5 個時間開銷增幅超過10%的實驗對象進行代碼分析發現：（1）solvers_foo 和 double2long_foo 中均存在JDart 無法覆蓋的路徑，JDart-Ga 覆蓋了更多的程序路徑，從而導致時間開銷分別增加了15.2%和14.8%；（2）fields_foo、functions_foo和nhandler_foo中的DON’T KNOW PATHS 為約束求解器報告錯誤，實際上應該為unsat，而遺傳算法并不能從邏輯上去判斷約束條件是否有解，這導致JDart-Ga仍嘗試使用遺傳算法生成覆蓋上述路徑的測試輸入，消耗了大量無效時間，時間開銷分別增加了596.6%、400.9%和372.7%。對測試時間開銷大幅降低的nested_bar 進行分析，發現在該程序中有8條路徑約束條件都含有強制類型轉換操作，故約束求解器在無法判斷該類型的路徑約束條件是否有解的過程中消耗了大量的時間，而JDart-Ga 可以快速求解，從而節省了大量時間開銷。

表3 測試時間對比 ms

5 總結

本文深入研究了現有符號執行測試方法面臨的問題和挑戰，提出了一種遺傳算法輔助的動態符號執行測試方法。該方法能夠彌補動態符號執行中約束求解器所存在的求解能力不足的問題，從而達到提升路徑覆蓋的目的。實驗結果表明，本文提出的方法能夠有效地提升路徑覆蓋率。在下一步工作中，將嘗試將優化本方法應用于更加復雜的輸入數據類型和更大規模程序。