基于GCC的符號執行工具

劉濕潤

(北京郵電大學，北京 海淀 100876)

基于GCC的符號執行工具

劉濕潤

(北京郵電大學，北京 海淀 100876)

靜態分析和符號執行是發現源代碼缺陷和提高源代碼質量的兩種有效方式。然而，這兩種技術都面臨各自的問題，靜態分析誤報率較高和符號執行一直面臨著路徑爆炸難題。為了減少靜態分析和符號執行的這些限制，本文構建了一個稱為ABARZER-SE的工具，它是第一個基于GCC結合符號執行和靜態分析的源代碼檢測工具。ABAZER-SE由兩個階段組成，第一階段是通過符號執行獲取可行性路徑，第二階段應用靜態分析技術對可行性路徑分析找到源代碼中缺陷。實驗結果表明該工具具有可行性、有效性和可擴展性。

信息安全；靜態分析；符號執行；GCC；誤報

0 引言

靜態分析是在不考慮軟件運行或輸入值的情況下發現軟件程序中潛在錯誤的不可或缺的方法。目前，已經有很多靜態分析工具實現用來發現程序中的錯誤[1-4]。靜態分析的核心部分是識別軟件代碼中的典型錯誤模式。例如，一些基于Engler[5]思想的工具，使用有限狀態機和檢查器來表示時序性邏輯漏洞或系統規則，自動機引擎用于源代碼和缺陷模式匹配[6-8]。然而，所有這些工具面臨著靜態分析中較高誤報率的挑戰。符號執行通常應用于檢測系統代碼[9]中的嚴重錯誤并生成高覆蓋率的測試用例。然而，由于路徑的數量龐大，這種技術在實際應用中面臨著路徑爆炸的挑戰。為了減少靜態分析和符號執行技術在各自應用中的弊端，本文采用一種輕量級的符號執行和靜態分析相結合的方法。眾所周知，已有許多成熟的基于LLVM的符號執行工具，如KLEE[9]，SAGE[10]。然而，本文的靜態分析和符號執行基于GCC。盡管近年來LLVM已經得到廣泛應用，但GCC仍然有其不可替代的優勢，如GCC是Linux系統的標準編譯器，并支持更多的平臺和語言。基于以上的方法，并創建了ABARZER-SE，這是一個結合靜態分析和符號執行技術的工具，用于高效地檢查程序的常規屬性。當分析到條件表達式時，它將使用已經收集的數據流信息來判斷條件的正確性并選擇正確的路徑。給定一個程序屬性的檢查規則，ABARZER-SE執行可行的路徑而不是探索其所有路徑，大大降低了分析結果中的誤報率。此外，它允許用戶通過編寫自定義檢查器進行特定的靜態分析。

本文的主要貢獻是：

（1）實現了漏洞檢測工具ABAZER-SE，第一個基于GCC分析的將符號執行和靜態分析相結合的工具。

（2）使用該工具對現實世界的軟件程序進行評估，結果表明ABARZER-SE可以顯著降低誤報率。

1 相關工作

軟件漏洞的存在，降低了軟件的穩定性和安全性。目前，已有很多技術嘗試解決這個挑戰，包括代碼審查，更高層次的編程語言，測試和靜態分析。盡管這些技術可以檢測出一些漏洞，但是仍然有很多不足。測試是一個檢測代碼正確性廣泛應用的方法，但是通常只訓練一小部分執行路徑，每條路徑有一個單獨輸入值集合。因此，會丟失由其它輸入觸發的漏洞。靜態分析，在發現很多類型的漏洞是非常高效的。然而，靜態分析通常使用抽象提高可擴展性不能精確地推理程序的值和指針關系。因此，靜態工具通常會丟失依賴于特定輸入值的深層的漏洞。為了解決現有技術的不足，應之而生的是符號執行技術。通過應用符號執行技術，增加數據流信息的保存，極大的提高了分析的精確性降低了誤報率。因此，利用符號執行進行軟件和系統漏洞的檢測具有深遠的研究意義。

靜態分析一直是研究領域或商業化市場中的一個活躍的主題。尤其是靜態分析的誤報得到了越來越多的關注。沒有檢查或沒有準確檢查不可行路徑是造成誤報的重要原因之一。Tripp等人[11]通過對警告進行統計學習精簡靜態安全檢查器的輸出來減少誤報。Mu等人[12]提出了一種算法，構建了一個面向控制流，數據流和模塊之間的相關性的數學模型以提取不可行路徑。然而，這些現有的工作需要構建復雜的公式或模型并且需要大量的計算。

