基于KLEE的復雜路徑中內(nèi)存泄露檢測研究

黃 琦,彭 武，蔡愛華，王冬海

(1.中國電子科學研究院，北京 100041;2.北京聯(lián)海信息系統(tǒng)有限公司，北京 100041)

0 引 言

在軟件安全問題中，內(nèi)存泄漏[1]指由于疏忽或錯誤造成程序未能釋放已經(jīng)不再使用的內(nèi)存的情況。內(nèi)存泄漏并非指內(nèi)存在物理上的消失，而是應用程序分配某段內(nèi)存后，由于設計錯誤，失去了對該段內(nèi)存的控制，因而造成了內(nèi)存的浪費。為了解決這一問題，科研工作者開發(fā)了非常多的檢測工具例如：ccmalloc[2]，Leaky[3]，LeakTracer[4]，MEMWATCH[5]，Valgrind[6]。這些檢測工具雖然檢測范圍廣泛，能夠處理很多的內(nèi)存泄露問題，但是運行花費較大，并且由于如今程序路徑的復雜程度越來越高，檢測工具對于代碼覆蓋率不高，因而許多復雜路徑中的內(nèi)存泄露問題無法得到解決。

本文利用符號執(zhí)行工具KLEE[7]，通過實現(xiàn)Z3[8]求解器在KLEE中的并行實現(xiàn)，生成能夠覆蓋復雜路徑的測試用例，最終利用生成的測試用例檢測出復雜路徑中的內(nèi)存泄露。

1 KLEE約束求解并行優(yōu)化設計

KLEE是一個運行在Linux操作系統(tǒng)上的開源動態(tài)符號執(zhí)行[9]工具，其具有自動化生成測試用例的特點，并且其生成的測試用例達到很高的代碼覆蓋率。KLEE中的求解模塊是由STP[10]求解器構成，由于原STP求解器支持的求解理論不足，我們將支持各種復雜求解理論的Z3求解器與STP求解器并行，共同實現(xiàn)KLEE的約束求解模塊，從而實現(xiàn)復雜路徑的覆蓋。

1.1 KLEE并行約束求解模塊

KLEE中使用符號執(zhí)行時，將收集程序路徑中的約束條件。對這些路徑約束條 件進行約束求解的主要作用有兩點，一是在程序中分支語句處的條件表達式中利用對變量值滿足條件與否來選擇程序執(zhí)行路徑，起到路徑預判的作用，二是在路徑選擇時，求解出滿足路徑約束條件的變量值分布。KLEE并行約束求解模塊如圖1所示。

圖1 KLEE并行約束求解模塊

KLEE并行約束求解模塊的實現(xiàn)將收集到的約束條件集經(jīng)過KLEE優(yōu)化模塊后，將Z3求解器和STP求解器并行求解，從而解決復雜路徑中生成的約束條件求解問題。

1.2 約束條件語法解析模塊

KLEE的約束求解模塊主要完成的功能是求解符號執(zhí)行過程中收集而來的約束條件集合來進行路徑選擇和變量求解。這項功能需要經(jīng)過如下三個步驟：首先，約束求解模塊應用優(yōu)化算法對約束集合進行化簡優(yōu)化；其次，因為在符號執(zhí)行中KLEE將約束條件描述成KQuery語法格式，因此約束集全發(fā)送到約束求解模塊后，還需要對該語法格式的約束條件調(diào)用求解器的函數(shù)接口進行解析，轉換成求解器的語法描述，才能進行求解。最后，求解器接受求解調(diào)度控制決定對化簡、轉換后的約束集合表達式進行求解。

KQuery語言是KLEE中約束表達式的文本表示語言，其語法描述使用擴展巴科斯范式(Extended Backus-Naur Form)表示[11]。KQuery定義了描述約束條件表達式的語法，在求解器和KQuery語言之間提供了一個抽象解析層，降低了具體的求解器代碼與KQuery的耦合度，可以增加KLEE中求解器的靈活性，如圖2所示。

圖2 約束條件解析層次圖

