劉濕潤(rùn)

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

基于GCC的符號(hào)執(zhí)行工具

劉濕潤(rùn)

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

靜態(tài)分析和符號(hào)執(zhí)行是發(fā)現(xiàn)源代碼缺陷和提高源代碼質(zhì)量的兩種有效方式。然而，這兩種技術(shù)都面臨各自的問(wèn)題，靜態(tài)分析誤報(bào)率較高和符號(hào)執(zhí)行一直面臨著路徑爆炸難題。為了減少靜態(tài)分析和符號(hào)執(zhí)行的這些限制，本文構(gòu)建了一個(gè)稱(chēng)為ABARZER-SE的工具，它是第一個(gè)基于GCC結(jié)合符號(hào)執(zhí)行和靜態(tài)分析的源代碼檢測(cè)工具。ABAZER-SE由兩個(gè)階段組成，第一階段是通過(guò)符號(hào)執(zhí)行獲取可行性路徑，第二階段應(yīng)用靜態(tài)分析技術(shù)對(duì)可行性路徑分析找到源代碼中缺陷。實(shí)驗(yàn)結(jié)果表明該工具具有可行性、有效性和可擴(kuò)展性。

信息安全；靜態(tài)分析；符號(hào)執(zhí)行；GCC；誤報(bào)

0 引言

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

本文的主要貢獻(xiàn)是：

（1）實(shí)現(xiàn)了漏洞檢測(cè)工具ABAZER-SE，第一個(gè)基于GCC分析的將符號(hào)執(zhí)行和靜態(tài)分析相結(jié)合的工具。

（2）使用該工具對(duì)現(xiàn)實(shí)世界的軟件程序進(jìn)行評(píng)估，結(jié)果表明ABARZER-SE可以顯著降低誤報(bào)率。

1 相關(guān)工作

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

靜態(tài)分析一直是研究領(lǐng)域或商業(yè)化市場(chǎng)中的一個(gè)活躍的主題。尤其是靜態(tài)分析的誤報(bào)得到了越來(lái)越多的關(guān)注。沒(méi)有檢查或沒(méi)有準(zhǔn)確檢查不可行路徑是造成誤報(bào)的重要原因之一。Tripp等人[11]通過(guò)對(duì)警告進(jìn)行統(tǒng)計(jì)學(xué)習(xí)精簡(jiǎn)靜態(tài)安全檢查器的輸出來(lái)減少誤報(bào)。Mu等人[12]提出了一種算法，構(gòu)建了一個(gè)面向控制流，數(shù)據(jù)流和模塊之間的相關(guān)性的數(shù)學(xué)模型以提取不可行路徑。然而，這些現(xiàn)有的工作需要構(gòu)建復(fù)雜的公式或模型并且需要大量的計(jì)算。

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

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

2 實(shí)現(xiàn)

2.1 指令模擬

符號(hào)執(zhí)行的核心思想是模擬程序運(yùn)行以獲得精確的數(shù)據(jù)流信息。ABAZER-SE基于GCC前端，從抽象語(yǔ)法樹(shù)提取數(shù)據(jù)流信息和進(jìn)行內(nèi)存模擬是ABAZER-SE的主要研究?jī)?nèi)容。

2.1.1 內(nèi)存模型

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

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

圖1 代碼片段

圖2 圖1代碼的內(nèi)存模型

2.1.2 指令語(yǔ)義的模擬

接下來(lái)，將使用上一節(jié)中構(gòu)建的內(nèi)存模型來(lái)進(jìn)行語(yǔ)句語(yǔ)義的模擬。為了收集數(shù)據(jù)流信息，指令語(yǔ)義模擬主要計(jì)算變量的值和地址。模擬指令語(yǔ)義的核心操作是操作符的處理。目前，已經(jīng)模擬了32個(gè)運(yùn)算符的語(yǔ)義，包括算術(shù)運(yùn)算符，邏輯運(yùn)算符，關(guān)系運(yùn)算符，指針解引用，數(shù)組，結(jié)構(gòu)引用等等。目前，已經(jīng)實(shí)現(xiàn)了C語(yǔ)言中73%操作符的語(yǔ)義模擬。

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

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