符號執行在最近幾年重新得到了廣泛關注。它可以用于自動軟件測試[9]，檢查嚴重缺陷[13,8-9]和驗證路徑[14]。ABAZER-SE與這些工作相似的地方是都是符號執行和靜態分析的結合，最大的區別是所基于的平臺ABAZER-SE基于GCC。除此之外，本文的分析基于GCC抽象語法樹而不是中間語言，在編譯器中抽象語法樹在中間語言的前一個階段所以抽象語法樹含有更豐富的源代碼信息。

目前國內外很多研究者采用靜態分析和符號執行相結合的方法進行漏洞檢測。2013年，WOODPECKER[8]的出現是符號執行史上的里程碑事件，首次將其用于系統規則的檢查，對于通常的規則它提供了一個安裝在內部checkers集合，和一個針對于用戶的接口以方便用戶檢查新的規則。它指示與檢測規則相關的符號執行程序路徑，消除冗余的路徑，加速了符號執行的速度；2015年，基于KLEE的UC-KLEE[15]由David等人提出，UC-KLEE一個新穎的可擴展性框架用于檢查C和C++代碼，通過直接檢測單個函數而不是整個程序提高可擴展性。Su等人[16]采用將符號執行和反例引導下基于精煉抽象模型相結合檢測方法，對于可行的測試目標輸出測試數據，減少不可行的測試目標。但是以上所有的符號執行分析都基于llvm低層虛擬機平臺，利用clang前端編譯器將程序生成中間代碼提取信息進行分析。

2 實現

2.1 指令模擬

符號執行的核心思想是模擬程序運行以獲得精確的數據流信息。ABAZER-SE基于GCC前端，從抽象語法樹提取數據流信息和進行內存模擬是ABAZER-SE的主要研究內容。

2.1.1 內存模型

內存模型是語義模擬的基礎并是ABAZER-SE的核心組成部分。構建內存模型的一個極端是將存儲器空間視為單字節數組[18]。顯然這樣具有相當高的精度，但是它的可擴展性非常差，并伴隨著巨大開銷。Burstall內存模型[19]廣泛應用于類型安全代碼分析。該模型的主要概念是將存儲器分成不相交的空間，但是它不夠準確。為了對內存進行建模，構建了一個新穎的內存模型，該內存模型可以精確地將每個左值表達式映射到相應的內存對象上。與上述所提到的內存模型相比，該模型具有很大的優勢。它支持更豐富的數據類型，包括基本類型，如void，char，integer和floating-point，以及派生類型，如pointer，array和struct。它可以處理各種算術運算。此外，構建了特定的內存模型結構來處理地址不確定的數據。在C語言中，有三種存儲區域：棧（本地），靜態區域（全局）和堆（動態分配的內存）。在該符號分析模型中，也遵循C語言的存儲策略。本文中的內存模型基于分層機制并支持整數類型，浮點類型，指針，數組和結構類型的存儲。

為了更好地理解本文所構建的內存模型，通過圖1和圖2進一步闡釋說明，圖1是要分析的程序片段，其對應的內存模型則如圖2。第一層中的內存單元主要包含程序中定義的變量，第二層內存單元主要包含的內容是第一層指向的元素，后續的內存單元以相同的方式分配。數組a 有五個字段，變量a指向該數組。指針p指向數組的首地址。結構體ss指向包含其結構字段的內存單元。結構體ss的第一個字段的值為1，因此相應的內存單元記錄值1。此外，為了處理浮點數運算，因此該內存模型也支持浮點數的存儲。浮點數b的值通過調用函數scanf獲得，因此并不知道其具體值，所以賦給它一個符號值sym1。

圖1 代碼片段

圖2 圖1代碼的內存模型

2.1.2 指令語義的模擬

接下來，將使用上一節中構建的內存模型來進行語句語義的模擬。為了收集數據流信息，指令語義模擬主要計算變量的值和地址。模擬指令語義的核心操作是操作符的處理。目前，已經模擬了32個運算符的語義，包括算術運算符，邏輯運算符，關系運算符，指針解引用，數組，結構引用等等。目前，已經實現了C語言中73%操作符的語義模擬。