解析層定義為一個抽象類型，聲明了對于解析KQuery語法的操作函數(shù)，而具體的解析動作放在繼承類中實現(xiàn)，創(chuàng)建抽象類SolverBuilder用于定義解析KQuery語法的變量、數(shù)組以及表達式操作。如：位操作、算術操作、邏輯操作等。STP求解器和Z3求解器分別按照各自的實現(xiàn)方法實現(xiàn)這些操作。

1.3 約束求解調(diào)度設計

調(diào)用約束求解器的操作，都是在SolverImpl的子類STPSolverImpl中以直接調(diào)用STP的求解函數(shù)的形式實現(xiàn)，而對SolverImpl的操作又是放在Solver類對象中進行的。因此，可以在Solver的操作函數(shù)中，增加一個調(diào)度接口。同時在Solver類對象中增加一個SolverImpl實例。讓Solver對象需要調(diào)用求解器時，都經(jīng)過調(diào)度函數(shù)選擇兩個SolverImpl類型的派生對象來同時求解。如圖3所示。

圖3 求解調(diào)度層次圖

利用這種方法對于原有的代碼不需要進行修改，只要新增Solver的繼承類對象，在其中增加對SolverImpl對象的調(diào)度操作，從而實現(xiàn)了STP求解器和Z3求解器的并行設計。

2 KLEE約束求解器并行化的實現(xiàn)

從符號執(zhí)行過程中得到的約束條件集采用 KQuery語法描述，求解器無法直接求解這種格式的約束條件。STP求解器和Z3求解器都需要將約束條件轉換為自身的語法形式，才能完成求解。因此，上圖中約束解析層起到解析KQuery語句，將約束條件轉換為各個求解器自己設計的語法形式。使用抽象的約束解析層，對外隱藏了各個求解器具體的解析過程，使得解析操作具有一個統(tǒng)一的對外調(diào)用形式。

2.1 KQuery抽象解析層

KLEE中原有求解模塊改進為并行求解模塊后的求解流程。從符號執(zhí)行過程中得到的約束條件集采用KQuery語法描述，求解器無法直接求解這種格式的約束條件。如圖4所示。

圖4 抽象解析層實現(xiàn)

KQuery抽象解析層設計的主要目的是為解析KQuery表示的約束條件提供統(tǒng)一的對外調(diào)用接口，同時對聲明了基本的解析函數(shù)名。在設計中，考慮到可擴展性和規(guī)范性，沒有沿用KLEE源代碼中STP的解析設計，而是重新設計了該抽象解析類的操作函數(shù)。

如上面所示代碼是KQuery的抽象解析的主體部分，定義了與各個KQuery語句對應的虛函數(shù)，具體的實現(xiàn)有賴于具體求解器的不同代碼。最后一個Analysis方法應用上面的函數(shù)，對約束條件進行解析。其偽代碼形式如圖5所示。

圖5 Analysis偽代碼

符號執(zhí)行過程收集起來的約束條件以Expr結構的形式傳遞給解析過程，通過 讀取該結構中的內(nèi)容，通過類似Switch的分支選擇，可以分析出這段字符串中含 有哪些約束條件，通過解析后將這些約束條件轉換為求解器相關的語法形式，存入求解器的存儲空間也就是*Constraints 指示的空間中。在約束條件解析完成后將該地址返回。

2.2 Z3約束求解器實現(xiàn)

KLEE源代碼中有關于STP求解器模塊，是KLEE在進行約束求解過程中調(diào)用了STP求解器模塊進行求解，但是與此同時STP求解器在于非線性問題上的欠缺和理論上的不足，導致對于復雜路徑的約束條件無法求解，于是這里我們將Z3求解器并行加入，與STP求解器共同對KLEE中經(jīng)過符號執(zhí)行過后收集的約束條件進行求解。當一個子進程結束后，主進程中止運行中的求解，將會得到兩者共享的區(qū)域中得到結果。

圖6 Z3SolverImpl類主要成員及操作