2.2 不確定性內(nèi)存地址的處理

圖3 賦值語(yǔ)句a=1的抽象語(yǔ)法樹(shù)

不確定性地址數(shù)據(jù)的處理是符號(hào)執(zhí)行的挑戰(zhàn)之一。當(dāng)然在本文的分析過(guò)程中，也面臨著這個(gè)問(wèn)題。例如，指針間接引用*(p + i)中變量p指向數(shù)組頭地址，變量i為輸入變量即其值不確定。對(duì)于這種情況，不能從已構(gòu)建的內(nèi)存模型中獲取*(p+i)值，因?yàn)闊o(wú)法得到p + i指向的地址。為了解決這個(gè)問(wèn)題，創(chuàng)建了特定的內(nèi)存結(jié)構(gòu)。通過(guò)創(chuàng)建鏈表，用鏈表結(jié)點(diǎn)來(lái)存儲(chǔ)此特定數(shù)據(jù)類(lèi)型。鏈表結(jié)點(diǎn)字段包括值，類(lèi)型和索引。如果鏈表結(jié)點(diǎn)沒(méi)有具體值，則將為其分配符號(hào)值?？梢栽阪湵碇蓄l繁地添加或查詢結(jié)點(diǎn)進(jìn)行不確定地址的處理。

2.3 約束求解

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

3 實(shí)驗(yàn)

圖4 實(shí)驗(yàn)代碼

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

表1顯示了ABAZER-SE與ABAZER實(shí)驗(yàn)結(jié)果對(duì)比，包括真陽(yáng)性、誤報(bào)率和運(yùn)行時(shí)間，人工驗(yàn)證了所有的誤報(bào)。實(shí)驗(yàn)測(cè)試對(duì)象為Coreutils 6.11，由于ABAZER-SE是基于規(guī)則的漏洞掃描工具，故在實(shí)驗(yàn)過(guò)程中主要關(guān)注三類(lèi)缺陷，包括內(nèi)存泄漏，約束溢出和除零錯(cuò)誤。結(jié)果說(shuō)明ABAZER-SE在對(duì)檢測(cè)出真正缺陷沒(méi)有影響的情況下可以有效減少誤報(bào)誤報(bào)，并且時(shí)間開(kāi)銷(xiāo)在可以接受的范圍內(nèi)。

表1 ABAZER-SE與ABAZER實(shí)驗(yàn)結(jié)果對(duì)比

4 結(jié)論

在本文中，使用符號(hào)執(zhí)行技術(shù)來(lái)減少靜態(tài)分析中的誤報(bào)。ABAZER-SE是第一個(gè)在GCC上構(gòu)建的符號(hào)執(zhí)行引擎，從GCC語(yǔ)法樹(shù)中提取信息進(jìn)行符號(hào)化分析，最終構(gòu)建了ABAZER-SE漏洞檢測(cè)工具。雖然已有一些成熟的符號(hào)執(zhí)行工具在LLVM上實(shí)現(xiàn)，實(shí)驗(yàn)結(jié)果表明，基于GCC的符號(hào)執(zhí)行仍然有其相對(duì)優(yōu)勢(shì)。使用符號(hào)執(zhí)行技術(shù)和靜態(tài)分析兩種技術(shù)互補(bǔ)檢測(cè)源代碼中的缺陷,利用符號(hào)執(zhí)行提供的足夠的數(shù)據(jù)流信息提高靜態(tài)分析的精確性。當(dāng)然，由于ABAZER-SE符號(hào)化分析還不夠完善該工具還在構(gòu)建中，目前還不能解析位運(yùn)算符，與KLEE相比其分析精度還不夠高，接下來(lái)我們會(huì)進(jìn)一步完善該工具。

[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

本文著錄格式：劉濕潤(rùn). 基于GCC的符號(hào)執(zhí)行工具[J]. 軟件，2016，37（12）：97-101