AST是表示源代碼的抽象語法結構。樹中的每個節點都包含著源代碼的信息。首先，模擬工作從AST根結點開始，然后遞歸解析抽象語法樹的左子樹和右子樹。一個表達式的樹編碼類型表示此表達式的類型同時也是指令語義模擬分析的基本結構，樹編碼類型可以使用宏操作TREE_CODE獲取。接著，在第一步中獲得的樹編碼類型可以決定需要模擬的語義。如果表達式是一個變量聲明或一個參數聲明表達式，可以從抽象語法樹中得到該變量或參數的類型、名字和其他有關信息，然后為該變量分配內存存儲單元。如果表達式是算術運算，邏輯運算，關系運算或內存引用操作表達式，可以從抽象語法樹中獲取操作符和操作數并遞歸地計算它們的值。需要計算操作數的地址還是值由第一步中的獲得的樹編碼決定。最后，使用獲得的操作數的值并基于操作符的語義完成相應操作運算。

圖3展示了賦值表達式a=1的抽象語法樹。該賦值表達式的語義是給變量a賦值1。為了模擬該語句的語義，使用該操作TREE_CODE(a=1)可以得到該表達式的樹編碼類型MODIFY_EXPR。為了模擬MODIFY_EXPR的語義，需要得到左操作數（左子樹）的地址和右操作數（右子樹）的值。左子樹是一個VAR_DECL表達式，相應的變量地址可以從內存模型中獲取。右子樹是一個INTERGER_CST樹結點，值1可以通過宏操作直接從AST上獲取。最后一步是將值1存儲到變量的地址。至此，完成了對表達式a=1的語義模擬。

2.2 不確定性內存地址的處理

圖3 賦值語句a=1的抽象語法樹

不確定性地址數據的處理是符號執行的挑戰之一。當然在本文的分析過程中，也面臨著這個問題。例如，指針間接引用*(p + i)中變量p指向數組頭地址，變量i為輸入變量即其值不確定。對于這種情況，不能從已構建的內存模型中獲取*(p+i)值，因為無法得到p + i指向的地址。為了解決這個問題，創建了特定的內存結構。通過創建鏈表，用鏈表結點來存儲此特定數據類型。鏈表結點字段包括值，類型和索引。如果鏈表結點沒有具體值，則將為其分配符號值。可以在鏈表中頻繁地添加或查詢結點進行不確定地址的處理。

2.3 約束求解

為了檢查生成的約束集的可滿足性，本文使用Z3求解器來檢查。Z3是由微軟公司開發的一種新型的高效的SMT求解器，可從微軟官網上免費下載。Z3通常用于驗證各種軟件和分析應用程序。可滿足性模理論（SMT）問題是關于一階邏輯公式的決策問題，涉及很多理論背景知識，例如：算術、位向量、數組和未解釋函數[17]。ABARZER-SE使用由Z3提供的API進行約束求解。首先，將路徑條件轉換為由Z3可以識別的SMTLIB2.0標準形式。然后，將路徑條件傳送到Z3接口進行約束求解。最后，ABARZE-SE可以根據求解器的返回值確定路徑可行性。

3 實驗

圖4 實驗代碼

如圖4所示實驗代碼樣本，代碼中包含不可達路徑。ABAZER檢測該代碼時無法識別其中的不可達路徑，故對所有路徑都會進行分析，導致在不可達路徑中檢測到內存泄露和指針未分配空間即釋放的問題，而ABAZER-SE分析該代碼時，通過符號執行分析得到b=(int*)malloc(4)語句執行結束后表示2*m-1=n條件成立且m已經被賦值為20，通過符號執行的分析可知m+n<=16是不可能成立的，故不存在指針為分配空間即釋放問題。上述兩種缺陷的誤報在ABAZER-SE的分析結果中不會出現。以此證明，引入符號執行可有效裁剪不可達路徑，降低ABAZER的誤報率。

表1顯示了ABAZER-SE與ABAZER實驗結果對比，包括真陽性、誤報率和運行時間，人工驗證了所有的誤報。實驗測試對象為Coreutils 6.11，由于ABAZER-SE是基于規則的漏洞掃描工具，故在實驗過程中主要關注三類缺陷，包括內存泄漏，約束溢出和除零錯誤。結果說明ABAZER-SE在對檢測出真正缺陷沒有影響的情況下可以有效減少誤報誤報，并且時間開銷在可以接受的范圍內。

表1 ABAZER-SE與ABAZER實驗結果對比

4 結論