Z3求解器類繼承自SolverImpl基類。在圖6中給出的Z3SolverImpl類中包含了解析類對象SolverBuilder的指針，以及一個Solver類對象指針。在Z3SolverImpl類對象構造的時候，給這兩個指針賦以對應的對象地址。SolverBuilder類型指針用來使用前面構造完成的Z3解析類對象。而Solver類型的指針的作用是在Z3約束求解類對象中加入對約束條件集的優(yōu)化操作。

KLEE中本來的Solver基類的接口函數(shù)與我們設計的ConcurrentSolver類型設計相符合，在使用的時候可以像源代碼中使用STPSolver類一樣的使用，由于我們設計的接口保持了與原來KLEE原約束求解模塊的接口保持了一致，在實驗中可以通過直接KLEE的運行參數(shù)來調(diào)用這兩個求解器進行測試用例的生成。求解模塊如圖7所示。

圖7 Z3和STP求解模塊調(diào)度實現(xiàn)

通過上述對Z3求解器調(diào)度的實現(xiàn)，將兩個求解器并行加入到KLEE中去，在原有的KLEE基礎上，實現(xiàn)了在KLEE中利用多進程使用Z3和STP求解器對約束條件集合同時進行求解的代碼實現(xiàn)。從而實現(xiàn)對復雜路徑進行約束求解，生成覆蓋復雜路徑的測試用例。

3 復雜路徑中內(nèi)存泄露檢測方法

對于C和C++這種沒有Garbage Collection 的語言來講，我們主要關注兩種類型的內(nèi)存泄漏：堆內(nèi)存泄漏[12](Heap leak)。對內(nèi)存指的是程序運行中根據(jù)需要分配通過malloc,realloc new等從堆中分配的一塊內(nèi)存，再是完成后必須通過調(diào)用對應的 free或者delete 刪掉。如果程序的設計的錯誤導致這部分內(nèi)存沒有被釋放，那么此后這塊內(nèi)存將不會被使用，就會產(chǎn)生Heap Leak；系統(tǒng)資源泄露(Resource Leak)[13]主要指程序使用系統(tǒng)分配的資源比如 Bitmap,handle ,SOCKET等沒有使用相應的函數(shù)釋放掉，導致系統(tǒng)資源的浪費，嚴重可導致系統(tǒng)效能降低，系統(tǒng)運行不穩(wěn)定。

由于之前利用并行了Z3求解器的KLEE能夠生成覆蓋復雜路徑各個分支的測試數(shù)據(jù)、路徑條數(shù)、結點位置。本文利用output窗口定位檢測引發(fā)內(nèi)存泄露的代碼。

首先將檢測程序調(diào)成debug模式，然后在需要檢測的內(nèi)存泄露程序cpp頭上加上以下代碼如圖8。

圖8 內(nèi)存泄露檢測

最后在由并行了Z3求解器的KLEE測試出來的每條路徑上分別加入圖9中的檢測代碼：

圖9 內(nèi)存泄露檢測代碼

通過上述的操作之后，能夠在輸出中看到檢測程序的內(nèi)存泄露情況，上述原理是將MFC中的內(nèi)存泄露檢測方法推廣到一般的內(nèi)存泄露檢測問題中，從而生成內(nèi)存泄露問題的檢測報告。報告中不僅能檢測出內(nèi)存泄露問題，還能定位內(nèi)存泄露的位置和個數(shù)，達到內(nèi)存泄露檢測的目的。

4 實 驗

為了驗證本文方法的正確性和有效性，我們在linux系統(tǒng)下進行KLEE的測試，最終的內(nèi)存泄露檢測在windows系統(tǒng)下進行，在編寫的10條復雜路徑中的每段分支都加入內(nèi)存泄露代碼，通過上述方法進行內(nèi)存泄露的檢測，生成內(nèi)存泄露報告。

進行測試的部分源代碼如圖10所示。

圖10 部分內(nèi)存泄露代碼

下面給出KLEE及Z3求解器并行之后的KLEE測試結果：

KLEE測試的結果如圖11所示。

圖11 KLEE測試結果

改進后KLEE測試的結果如圖12所示。

圖12 Z3求解器并行的KLEE測試結果

通過上述求解的結果的對比，并行Z3求解器后的KLEE測試出10條路徑中的8條，并且對每條路徑都生成了能夠覆蓋的測試數(shù)據(jù)，而原KLEE求解器只覆蓋了其中5條路徑。充分說明了Z3求解器并行實現(xiàn)的KLEE具有更強的求解復雜路徑的能力，該方法具有正確性和可行性。

下面利用上面的測試的數(shù)據(jù)，按照本文中采用的內(nèi)存泄露檢測方法，進行漏洞泄露檢測，實驗結果如圖13所示。

圖13 內(nèi)存泄露檢測結果

通過上述的內(nèi)存泄露檢測結果我們可以看出，利用Z3求解器并行后的KLEE找到了復雜路徑的各條路徑之后，對每條路徑進行內(nèi)存泄露檢測，最終得到了內(nèi)存泄露的位置、個數(shù)，證明了本文方法的正確性和可行性。

5 結 語

本文在原有的符號執(zhí)行工具KLEE的基礎上，改進了原有KLEE中STP求解器支持理論不足的問題，加入Z3求解器與STP求解器并行來求解復雜路徑問題，繼而利用測試數(shù)據(jù)對每條路徑分別進行內(nèi)存泄露的檢測，最終實現(xiàn)了復雜路徑中的內(nèi)存泄露檢測。通過結果定位了內(nèi)存泄露的位置和個數(shù)，充分證明了該方法的正確性和可行性。

本文在原KLEE的基礎上進行了Z3求解器的并行移植，最終通過求解數(shù)據(jù)分析出每條路徑對每條路徑分別進行內(nèi)存泄露檢測，提高了內(nèi)存泄露檢測的范圍。但是對于爆炸路徑的程序，這種檢測方法工作量將極其巨大，通過本文中已經(jīng)解決的復雜路徑的檢測方法可以進行推廣、優(yōu)化，為解決爆炸路徑提供了參考。

[1] Joy M M, Mueller W, Rammig F J. Source code annotated memory leak detection for soft real time embedded systems with resource constraints[C]//Dependable, Autonomic and Secure Computing (DASC), 2014 IEEE 12th International Conference on. IEEE, 2014: 166-172.

[2] Parashar S, Parashar A. Application Specific Data Trace Cache Design[J]. International Journal of Computer Applications, 2011, 22(5): 18-21.

[3] Bellinger A M, Reiken S, Carlson C, et al. Hypernitrosylated ryanodine receptor calcium release channels are leaky in dystrophic muscle[J]. Nature medicine, 2009, 15(3): 325-330.

[4] Wang G, Li N, Li F. Method of cumulative helium mass spectrometric combination test by using argon as gross-leak tracer gas: U.S. Patent Application 14/134,006[P]. 2013-12-19.

[5] Books L L C. Free Memory Management Software: Valgrind, Memcached, Mtrace, Leb128, Splint, Duma, Electric Fence, Memory Pool System, Mpatrol, Memwatch[J]. 2010.

[6] Developers V. Valgrind[J]. Web page at http://valgrind. org (2000-2005), 2010.

[7] Cadar C, Dunbar D, Engler D R. KLEE: Unassisted and Automatic eneration of High-Coverage Tests for Complex Systems Programs[C]//OSDI. 2008, 8: 209-224.

[8] De Moura L, Bj?rner N. Z3: An efficient SMT solver[M]//Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2008: 337-340.

[9] R. Martins, V. Manquinho, I. Lynce, An overview of parallel SAT solving, Constraints[R], 2012，17(3)： 304-347.

[10] H. Zhu, D. Huang, W. Zhang, Z. Wu, Y. Lu, H. Jia, M. Wang, C. Lu, The novel virulence-related gene stp of Streptococcus suis serotype 9 strain contributes to a significant reduction in mouse mortality, Microbial Pathogenesis[C], 51 (2011) 442-453.

[11] KQuery Language Reference Manual [EB/OL]. http://klee.github.io/klee/KQuery.html

[12] Serna F J. The info leak era on software exploitation[J]. Black Hat USA, 2012.

[13] Torlak E, Chandra S. Effective interprocedural resource leak detection[C]//Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1. ACM, 2010: 535-544.