在本文中，使用符號執行技術來減少靜態分析中的誤報。ABAZER-SE是第一個在GCC上構建的符號執行引擎，從GCC語法樹中提取信息進行符號化分析，最終構建了ABAZER-SE漏洞檢測工具。雖然已有一些成熟的符號執行工具在LLVM上實現，實驗結果表明，基于GCC的符號執行仍然有其相對優勢。使用符號執行技術和靜態分析兩種技術互補檢測源代碼中的缺陷,利用符號執行提供的足夠的數據流信息提高靜態分析的精確性。當然，由于ABAZER-SE符號化分析還不夠完善該工具還在構建中，目前還不能解析位運算符，與KLEE相比其分析精度還不夠高，接下來我們會進一步完善該工具。

[1] PolySpaceVerifier, http://www.softdevtools.com/modules/weblinks/ singlelink.php?lid=116(2007).

[2] Coverity-A Higher Code, http://www.coverity.com/library/pdf/coverity_prevent.pdf (2008).

[3] CodeSonar Source-Code Analyser, http://www.scl.com/grammatech/codesonar (2008).

[4] Papcun J. Integrating Static Code Analysis and Defect Tracking[D]. Masarykova univerzita, Fakulta informatiky, 2014.

[5] Engler D, Chelf B, Chou A, et al. Checking system rules using system-specific, programmer-written compiler extensions[C]// Proceedings of the 4th conference on Symposium on Operating System Design & Implementation-Volume 4. USENIX Association, 2000: 1.

[6] Kremenek T. Finding software bugs with the clang static analyzer[J]. California: Apple Inc, 2008.

[7] Ivannikov V P, Belevantsev A A, Borodin A E, et al. Static analyzer Svace for finding defects in a source program code[J]. Programming and Computer Software, 2014, 40(5): 265-275.

[8] Cui H, Hu G, Wu J, et al. Verifying systems rules using rule-directed symbolic execution[J]. ACM SIGARCH Computer Architecture News, 2013, 41(1): 329-342.

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

[10] Godefroid, P., Levin, M. Y., Molnar, D. Automated white box fuzz testing[C]. NDSS'08, Proceedings of the conference on Network and Distributed System Security Symposium. USA, 2008: 151-166.

[11] Tripp O, Guarnieri S, Pistoia M, et al. Aletheia: Improving the usability of static security analysis[C]//Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. ACM, 2014: 762-774.

[12] Mu Y, Zheng Y, Zhang Z, et al. The algorithm of infeasible paths extraction oriented the function calling relationship[J]. Chinese Journal of Electronics, 2012, 21(2).

[13] Zhang Y, Clien Z, Wang J, et al. Regular property guided dynamic symbolic execution[C]//Proceedings of the 37th International Conference on Software Engineering-Volume 1. IEEE Press, 2015: 643-653.

[14] D. A. Ramos and D. R. Engler. Practical, low-effort equivalence verification of real code. In Proceedings of the 23rd international conference on Computer aided verification, CAV’11, pages 669–685, 2011.

[15] LAHIRI, S., HAWBLITZEL, C., KAWAGUCHI, M., AND REBELO, H. SymDiff: A language-agnostic semantic diff tool for imperative programs. In Proc. of Intl. Conf. on Computer Aided Verification (CAV) (2012).

[16] Su, Ting, et al. "Combining symbolic execution and model checking for data flow testing." 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering. Vol. 1. IEEE, 2015.

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

[18] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2004: 168-176.

[19] Burstall R M. Some techniques for proving correctness of programs which alter data structures[J]. Machine intelligence, 1972, 7(23-50): 3.

The Symbolic Execution Tool Based on GCC

LIU Shi-run
(Beijing University of Posts and Telecommunications, Beijing city Haidian District Xitucheng Road No. 10)

Static analysis and symbolic execution are two powerful ways of finding bugs and improving the quality of software. However, both of these techniques face their respective issues, e.g. false positives with static analysis tools and path explosion with symbolic execution method. To mitigate these limitations of static analysis and symbolic execution, we present a tool called ABARZER-SE, which is the first to implement symbolic execution and static analysis based on GCC. The workflow of ABAZER-SE consists of two phases, the first phase is to achieve feasible path by using symbolic execution, the second combines static analysis to analyze potential bugs. Experiment results show the effectiveness and scalability of the tool when it is used to analyze real-world software.

Static analysis; Symbolic execution; False positives; GCC

TP311.1

A

10.3969/j.issn.1003-6970.2016.12.022

本文著錄格式：劉濕潤. 基于GCC的符號執行工具[J]. 軟件，2016，37（12）：97-101