(南京大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)系,江蘇 南京 210023)

(計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué)),江蘇 南京 210023)

隨著移動計(jì)算、物聯(lián)網(wǎng)、云計(jì)算、人工智能、開源軟件、RISC-V 開源指令集等領(lǐng)域的飛速發(fā)展,相關(guān)的軟/硬件都迎來了新的發(fā)展機(jī)遇和挑戰(zhàn).為了適應(yīng)軟/硬件的發(fā)展,當(dāng)前也涌現(xiàn)出了很多新的編程語言和編譯器.但是,C 語言作為高效率、面向過程、抽象化的通用程序設(shè)計(jì)語言,仍然廣泛應(yīng)用于系統(tǒng)軟件的開發(fā).系統(tǒng)軟件中如果存在漏洞,就可能會被惡意利用,將會嚴(yán)重影響人們的生產(chǎn)生活,甚至威脅到生命財(cái)產(chǎn)安全.軟件安全已成為軟件企業(yè)不能回避的挑戰(zhàn).

C 語言被廣泛應(yīng)用于底層軟件生態(tài)系統(tǒng)的開發(fā),這是因?yàn)镃 語言程序具有更高的運(yùn)行效率.其中,數(shù)組是C語言最重要的數(shù)據(jù)結(jié)構(gòu)之一.當(dāng)一個數(shù)組在程序中被使用時,訪問該數(shù)組的下標(biāo)索引必須在一定范圍之內(nèi),即不小于0 并且小于數(shù)組的大小,否則會造成數(shù)組下標(biāo)越界.數(shù)組越界的缺陷在很多編譯后的系統(tǒng)中都存在,而且通過實(shí)驗(yàn),我們發(fā)現(xiàn),像gcc、clang 這樣主流的C 語言編譯器,在編譯過程中不會對數(shù)組下標(biāo)取值范圍的合法性加以嚴(yán)格檢查.數(shù)組越界有兩種模式,讀越界和寫越界.讀越界會導(dǎo)致讀取到隨機(jī)的值,繼而使用該值會導(dǎo)致未定義行為.相比之下,寫越界會造成更加嚴(yán)重的后果,不僅會造成未定義行為,甚至?xí)?dǎo)致控制流截取,使得攻擊者可執(zhí)行任意惡意代碼[1,2].如圖1 所示,根據(jù)CVE 歷史統(tǒng)計(jì)可以發(fā)現(xiàn),占據(jù)前三的漏洞類型為拒絕服務(wù)、代碼執(zhí)行和溢出[3].而數(shù)組越界缺陷常常會導(dǎo)致拒絕服務(wù)、代碼執(zhí)行和溢出.比如Adobe 閱讀器2017 之前版本中存在的遠(yuǎn)程代碼執(zhí)行和拒絕服務(wù)漏洞就是由于外部輸入作為數(shù)組下標(biāo)從而可能導(dǎo)致寫越界引起的(CVE-2017-16391、CVE-2017-16410).同時,研究表明[4-6],31%的緩沖區(qū)溢出是由數(shù)組越界造成的.因此,可見數(shù)組越界缺陷仍然是嚴(yán)重威脅系統(tǒng)軟件安全的重要缺陷類型.本文主要針對在給定C 程序源碼時,檢測數(shù)組下標(biāo)越界和由循環(huán)導(dǎo)致的數(shù)組下標(biāo)越界問題.為了提高系統(tǒng)軟件的安全性,程序必須對由外部輸入控制的數(shù)組下標(biāo)進(jìn)行邊界檢查.但是,開發(fā)者可能會遺漏邊界檢查或者沒有進(jìn)行正確的邊界檢查,使得程序處于可被攻擊利用的不利狀態(tài).

Fig.1 Statistics of the number of common types of CVE vulnerabilities圖1 CVE 常見類型漏洞的數(shù)目統(tǒng)計(jì)

目前已有一些研究工作提出使用靜態(tài)分析方法和動態(tài)測試方法來進(jìn)行數(shù)組越界檢查.由于動態(tài)方法總是依賴于測試用例的完整性,從而導(dǎo)致這些方法無法達(dá)到足夠高的程序覆蓋率.靜態(tài)分析方法通過掃描分析程序源代碼以檢查程序中的缺陷.當(dāng)前的靜態(tài)分析方法出于效率的考慮,未對程序進(jìn)行高精度的分析,未處理循環(huán)導(dǎo)致的數(shù)組越界,并且多是基于規(guī)則的匹配方法,無法處理復(fù)雜約束、復(fù)雜表達(dá)式等情況,導(dǎo)致一些已有的數(shù)組越界靜態(tài)檢測方法從而存在大量的誤報和漏報現(xiàn)象.

因此,為了進(jìn)行高精度的、高效的靜態(tài)分析來檢測數(shù)組越界缺陷,一方面,我們提出使用按需污點(diǎn)分析計(jì)算數(shù)組下標(biāo)和數(shù)組長度的污點(diǎn)值,當(dāng)數(shù)組長度污染時,即使在數(shù)組下標(biāo)非污染的情況下仍然可能導(dǎo)致數(shù)組越界(比如圖2 第11 行所示的數(shù)組訪問語句),而在數(shù)組下標(biāo)污染時,則需要進(jìn)行高精度的數(shù)據(jù)流分析以檢測是否會導(dǎo)致數(shù)組越界;另一方面,我們提出在靜態(tài)分析的過程中使用優(yōu)化后的約束求解器來處理程序中與數(shù)組訪問相關(guān)的復(fù)雜約束和復(fù)雜表達(dá)式,從而有效地提高檢測方法的準(zhǔn)確性.對于數(shù)組下標(biāo)越界問題,我們關(guān)注從程序入口到數(shù)組訪問語句之間,數(shù)組下標(biāo)越界條件的可滿足性,通過將約束求解引入到數(shù)據(jù)流分析過程中,能夠更加精確地檢查數(shù)組越界問題.

在本文中,我們提出了一個靜態(tài)分析框架Carraybound,該框架基于靜態(tài)的污點(diǎn)分析、數(shù)據(jù)流分析以及約束求解檢查程序中是否存在潛在的數(shù)組越界缺陷.除此之外,Carraybound 還提供待增加的數(shù)組邊界檢查條件,可以幫助程序員更加方便、快速地定位、確認(rèn)和修復(fù)我們報告的數(shù)組越界警報.實(shí)驗(yàn)結(jié)果表明Carraybound 可以快速、有效地報告出程序中的數(shù)組越界缺陷,并通過與已有靜態(tài)分析工具Cppcheck、Checkmarx 和HP Fortify進(jìn)行對比,展示了Carraybound 在發(fā)現(xiàn)數(shù)組越界缺陷上的優(yōu)越性.

本文的主要貢獻(xiàn)包括:

·提出流敏感、上下文敏感的按需指針分析方法,實(shí)現(xiàn)數(shù)組長度區(qū)間分析;提出按需污點(diǎn)分析方法,實(shí)現(xiàn)數(shù)組下標(biāo)和數(shù)組長度污染情況的計(jì)算.

·提出基于污點(diǎn)分析的數(shù)組越界缺陷的檢測方法,定義了數(shù)組越界缺陷判定規(guī)則,然后依據(jù)判定規(guī)則,使用后向數(shù)據(jù)流分析檢測數(shù)組越界,并將約束求解引入到數(shù)據(jù)流分析過程中以檢查數(shù)組越界缺陷,同時通過優(yōu)化盡量減少對約束求解器的調(diào)用,以提高分析效率.

·實(shí)現(xiàn)了一個靜態(tài)分析工具Carraybound,檢測C 程序中的數(shù)組越界缺陷(包括由循環(huán)導(dǎo)致的數(shù)組越界缺陷),并通過實(shí)驗(yàn)展示了工具的有效性.

本文第1 節(jié)介紹我們工作的背景知識.第2 節(jié)介紹所提出的基于污點(diǎn)分析的數(shù)組越界的靜態(tài)檢測方法.第3節(jié)介紹實(shí)現(xiàn)工具Carraybound,并通過實(shí)驗(yàn)展示該工具的有效性和效率,同時討論該工具的不足之處.第4 節(jié)介紹相關(guān)工作.第5 節(jié)進(jìn)行總結(jié),并提出未來工作展望.

1 背景知識

1.1 數(shù)組越界

數(shù)組是在內(nèi)存中連續(xù)存儲的具有相同類型的一組數(shù)據(jù)的集合.C 語言中數(shù)組分為靜態(tài)數(shù)組和動態(tài)數(shù)組.靜態(tài)數(shù)組在內(nèi)存中位于棧區(qū),其長度為常量,是定義時就在棧上分配了固定大小,運(yùn)行時,這個大小不能改變,例如char a[7].對靜態(tài)數(shù)組的寫越界訪問將會導(dǎo)致棧上的緩沖區(qū)溢出.動態(tài)數(shù)組在內(nèi)存中位于堆區(qū),其長度可以是變量,亦即可以在程序運(yùn)行時在堆上動態(tài)分配大小,例如int *a=(int*)malloc(sizeof(int)*10).對動態(tài)數(shù)組的寫越界訪問將會導(dǎo)致堆上的緩沖區(qū)溢出.

當(dāng)一個數(shù)組在程序中被使用時,訪問該數(shù)組的下標(biāo)索引必須在一定范圍之內(nèi),即不小于0 并且小于數(shù)組的大小,否則會造成數(shù)組下標(biāo)越界[8].如圖2 中第11 行所示的數(shù)組,由于數(shù)組arr的長度m來自于外部輸入,因此常量數(shù)組下標(biāo)也可能會導(dǎo)致數(shù)組越界訪問.

如圖3 所示,我們將C 語言程序中的越界訪問問題歸結(jié)為以下兩類.

①數(shù)組下標(biāo)越界:包括讀越界和寫越界.例如char c=a[5]是讀越界而a[5]=0 屬于數(shù)組的寫越界.其中,數(shù)組下標(biāo)訪問寫越界會導(dǎo)致緩沖區(qū)溢出,即圖3 所示的交集部分.數(shù)組下標(biāo)越界還包括循環(huán)導(dǎo)致的數(shù)組下標(biāo)越界,比如char a[5];for (int i=0;i＜6;i++){a[i]=0;}.

② 緩沖區(qū)溢出:包括API 調(diào)用和數(shù)組下標(biāo)訪問寫越界導(dǎo)致的緩沖區(qū)溢出.比如strcpy(dest,src)和a[5]=0.

本文方法目前側(cè)重于數(shù)組下標(biāo)越界(包含循環(huán)導(dǎo)致的數(shù)組下標(biāo)越界)問題.對于由API 調(diào)用導(dǎo)致的緩沖區(qū)溢出問題,我們的另一項(xiàng)緩沖區(qū)溢出靜態(tài)警報確認(rèn)的工作重點(diǎn)關(guān)注了該類問題[5].

通常情況下,程序員可以通過特定的方式限制數(shù)組下標(biāo)的范圍,以避免數(shù)組越界的發(fā)生.常見的3 種方式如下所示.

①idx=idx % size;

② if (idx＞=size||idx＜0)…

③assert (idx＞=0 && idx＜size);

程序中也可能存在一些復(fù)雜的約束和表達(dá)式實(shí)現(xiàn)了對數(shù)組下標(biāo)的范圍限制,比如按位操作、包含多個運(yùn)算符的線性運(yùn)算,甚至是非線性約束.這些情況會加大分析難度,導(dǎo)致傳統(tǒng)方法無法精準(zhǔn)地檢查出程序中的數(shù)組越界缺陷.

Fig.2 Example code of test.c圖2 test.c 代碼示例

Fig.3 Buffer overflow vs.array index out of bound圖3 緩沖區(qū)溢出和數(shù)組下標(biāo)越界關(guān)系圖

1.2 污點(diǎn)分析

污點(diǎn)分析是檢測程序漏洞的常用技術(shù)[7,9,10].如果攻擊者向程序輸入一些惡意數(shù)據(jù),而程序沒有進(jìn)行恰當(dāng)?shù)姆雷o(hù),則可能會導(dǎo)致系統(tǒng)處于不安全的狀態(tài).這些受外部輸入影響的數(shù)據(jù)在污染分析中標(biāo)記為污染.外部輸入包括用戶或文件的輸入、主函數(shù)的參數(shù).污點(diǎn)分析嘗試識別程序中那些會被用戶輸入污染的變量,并最終追溯到可能會導(dǎo)致程序缺陷的語句.如果在該語句之前,未經(jīng)檢查就直接使用被污染的數(shù)據(jù),則視為一個程序缺陷.污點(diǎn)分析分為靜態(tài)污點(diǎn)分析和動態(tài)污點(diǎn)分析.其中,動態(tài)污點(diǎn)分析需要執(zhí)行程序,無法保證對源碼的覆蓋率.靜態(tài)污點(diǎn)分析主要依賴于程序抽象語法樹和控制流圖進(jìn)行數(shù)據(jù)流分析,不需要實(shí)際執(zhí)行程序.因此靜態(tài)污點(diǎn)分析可以實(shí)現(xiàn)比動態(tài)污點(diǎn)分析更高的源代碼覆蓋率.但靜態(tài)污點(diǎn)分析可能因缺乏運(yùn)行時信息而產(chǎn)生誤報和漏報.

1.3 數(shù)據(jù)流分析

數(shù)據(jù)流分析通常用于靜態(tài)代碼分析,是一種基于控制流圖來收集數(shù)據(jù)流信息的技術(shù).對程序進(jìn)行數(shù)據(jù)流分析的一種簡單方法是為控制流圖的每個節(jié)點(diǎn)建立數(shù)據(jù)流方程,并通過在每個節(jié)點(diǎn)上重復(fù)計(jì)算輸入的輸出來反復(fù)迭代,直到整個系統(tǒng)到達(dá)不動點(diǎn)[11,12].前向數(shù)據(jù)流分析和后向數(shù)據(jù)流分析是數(shù)據(jù)流分析的兩種不同方法.前向數(shù)據(jù)流分析沿著正常的執(zhí)行路徑,從入口節(jié)點(diǎn)開始并在目標(biāo)節(jié)點(diǎn)處結(jié)束.一個基本塊的出口狀態(tài)是該基本塊中的語句對該基本塊的入口狀態(tài)作用的結(jié)果,一個基本塊的入口狀態(tài)則是其所有前驅(qū)基本塊的出口狀態(tài)的組合.與之相對地,后向數(shù)據(jù)流分析與控制流圖中的有向邊方向相反,從目標(biāo)節(jié)點(diǎn)開始并在入口節(jié)點(diǎn)處結(jié)束.一個基本塊的入口狀態(tài)是該基本塊中的語句對該基本塊的出口狀態(tài)作用的結(jié)果,一個基本塊的出口狀態(tài)則是其所有后繼基本塊的入口狀態(tài)的組合.

1.4 指針分析

數(shù)組越界缺陷的根源實(shí)際上是由于指針對內(nèi)存的越界訪問引起的.數(shù)組名代表了一個指向數(shù)組首元素的指針,通過數(shù)組下標(biāo)訪問數(shù)組元素(即p[i]),實(shí)際上與指針從數(shù)組首元素移動到特定元素進(jìn)行訪問(即*(p+i))是等價的.為了計(jì)算數(shù)組名實(shí)際指向的內(nèi)存區(qū)域,就需要進(jìn)行指針分析.

指針分析是一類特殊的數(shù)據(jù)流問題,是指通過程序分析方法計(jì)算指向相同內(nèi)存區(qū)域的指針表達(dá)式的集合.指針分析有幾個重要的精度衡量屬性,如流敏感性、上下文敏感性等.流敏感的指針分析會區(qū)分指針變量在不同控制流位置的指向信息.上下文敏感性用來反映過程間分析在分析某個過程時,是否會區(qū)分不同調(diào)用點(diǎn)的上下文對過程輸入帶來的不同,從而影響過程的輸出.

1.5 SMT可滿足性問題

可滿足性模理論(satisfiability modulo theories,簡稱SMT)求解器是用來判定一階邏輯公式可滿足性的程序,是許多形式化方法的驗(yàn)證引擎.SMT 求解技術(shù)在有界模型檢驗(yàn)、基于符號執(zhí)行的程序分析、線性規(guī)劃和調(diào)度、測試用例生成以及電路設(shè)計(jì)和驗(yàn)證等領(lǐng)域有著非常廣泛的應(yīng)用[13].

Z3[14,15]是一個由微軟研究院開發(fā)的高性能SMT 求解器,是目前為止綜合求解能力最強(qiáng)的SMT 求解器.因此,本文中引入Z3 約束求解器以幫助Carraybound 能夠更精確地檢測數(shù)組越界缺陷.

2 Carraybound:基于污點(diǎn)分析的數(shù)組越界缺陷的靜態(tài)檢測方法

2.1 方法框架

本文的數(shù)組越界缺陷的檢查方法主要基于靜態(tài)污點(diǎn)分析技術(shù)和數(shù)據(jù)流分析技術(shù),這些方法主要基于程序的抽象語法樹、函數(shù)調(diào)用圖和控制流程圖進(jìn)行分析.本文方法的框架如圖4 所示,首先根據(jù)程序的源碼生成抽象語法樹(AST),再根據(jù)AST 構(gòu)建函數(shù)調(diào)用圖(call graph)和控制流程圖(CFG).然后,基于CFG、AST 和函數(shù)調(diào)用圖,執(zhí)行污點(diǎn)分析以確定可能被污染的數(shù)組下標(biāo).然后,定位所有包含這些被污染的數(shù)組下標(biāo)的數(shù)組表達(dá)式的語句,將數(shù)組下標(biāo)符號化,通過邊界分析得到每個數(shù)組下標(biāo)的邊界信息.接下來,執(zhí)行后向數(shù)據(jù)流分析,并提供簡單匹配和約束求解兩種方法,檢測程序中是否存在相應(yīng)的表達(dá)式保證了數(shù)組下標(biāo)的邊界條件.如果不存在這些表達(dá)式,則報告數(shù)組越界缺陷警報.

Fig.4 The overall framework of our method圖4 方法框架

2.2 數(shù)組長度區(qū)間分析

首先,定位數(shù)組下標(biāo)訪問語句,然后,通過后向數(shù)據(jù)流分析得到所關(guān)注數(shù)組名的別名,進(jìn)而定位到數(shù)組聲明語句,每一個數(shù)組聲明語句對應(yīng)一個相應(yīng)的數(shù)組長度.由于一個數(shù)組可能對應(yīng)多個數(shù)組聲明語句,因此,這一過程將分析得到數(shù)組的長度區(qū)間,具體步驟如下.

數(shù)組長度區(qū)間分析.對于數(shù)組訪問語句arr[idx],在AST 上判斷是否存有數(shù)組聲明大小,如果無法直接獲取數(shù)組聲明大小,則進(jìn)行指針分析,得到arr實(shí)際是某個或者某幾個靜態(tài)數(shù)組或動態(tài)數(shù)組的別名.

本文設(shè)計(jì)了一種流敏感、上下文敏感的按需指針分析.按需是指本文只對所關(guān)注的數(shù)組名(即通過被污染數(shù)組下標(biāo)訪問數(shù)組元素的語句中的數(shù)組名)進(jìn)行指針分析,目的是計(jì)算出數(shù)組名實(shí)際對應(yīng)的靜態(tài)數(shù)組或動態(tài)數(shù)組表達(dá)式.對于每個函數(shù)f,首先,統(tǒng)計(jì)每個基本塊block中包含被污染的數(shù)組下標(biāo)的數(shù)組表達(dá)式,然后從最底層包含關(guān)注數(shù)組表達(dá)式的位置開始,向上進(jìn)行一個后向數(shù)據(jù)流分析,后向數(shù)據(jù)流分析中,使用OutState表示一個基本塊在該基本塊出口時的狀態(tài),是其所有后繼基本塊的InState的并集,如公式(1)所示,此處代表在該基本塊每個所關(guān)注的數(shù)組名對應(yīng)的待分析的指針集合;InState表示一個基本塊在該基本塊入口時的狀態(tài),如公式(2)所示,此處是在其OutState的基礎(chǔ)上,該基本塊的賦值語句根據(jù)下文的指針處理規(guī)則對每個所關(guān)注的數(shù)組名對應(yīng)的待分析的指針集合進(jìn)行殺死(kill)和生成(gen)的結(jié)果.

指針分析時,InState和OutState維護(hù)的是在某一個基本塊中每個所關(guān)注的數(shù)組名arr對應(yīng)的待分析的指針集合AliasSet={p1,p2,…,pn}.初始時,AliasSet={arr}.對于AliasSet中每一個指針p,首先查詢AST 是否可以直接獲取靜態(tài)數(shù)組聲明的大小,如果可以,則將AliasSet中該元素p標(biāo)記為終止點(diǎn),停止對p進(jìn)行指針分析;否則,繼續(xù)對p進(jìn)行指針分析,針對以下賦值語句,后向數(shù)組流分析的具體指針處理規(guī)則為:

·p=malloc(size)將AliasSet中的p替換為malloc(size),并將AliasSet中該元素malloc(size)標(biāo)記為終止點(diǎn),停止對malloc(size)進(jìn)行指針分析.

·p=&a將AliasSet中的p替換為&a.

·p=q將AliasSet中的p替換為q,后續(xù)數(shù)據(jù)流分析繼續(xù)分析q的別名.

·p=*q將AliasSet中的p替換為*q.

·*p=q將AliasSet中的p替換為&q.

·p=g(…)將進(jìn)入函數(shù)g中,從函數(shù)返回語句開始進(jìn)行指針分析.

如果AliasSet中的元素包含&符號,形如&p,則在后續(xù)數(shù)據(jù)流分析中分析對p的賦值表達(dá)式,如果替換的新指針為q,則AliasSet中替換&p為&q,如果新指針為*q,則AliasSet中&p替換為&(*q),即替換為q,以此類推.規(guī)則中將AliasSet中的p替換為q,對應(yīng)著對AliasSet中殺死(Kill)p和生成(Gen)q.

如果在函數(shù)f中沒有定位到數(shù)組名對應(yīng)的數(shù)組聲明語句,則用相同方法分析該函數(shù)的所有調(diào)用者.以此類推,直到定位到數(shù)組聲明語句.由于不同的上下文、不同的分支將導(dǎo)致一個數(shù)組名可能存在多個數(shù)組聲明語句作為別名,其中,每一個數(shù)組聲明語句將對應(yīng)一個數(shù)組長度,因此,對于一個數(shù)組名arr,通過指針分析將得到它的一組數(shù)組長度{s0,s1,…,sn}.為了支持流敏感和上下文敏感,將在數(shù)據(jù)流分析過程中額外記錄:(1)每個基本塊block的后繼節(jié)點(diǎn)集合(計(jì)算方法參照公式(1)),記為succs(block);(2)在分析函數(shù)f時,過程間后向數(shù)據(jù)流分析的函數(shù)調(diào)用鏈,記為succs(f).對于數(shù)組名arr,當(dāng)在指針分析時,在函數(shù)f的基本塊bb中定位到一個arr的數(shù)組聲明語句作為別名時(即AliasSet中的終止點(diǎn)之一記為p0),設(shè)p0對應(yīng)的數(shù)組長度為s0,則將記錄s0對應(yīng)的有效函數(shù)和基本塊信息,有效函數(shù)信息為過程間后向數(shù)據(jù)流分析的函數(shù)調(diào)用鏈,即ValidFuncs(s0)=succs(f),有效基本塊信息為所在基本塊的后繼節(jié)點(diǎn)集合,即ValidBBs(s0)=succs(bb).最終,每個數(shù)組名arr,記錄一組數(shù)組長度{s0,s1,…,sn},且其中每一個數(shù)組長度si記錄該值的作用域,即有效函數(shù)ValidFuncs(s0)=succs(f)和有效基本塊ValidBBs(s0)=succs(bb),并由此推導(dǎo)出每個函數(shù)f的每個基本塊bb中數(shù)組名arr對應(yīng)的數(shù)組長度的集合size(arr,f,bb)={si,sj,…,sk}.

基于每個函數(shù)f的基本塊bb中數(shù)組名arr的數(shù)組長度的集合size(arr,f,bb)={si,sj,…,sk},取其中的最大值記為數(shù)組長度的上界up,取其中的最小值記為數(shù)組長度的下界low,則數(shù)組長度的區(qū)間為[low,up],如果數(shù)組長度為外部輸入的變量,無法確定上下界,則保留長度集合.

示例解析.如圖2 代碼示例,遍歷可知,在函數(shù)f中,共有4 個數(shù)組表達(dá)式的使用位置,即11 行的s.noisy[n]、12 行的arr[2]和16 行的s.arr[i]以及tmp[i].s.noisy[n]和s.arr[i]均為結(jié)構(gòu)體成員數(shù)組,可以直接定位其數(shù)組聲明位置為第3 行、第4 行,繼而可知數(shù)組長度分別為12 和15.tmp[i]的數(shù)組聲明位置為第9 行,數(shù)組長度為3.arr[2]來自于函數(shù)參數(shù),通過指針分析可知,動態(tài)數(shù)組p和q為arr的別名,因此arr數(shù)組長度集合為{j,k}.

2.3 按需污點(diǎn)分析

按需污點(diǎn)分析是指本文中的污點(diǎn)分析只針對程序中的數(shù)組下標(biāo)和數(shù)組長度進(jìn)行靜態(tài)污點(diǎn)分析,包括過程內(nèi)和過程間污點(diǎn)分析.本文將外部輸入(包括用戶或文件的輸入以及主函數(shù)的參數(shù))作為污點(diǎn)源.通過污點(diǎn)傳播,可以得到程序中每個關(guān)注變量v的污點(diǎn)值T(v),可以是被污染(tainted)或者無污染(untainted),即

T(v)∈{tainted,untainted}.

污點(diǎn)值的tainted可以對應(yīng)布爾值1,untainted可以對應(yīng)布爾值0,因此可以使用邏輯運(yùn)算符“或”(記為∨）來計(jì)算污點(diǎn)值的和,即只要有一個子表達(dá)式的污點(diǎn)值為tainted,則整個表達(dá)式的污點(diǎn)值為tainted.

2.3.1 污點(diǎn)傳播規(guī)則

對于污點(diǎn)分析中遇到的每條語句,將按照如下污點(diǎn)傳播規(guī)則計(jì)算該語句的污點(diǎn)值.

常量.每個常量c是非污染的.比如字符串常量、整型常量和浮點(diǎn)型常量等.

T(c)=untainted.

類型轉(zhuǎn)換.類型轉(zhuǎn)換后的表達(dá)式CastExpr(e)的污點(diǎn)值與原來類型的表達(dá)式e的污點(diǎn)值一致.

T(CastExpr(e))=T(e).

數(shù)組下標(biāo)表達(dá)式.將被當(dāng)作一個整體,數(shù)組的某一個元素被污染,則整個數(shù)組為污染的.結(jié)構(gòu)體同理.

T(arr[i])=T(arr),T(expr.elem)=T(expr).

一元運(yùn)算表達(dá)式.op expr的污點(diǎn)值等于其中表達(dá)式expr的污點(diǎn)值.

T(op expr)=T(expr).

二元運(yùn)算表達(dá)式.expr1op expr2 的污點(diǎn)值等于子表達(dá)式expr1 和expr2 的污點(diǎn)值之和.

T(expr1op expr2)=T(expr1)∨T(expr2).

三元運(yùn)算表達(dá)式.expr1?expr2:expr3 的污點(diǎn)值等于子表達(dá)式expr2 和expr3 的污點(diǎn)值之和.

賦值表達(dá)式.賦值語句expr1=expr2 將把右側(cè)表達(dá)式的污點(diǎn)值傳遞給左側(cè)變量.

T(expr1)=T(expr2).

條件語句.ifcthenexpr1 elseexpr2 將把條件語句中條件表達(dá)式c的污點(diǎn)值傳遞給基本塊中的賦值語句中的左值.循環(huán)語句同理,同時,循環(huán)變量的污點(diǎn)值等于循環(huán)上界的污點(diǎn)值.

函數(shù)調(diào)用語句.設(shè)函數(shù)f有n個參數(shù),對f的調(diào)用語句將把第i個實(shí)參pi的污點(diǎn)值傳遞給第i個形參ai.

?i∈[0,n),T(ai)=T(pi).

同時,函數(shù)調(diào)用語句將把被調(diào)用函數(shù)返回值的污點(diǎn)狀態(tài)傳遞給調(diào)用者被賦值的變量.

函數(shù)返回語句.如果返回的是變量,則函數(shù)返回值的污點(diǎn)值等于該變量的污點(diǎn)值;如果返回的是常量(包括返回值為空),則函數(shù)返回值的污點(diǎn)值為untainted.

2.3.2 按需過程內(nèi)污點(diǎn)分析

污點(diǎn)分析前,首先統(tǒng)計(jì)程序中所有與數(shù)組下標(biāo)和數(shù)組長度相關(guān)的函數(shù),以及直到入口函數(shù)的所有調(diào)用者函數(shù),構(gòu)成數(shù)組相關(guān)函數(shù)集合FS.過程內(nèi)的污點(diǎn)分析是對FS中的每個函數(shù)進(jìn)行前向數(shù)據(jù)流分析.對于函數(shù)中的每個基本塊,使用InState表示一個基本塊在該基本塊入口時的污點(diǎn)狀態(tài),是其所有前驅(qū)基本塊的OutState的并集,代表在該基本塊執(zhí)行前所有表達(dá)式的污點(diǎn)狀態(tài);OutState表示一個基本塊在該基本塊出口時的污點(diǎn)狀態(tài),是在該基本塊的InState的基礎(chǔ)上,由該基本塊中的語句按照上一節(jié)中的污點(diǎn)傳播規(guī)則更新表達(dá)式的污點(diǎn)狀態(tài)的結(jié)果,其中,Kill將消除表達(dá)式的污點(diǎn)狀態(tài),Gen將生成表達(dá)式的污點(diǎn)狀態(tài):

對于包含循環(huán)的函數(shù),將迭代計(jì)算每個基本塊的InState和OutState,直到該基本塊的InState和OutState的狀態(tài)不再改變.函數(shù)的污點(diǎn)狀態(tài)與函數(shù)出口基本塊的OutState相同.這樣,就可以得到函數(shù)內(nèi)所有表達(dá)式與相應(yīng)函數(shù)形參之間的污點(diǎn)關(guān)系,即為該函數(shù)f的污點(diǎn)摘要TS(f).

對于每個函數(shù)f,其形參列表為A={a1,a2,…},函數(shù)中每個變量v的污點(diǎn)狀態(tài)記為T(v),其值可能是被污染、無污染或依賴于函數(shù)的形參,即

2.3.3 按需過程間污點(diǎn)分析

首先將入口函數(shù)的參數(shù)標(biāo)記為污染的.然后從入口函數(shù)開始,對FS的所有函數(shù)依據(jù)調(diào)用圖上的拓?fù)漤樞蚍治?通過函數(shù)調(diào)用語句,在調(diào)用點(diǎn)將實(shí)參的污點(diǎn)值傳遞給函數(shù)形參,計(jì)算得到FS中每個函數(shù)形參的污點(diǎn)值.如果有多個函數(shù)調(diào)用同一函數(shù),則被調(diào)用函數(shù)的參數(shù)污點(diǎn)值是其所有調(diào)用者實(shí)參的污點(diǎn)值之和.

對于函數(shù)f的第i個形參,其污點(diǎn)值是f所有調(diào)用者Caller1,…,Callerj相應(yīng)實(shí)參pi的污點(diǎn)值之和,即

當(dāng)需要查詢程序中表達(dá)式的污點(diǎn)狀態(tài)時,如果發(fā)現(xiàn)可以直接得到污點(diǎn)值,則直接返回(tainted/untainted);否則,表示該表達(dá)式的污點(diǎn)狀態(tài)依賴于函數(shù)的形參,此時只需要將所依賴的函數(shù)形參的污點(diǎn)值T(a)代入到公式(5)第3 個賦值中即可得到原表達(dá)式的污點(diǎn)值.

2.3.4 示例解析

如圖2 所示的代碼片段,其中,函數(shù)f的控制流程圖如圖5 所示,圖5 中冒號后的數(shù)字是入口語句的行號.分析可知,4 個數(shù)組表達(dá)式的數(shù)組下標(biāo)為n、2 和i.通過對函數(shù)f進(jìn)行污點(diǎn)分析,可以知道f中的變量n和i的污點(diǎn)值與f的參數(shù)m一致.然后對main函數(shù)進(jìn)行污點(diǎn)分析,argc和argv由外部輸入,因此是污染的.由于main函數(shù)通過參數(shù)argc-1 調(diào)用函數(shù)f,導(dǎo)致函數(shù)f的形參m為污染的.進(jìn)而,f中的變量n和i也是污染的.

Fig.5 CFG of function f in test.c圖5 示例test.c 函數(shù)f 的控制流程圖

2.4 數(shù)組越界缺陷檢測

對于每一條數(shù)組訪問語句arr[idx],數(shù)組arr對應(yīng)的數(shù)組長度列表為{len0,len1,…,lenn},其數(shù)組越界缺陷的檢測結(jié)果記為W(arr[idx]),W(arr[idx])≡T表示該數(shù)組訪問語句會導(dǎo)致數(shù)組越界,W(arr[idx])≡F表示該數(shù)組訪問語句不會導(dǎo)致數(shù)組越界.

判定規(guī)則1.對于數(shù)組訪問語句arr[idx],如果數(shù)組下標(biāo)idx為非污染的,數(shù)組長度列表中任意一個長度為污染的,則該數(shù)組訪問語句會導(dǎo)致數(shù)組越界.

判定規(guī)則2.對于數(shù)組訪問語句arr[idx],如果數(shù)組下標(biāo)idx為非污染的,數(shù)組長度列表中每一個長度都為非污染的,則如果數(shù)組下標(biāo)小于數(shù)組長度列表中的每一個長度,則該數(shù)組訪問語句不會導(dǎo)致數(shù)組越界;否則,該數(shù)組訪問語句會導(dǎo)致數(shù)組越界.

判定規(guī)則3.對于數(shù)組訪問語句arr[idx],如果數(shù)組下標(biāo)idx為污染的,假設(shè)程序中有n條與數(shù)組下標(biāo)idx相關(guān)的語句,構(gòu)成語句序列為S1,S2,…,Sn,將每一條語句轉(zhuǎn)換為約束表達(dá)式,則約束表達(dá)式序列為c1,c2,…,cn,設(shè)第i條語句Si在函數(shù)f的基本塊bb中,此時數(shù)組arr對應(yīng)的數(shù)組下標(biāo)為idxi,數(shù)組長度列表為.如果存在一條語句Si,可以推導(dǎo)出idx大于等于LenSeti中任一長度(公式(8)中的條件A);或者如果存在一條語句Si,可以推導(dǎo)出idx小于0(公式(8)中的條件B);或者對所有語句都不能推導(dǎo)出idx小于LenSeti中所有長度(公式(8)中的條件C)或者大于等于0(公式(8)中的條件D),則該數(shù)組訪問語句會導(dǎo)致數(shù)組越界.如果存在一條語句Si,可以推導(dǎo)出idx小于LenSeti中所有長度(公式(8)中的條件E),并且存在一條語句Sj,可以推導(dǎo)出idx大于0(公式(8)中的條件F),則該數(shù)組訪問語句不會導(dǎo)致數(shù)組越界.

依據(jù)以上3 個判定規(guī)則,本文將參照算法1 對程序進(jìn)行數(shù)組越界檢測.對于每一條數(shù)組訪問語句,首先查詢數(shù)組下標(biāo)的污點(diǎn)值.如果數(shù)組下標(biāo)為非污染的,則根據(jù)判定規(guī)則1 和規(guī)則2 檢測該數(shù)組訪問語句是否會導(dǎo)致數(shù)組越界.如果數(shù)組下標(biāo)為污染的,則通過高精度的后向數(shù)據(jù)流分析,檢測該數(shù)組下標(biāo)是否可能導(dǎo)致數(shù)組越界.后向數(shù)據(jù)流分析時,使用OutState表示一個基本塊在該基本塊出口時的狀態(tài),是其所有后繼基本塊的InState的并集,如公式(4)所示(見第3.2 節(jié)),此處代表在該基本塊待檢查是否會導(dǎo)致數(shù)組越界的數(shù)組訪問語句信息的集合;InState表示一個基本塊在該基本塊入口時的狀態(tài),如公式(5)所示(見第3.2 節(jié)),此處是在其OutState的基礎(chǔ)上,該基本塊的語句根據(jù)判定規(guī)則3 和表1 對待檢查是否會導(dǎo)致數(shù)組越界的數(shù)組訪問語句信息的集合進(jìn)行殺死和生成的結(jié)果.過程內(nèi)后向數(shù)據(jù)流分析從數(shù)組訪問語句所在的基本塊開始,向上遍歷函數(shù)中的每個基本塊,到函數(shù)的入口點(diǎn)結(jié)束.當(dāng)分析完一個基本塊bb后向上分析其前驅(qū)基本塊pred時,將同時根據(jù)bb位于pred的哪個分支,以決定在使用分支語句的條件時是否需要取反.如果在到達(dá)入口點(diǎn)時待檢查語句集合為空,則將終止后向數(shù)據(jù)流分析,否則將繼續(xù)進(jìn)行過程間的后向數(shù)據(jù)流分析.首先,需要根據(jù)程序的函數(shù)調(diào)用圖獲取函數(shù)f的所有父函數(shù).對于每個父函數(shù),遍歷其CFG 并找到調(diào)用數(shù)組函數(shù)f的調(diào)用語句.對于每個數(shù)組邊界條件,如果其下標(biāo)索引與函數(shù)f的形參之一相同,則將獲取相應(yīng)的實(shí)參來構(gòu)造新的數(shù)組邊界條件,見算法interABChecker第7 行.然后在父函數(shù)中繼續(xù)進(jìn)行過程內(nèi)的后向數(shù)據(jù)流分析.過程間后向數(shù)據(jù)流分析過程將一直執(zhí)行,直到待檢查語句集合為空或達(dá)到配置的檢查深度.

Table 1 Types of statements related to array out-of-bound checking表1 數(shù)組越界檢測相關(guān)的語句類型

算法1.數(shù)組越界檢測算法.

如算法1 中函數(shù)checkStmt所示,在數(shù)據(jù)流分析過程中,對于遇到的每一條語句stmt,將根據(jù)表1 和判定規(guī)則3 進(jìn)行處理.如果分析到一條語句可使公式(8)中的條件A或條件E滿足,則后續(xù)數(shù)據(jù)流分析中不再關(guān)注A、C、E;如果分析到一條語句可使公式(8)中的條件B或條件F滿足,則在后向數(shù)據(jù)流分析過程中不再關(guān)注B、D、F.在后向數(shù)據(jù)流分析過程中,主要關(guān)注與數(shù)組下標(biāo)相關(guān)的語句,如表1 的前兩列所示,主要包括包含該數(shù)組下標(biāo)的條件語句(包括循環(huán)條件)和對數(shù)組下標(biāo)的賦值表達(dá)式(包括聲明賦值表達(dá)式和復(fù)合賦值表達(dá)式).其中,聲明賦值表達(dá)式中idx聲明的數(shù)據(jù)類型如果是無符號類型,則公式(8)中的條件F成立,同時,條件B和條件D不成立.本文提供了兩種判斷方法來檢查公式(8)中條件A～F是否滿足,即簡單匹配方法和約束求解方法,將條件A～F統(tǒng)一用ci→(idx op expr)來表示,以下描述中均先假設(shè)數(shù)組訪問語句所在的基本塊條件語句.

簡單匹配處理方法.主要處理包含目標(biāo)數(shù)組下標(biāo)和常量的語句,即條件格式為(idx op const1)→(idx op const2),且當(dāng)其中的兩個操作符op一致時,通過比較兩個常量const1和const2來判斷條件的可滿足性.針對不同類型的語句,如表1 的第3 列所示,具體處理規(guī)則如下.

·賦值語句.只能處理語句為idx=const和idx=expr%const的情形,其中,若idx=const中const大于0,則公式(8)中條件F成立,同時條件B和條件D不成立;同時,如果公式(8)中條件E中的數(shù)組長度len也為常量,且若語句中的常量const小于或等于所有數(shù)組長度len,則條件E成立,同時條件A和條件C不成立;如果語句中的常量const大于任一常量數(shù)組長度len,則條件A成立,報告數(shù)組越界.當(dāng)語句為idx=expr%const時,則只在公式(8)中條件E中的數(shù)組長度len同時也為常量時,若常量const小于或等于所有數(shù)組長度len,則條件E成立,同時條件A和條件C不成立.

·復(fù)合賦值語句.只能處理語句為idx%=const的情形,判定方法與idx=expr%const相同.

·條件語句.只能處理語句條件為idxconst和idx>=const的情形.當(dāng)條件為idxconst時,判定const是否大于-1;當(dāng)條件為idx>=const時,判定const是否大于0.

約束求解處理方法.直接將條件ci→(idx op expr)作為約束,并將約束取反(即!(cond→idx

·賦值語句.如表1 第4 列所示,將賦值語句idx=expr和待檢查的數(shù)組邊界檢查條件idx〈len/idx〉=len/idx＜0/idx＞=0,構(gòu)成!(idx==expr→idx

·復(fù)合賦值語句.如表1 第4 列所示,將復(fù)合賦值語句idx op=expr和待檢查的數(shù)組邊界檢查條件idx＜len,構(gòu)成!(idx1==idx0op expr→idx1＜len)約束交給約束求解器進(jìn)行求解.

·條件語句.當(dāng)遇到“if”語句、“for”語句或“while”語句時,將抽取出語句中的條件expr和待檢查的數(shù)組邊界檢查條件idx

循環(huán)越界檢測.如果在“for”或“while”條件中找不到對相應(yīng)數(shù)組邊界的檢查,那么我們將檢查數(shù)組下標(biāo)是否是循環(huán)變量.如果“for”或“while”條件與模式idx

當(dāng)分析結(jié)束時,將報告數(shù)組越界警報.數(shù)組越界檢查報告主要包括關(guān)于每個數(shù)組下標(biāo)索引的以下信息:文件、行號、函數(shù)及其所在的數(shù)組表達(dá)式,以及待添加的邊界檢查條件.這些信息比較詳細(xì),可以幫助程序員更加方便、快速地定位和確認(rèn)工具報告的數(shù)組越界警報,也可以作為修復(fù)推薦建議提供給程序員作為參考.

示例解析.如圖2 所示代碼,對于數(shù)組訪問語句arr[2],數(shù)組下標(biāo)2 為非污染,數(shù)組長度{j,k}為污染的,根據(jù)判定規(guī)則1,確定為數(shù)組越界缺陷.對于數(shù)組訪問語句s.noisy[n]、s.arr[i]和tmp[i],其數(shù)組下標(biāo)n和i為污染的,將通過后向數(shù)據(jù)流分析并根據(jù)判定規(guī)則3 檢測是否會導(dǎo)致數(shù)組越界.由于結(jié)構(gòu)體中的數(shù)組noisy和arr以及數(shù)組tmp是無符號類型,因此數(shù)組下標(biāo)一定不小于0,只需要檢測是否越出數(shù)組上界.如圖5 所示的CFG,我們從包含數(shù)組表達(dá)式的最底層基本塊Block2 開始執(zhí)行數(shù)組越界檢查,也就是從源碼中的第16 行代碼開始進(jìn)行分析.首先,將遍歷基本塊Block2,未發(fā)現(xiàn)對數(shù)組下標(biāo)邊界的檢查.然后繼續(xù)向上分析,得到Block2 的前驅(qū)塊Block4.接下來,我們得到Block4 的后繼(Block2 和Block3),從而得到Block4 中待檢查的數(shù)組信息,即OutState為16 行的s.arr[i]中i<15、tmp[i]中i<3.由于Block2 在Block4 的false 分支上,所以if 條件為!(i＞=15).由此可以推出i＜15,因此,找到了16 行的s.arr[i]應(yīng)滿足i<15 的邊界檢查,第16 行的s.arr[i]將從待檢查數(shù)組集合中移除.也就是說,Block4的InState是16 行的tmp[i]中的,i<3.然后繼續(xù)向上分析Block5,在Block5 中遇到for 語句時,16 行的tmp[i]中的i恰好為循環(huán)變量,轉(zhuǎn)換為循環(huán)越界問題處理,即在循環(huán)上方檢測循環(huán)上界n是否會超出數(shù)組tmp的長度,即檢測n<4.Block6 中的待檢測數(shù)組信息OutState為16 行的tmp[i]中的n<4,11 行的s.noisy[n]中的n＜12.當(dāng)遇到Block6中的賦值語句時,待檢測數(shù)組信息將更新為16 行的tmp[i]中m＜4,11 行的s.noisy[n]中的m＜12.因此,當(dāng)遇到函數(shù)f的入口時,待檢測數(shù)組信息不為空.如果配置的檢測深度為1,那么將報告數(shù)組越界警告.否則,將執(zhí)行過程間的后向數(shù)據(jù)流分析.

在函數(shù)main中,根據(jù)實(shí)參更新待檢測數(shù)組信息為16 行的tmp[i]中的argc＜5,11 行的s.noisy[n]中的argc＜13.if 語句的條件為argc+2＜15,使用簡單匹配方法,則11 行的p.noisy[n]的數(shù)組邊界檢查條件n<12 可以被滿足,因此,簡單匹配方法中的警報“test.c,line11,p.noisy[n],n＜12”為誤報.但是12 行的循環(huán)上界n應(yīng)小于11 才可以保證15 行的arr[i]中的i＜10,因此,簡單匹配方法和約束求解方法中的警報“test.c,line12,arr[i],n＜11”為真警報.

因此,當(dāng)使用簡單匹配方法進(jìn)行判斷時,無法匹配可以處理的模式,將會報告:

當(dāng)使用約束求解方法進(jìn)行判斷時,可得!((argc+2＜15)→(argc＜13))≡UNSAT,!((argc+2＜15)→(argc＜5))≡SAT,因此將會報告:

3 實(shí)現(xiàn)和實(shí)驗(yàn)評估

本文擴(kuò)展了我們的前期工作[16,17],實(shí)現(xiàn)了一個面向數(shù)組越界缺陷檢測的全自動跨平臺的靜態(tài)分析工具Carraybound,優(yōu)化了按需污點(diǎn)分析,并增加了按需指針分析,從而以此來分析數(shù)組長度的區(qū)間,引入了定理證明器Z3[15],在數(shù)組越界檢測過程中用以解決約束求解問題,工具的架構(gòu)如圖6 所示.該工具可以在Linux 和Windows 系統(tǒng)上運(yùn)行,底層依賴于Clang 3.6 和約束求解器Z3,由數(shù)組長度區(qū)間分析、按需污點(diǎn)分析和數(shù)組越界缺陷檢測共3 個模塊組成.提供了可配置的功能實(shí)現(xiàn)用戶按需調(diào)節(jié)檢測精度,用戶可以配置函數(shù)層數(shù)來控制執(zhí)行過程間數(shù)據(jù)流分析的深度,并通過內(nèi)存優(yōu)化、求解優(yōu)化等措施提升了工具的效率.

Fig.6 Architecture of Carraybound圖6 Carraybound 工具架構(gòu)

3.1 實(shí)現(xiàn)優(yōu)化

內(nèi)存優(yōu)化.大規(guī)模程序總是包含大量AST 文件.如果一次性讀入所有AST 文件,包含AST 文件的所有內(nèi)容,將會消耗大量內(nèi)存.這將會嚴(yán)重制約Carraybound 對大規(guī)模程序的支持.比如,PHP-5.6.16 包含25 萬行源代碼和211 個AST 文件,當(dāng)我們嘗試一次性讀入所有AST 文件時,在2GB 內(nèi)存的機(jī)器上將無法運(yùn)行.為了支持在有限的內(nèi)存資源下掃描10 萬行甚至100 萬行代碼的程序,我們在Carraybound 中實(shí)現(xiàn)了內(nèi)存優(yōu)化策略.內(nèi)存優(yōu)化策略的關(guān)鍵思想是使用一個AST 隊(duì)列僅在內(nèi)存保留最新使用的AST 文件,例如只保留200 個AST 文件.AST 文件越少,內(nèi)存消耗就越少.并且,AST 隊(duì)列的最大容量可以由用戶配置.用戶可以根據(jù)需求和計(jì)算機(jī)容量配置AST 隊(duì)列的最大容量.在分析AST 的內(nèi)容時,Carraybound 將首先檢查相應(yīng)的AST 是否在內(nèi)存中.如果AST 在內(nèi)存中,Carraybound 會將AST 移動到隊(duì)列的末尾.如果AST 不在內(nèi)存中,Carraybound 將從AST 文件讀入AST的內(nèi)容.當(dāng)AST 隊(duì)列達(dá)到其最大容量時,Carraybound 將刪除最先讀入的AST.值得注意的是,如果用戶設(shè)置了一個較小的最大AST 數(shù),Carraybound 將會更加頻繁地讀取AST 文件.因此,如果有足夠的內(nèi)存,用戶應(yīng)選擇更大的最大AST 數(shù),以減少頻繁的讀操作并提高Carraybound 的效率.

求解優(yōu)化.約束求解是非常耗時的,尤其是頻繁地調(diào)用約束求解器將嚴(yán)重增加分析時間,制約工具的可擴(kuò)展性.而在我們的方法中,由于需要計(jì)算不動點(diǎn),會增加對相同約束求解的需求.因此,我們針對Carraybound 分析方法的特征,在使用時進(jìn)行了特殊優(yōu)化.

·結(jié)果緩存.為了減少對約束求解器的調(diào)用,將保存函數(shù)內(nèi)語句是否隱含數(shù)組邊界檢查的結(jié)果列表,首先查詢這個列表,若未查詢到結(jié)果,再調(diào)用約束求解器,這樣可以大大減少對約束求解器的調(diào)用次數(shù).

·快速求解.由于在通過數(shù)據(jù)流分析判斷所遇到的表達(dá)式是否隱含數(shù)組邊界檢查時,總是將!(cond→idx

·時間限制.程序中可能存在一些按位操作及一些其他操作語句,對應(yīng)到Z3 約束求解時可能比較耗時.因此,我們?yōu)閆3 提供了timeout的配置項(xiàng).

3.2 實(shí)驗(yàn)評估

我們對Carraybound 的實(shí)驗(yàn)評估主要試圖回答以下幾個問題.

Q1:Carraybound 的有效性?

Q2:Carraybound 的效率?

Q3:Carraybound 與已有方法/工具的比較?

Q4:Carraybound 發(fā)現(xiàn)真實(shí)缺陷(CVE)的能力如何?

實(shí)驗(yàn)對象和工具.為了評估Carraybound 的有效性,我們選用了幾個常用的開源項(xiàng)目作為實(shí)驗(yàn)對象,見表2.由于在相關(guān)工作的文獻(xiàn)中未發(fā)現(xiàn)可用的工具,因此我們與如下幾個知名的可以檢查數(shù)組越界缺陷的靜態(tài)分析工具進(jìn)行了比較,包含開源靜態(tài)分析工具Cppcheck[18]、商業(yè)靜態(tài)分析工具Checkmarx[19]和HP Fortify[20].Cppcheck 是針對C/C++語言的開源靜態(tài)分析工具,該工具主要檢查未定義行為相關(guān)的程序缺陷,包括除零錯、整型溢出和越界訪問等安全問題[18].Checkmarx 是一個基于源碼的靜態(tài)分析工具,對于被測程序,該工具會首先根據(jù)代碼的元素和流程信息構(gòu)造邏輯圖,然后通過在該圖上進(jìn)行查詢以發(fā)現(xiàn)程序中可疑的安全漏洞和業(yè)務(wù)邏輯問題.HP Fortify 是一個基于規(guī)則的源碼級靜態(tài)分析工具,支持對25 種編程語言的漏洞分析.對這些工具的警報數(shù)目進(jìn)行了統(tǒng)計(jì),結(jié)果見表2,其中,CAB-Simple 為賦值語句簡單匹配處理方法,CAB-Z3 為約束求解處理方法.程序的規(guī)模最大可以達(dá)到200+萬行.我們通過人工審查程序源碼,對表2 中Carraybound 報告的數(shù)組越界檢查警報進(jìn)行了人工確認(rèn),確認(rèn)過程默認(rèn)為兩層函數(shù)調(diào)用.由于其他幾個靜態(tài)分析工具內(nèi)存消耗不易統(tǒng)計(jì),我們僅統(tǒng)計(jì)了其時間開銷,并在表2 的基礎(chǔ)上增加兩個大規(guī)模程序,見表3.由于我們不知道表2 中的程序包含多少個真正的數(shù)組越界缺陷,通過人工確認(rèn)的方式也無法完全確認(rèn)所有警報,因此,為了解答問題4,我們在CVE 中閱讀了與緩沖區(qū)溢出漏洞相關(guān)的報告,找到其中幾個由于數(shù)組越界缺陷導(dǎo)致的緩沖區(qū)溢出的程序以及其修復(fù)后的版本,見表4.

Table 2 Warnings of Carraybound and the compared tools表2 Carraybound 與對比工具的警報統(tǒng)計(jì)

Table 3 Time and memory consumption of Carraybound and the compared tools表3 Carraybound 與對比工具的時間和內(nèi)存開銷

Table 4 Results of checking programs with known out-of-bound CVEs and the repaired programs表4 對包含已知數(shù)組越界CVE 漏洞程序和修復(fù)后程序的檢查結(jié)果

Q1 有效性評估.我們分別統(tǒng)計(jì)了賦值語句簡單匹配處理方法(CAB-simple)和約束求解處理方法(CAB-Z3)的誤報情況,發(fā)現(xiàn)前者的平均誤報率為29.2%,后者的平均誤報率為16.3%.導(dǎo)致約束求解匹配處理方法誤報的主要原因是我們無法處理一些庫函數(shù)調(diào)用,如果在條件語句或者賦值語句中存在庫函數(shù)調(diào)用并保證了數(shù)組邊界,但是我們卻無法判斷從而導(dǎo)致誤報.而賦值語句簡單匹配處理方法相比約束求解匹配處理方法存在更多誤報的原因是前者只簡單匹配一些固定格式的語句并要求語句中特定位置為常量,很多復(fù)雜情形無法處理導(dǎo)致誤報;而通過約束求解我們可以增強(qiáng)條件判斷的能力,除了能處理更多的線性約束,甚至可以處理非線性約束.

Q2 效率評估.為了評估Carraybound 的分析效率,我們統(tǒng)計(jì)了如表3 所示的程序的分析時間和內(nèi)存消耗.約束求解匹配處理方法由于調(diào)用約束求解器,總體會比賦值語句簡單匹配處理方法消耗更多的時間和內(nèi)存.但是時間平均增加了1.53%,內(nèi)存平均增加了0.86%.使用約束求解方法并未造成明顯的時間和內(nèi)存消耗增加.這是因?yàn)?一方面,我們存儲和復(fù)用了約束求解的結(jié)果,避免了冗余的約束求解;同時,我們針對求解expr1→expr2 約束進(jìn)行了專門的優(yōu)化,減少了對約束求解器的調(diào)用;另一方面,由于約束求解可以精確地判斷程序語句是否對數(shù)組邊界進(jìn)行了檢查,可以盡早地移除已經(jīng)被滿足的數(shù)組邊界檢查,從而從總體上能夠節(jié)約開銷.如表3 所示,我們可以發(fā)現(xiàn)賦值語句簡單匹配處理方法和約束求解匹配處理方法在時間和內(nèi)存消耗上都隨著程序規(guī)模的擴(kuò)大,呈現(xiàn)接近線性趨勢的增長,因此我們的方法具有很好的可擴(kuò)展性.

Q3 與已有方法的比較.如表2 和表3 所示,有些工具無法指定只檢測數(shù)組越界缺陷,會有更高的時間開銷,我們不與其進(jìn)行效率比較,這里列出來僅供參考.

·Cppcheck:如圖3 所示的示例,Cppcheck 未報告任何數(shù)組越界相關(guān)的警報.而經(jīng)過實(shí)驗(yàn),類似于“char a[5];a[5]=0;”這樣簡單的數(shù)組越界,該工具是可以報告的.這表明,該工具可能存在一些漏報.同時,針對表2 所列的被測程序,該工具均未報告數(shù)組越界警報.如表3 所示,該工具由于不能指定單獨(dú)檢查越界問題,會消耗較長的時間進(jìn)行檢查其所支持的缺陷類型.

·Checkmarx:如圖3 所示的示例,Checkmarx 未報告任何數(shù)組越界相關(guān)的警報.表2 中所列的被測程序一共報告了617 個數(shù)組越界相關(guān)的警報,其中高風(fēng)險警報25 個,經(jīng)人工確認(rèn)有1 個為可疑的數(shù)組越界缺陷,其余為低風(fēng)險警報,經(jīng)人工確認(rèn)有4 個為可疑的數(shù)組越界缺陷.在人工確認(rèn)其報告時,發(fā)現(xiàn)該工具無法處理和循環(huán)相關(guān)的數(shù)組下標(biāo)訪問問題,即使數(shù)組下標(biāo)為循環(huán)變量,當(dāng)循環(huán)上界為數(shù)組上界時,仍然會誤報數(shù)組越界.如表3 所示,該工具在只選定幾個與數(shù)組越界相關(guān)的缺陷類型進(jìn)行檢測時,仍會消耗較長的時間.我們使用時發(fā)現(xiàn),該工具會消耗很長的時間對源碼進(jìn)行解析以生成該工具的一種中間表示,比如邏輯圖,然后再在該圖上進(jìn)行查詢以檢查缺陷.雖然我們只指定了數(shù)組越界相關(guān)的缺陷類型,但是該構(gòu)建邏輯圖的過程是針對所有類型的缺陷的,因此會消耗較長時間.

·HP Fortify:如圖3 所示的示例,Fortify 只報告test.c 中第11 行p.noisy[n]為緩沖區(qū)溢出警報點(diǎn),而該警報實(shí)際為誤報;并且漏報了test.c 中第15 行arr[i]會因?yàn)榈?2 行的循環(huán)導(dǎo)致數(shù)組越界/緩沖區(qū)溢出.表3 所示的被測程序,該工具報告了大量緩沖區(qū)溢出警報,我們?nèi)斯ずY選出其中與數(shù)組越界相關(guān)的警報,經(jīng)過人工確認(rèn)發(fā)現(xiàn)多數(shù)為誤報,并且多數(shù)情況下,無法處理和循環(huán)相關(guān)的數(shù)組下標(biāo)訪問問題.

Q4 對已知CVE 缺陷的報告比較.見表4,Carraybound 可以對缺陷版本的程序報告相應(yīng)的數(shù)組越界警報,而對修復(fù)后的版本的程序?qū)⒉辉賵蟾鏀?shù)組越界警報.Cppcheck 和Checkmarx 對修復(fù)前后的版本均未報告相應(yīng)的數(shù)組越界警報.而HP Fortify 對Sendmail 程序的修復(fù)前后的版本的報告是正確的,對file 程序的前后版本均未報告,對openjpeg 程序未檢查出該缺陷已被修復(fù).

3.3 實(shí)驗(yàn)討論

上述實(shí)驗(yàn)結(jié)果表明,這些已有的開源和商業(yè)靜態(tài)分析工具均不是專門針對數(shù)組越界檢查的工具,它們的存在可以幫助程序員發(fā)現(xiàn)程序中的各種類型的缺陷.但是這些工具未進(jìn)行精確的數(shù)據(jù)流分析和約束求解,因此對于數(shù)組越界這一類型的缺陷存在大量誤報和漏報.

我們的工具采用數(shù)組長度區(qū)間分析、按需污點(diǎn)分析、精確的數(shù)據(jù)流分析和約束求解,所以有相對更少的誤報和漏報.但在人工確認(rèn)這些靜態(tài)分析工具報告的警報時,我們也發(fā)現(xiàn)了本文工具Carraybound 在實(shí)現(xiàn)上的一些不足,主要包括可擴(kuò)展性和準(zhǔn)確性兩方面的不足.

可擴(kuò)展性.由于約束求解比較耗時,尤其是求解一些復(fù)雜約束,比如一些按位運(yùn)算時,約束求解器將無法在較短的時間內(nèi)給出求解結(jié)果.這將會限制我們工具的可擴(kuò)展性.在實(shí)驗(yàn)時只能通過設(shè)置timeout 時間來跳過一些復(fù)雜的約束求解,但是這樣做又可能會導(dǎo)致該工具的誤報和漏報.

準(zhǔn)確性.影響本文工具Carraybound 準(zhǔn)確性的問題主要包括:

(1)類型轉(zhuǎn)換:C 語言程序中經(jīng)常存在類型轉(zhuǎn)換,我們目前的工具實(shí)現(xiàn)中未能很好地處理該問題,因此可能會導(dǎo)致工具的誤報和漏報.

(2)復(fù)雜循環(huán)越界:有些情形下很難分析出數(shù)組下標(biāo)和循環(huán)上界的關(guān)系,這會導(dǎo)致工具的誤報和漏報.

(3)庫函數(shù):由于采用靜態(tài)分析方法,在不能獲得庫函數(shù)的源碼實(shí)現(xiàn)的情況下,我們將無法判斷這些庫函數(shù)的功能和作用,但是可能這些庫函數(shù)實(shí)現(xiàn)了對數(shù)組邊界的檢查和保證,因此會導(dǎo)致我們的工具產(chǎn)生誤報.

(4)復(fù)雜數(shù)組下標(biāo):程序中存在一些使用復(fù)雜表達(dá)式作為數(shù)組下標(biāo)的情形,會導(dǎo)致工具產(chǎn)生誤報.尤其是對于簡單匹配方法,容易因?yàn)闊o法匹配越界檢查條件,產(chǎn)生誤報.比如數(shù)組下標(biāo)2×i+j,而程序中可能是分別對i和j的范圍約束,無法直接匹配到如2×i+j＜xx的檢查語句,這樣就會導(dǎo)致誤報.目前的工具出于可擴(kuò)展性考慮,對約束求解設(shè)置了timeout 時間,因此復(fù)雜數(shù)組下標(biāo)也會導(dǎo)致約束求解方法的誤報和漏報.比如數(shù)組下標(biāo)為包含按位運(yùn)算的表達(dá)式,將會導(dǎo)致判定準(zhǔn)則中的約束更為復(fù)雜,從而無法在指定時間內(nèi)求解,進(jìn)而導(dǎo)致誤報.

4 相關(guān)工作

4.1 污點(diǎn)分析

動態(tài)污點(diǎn)分析是一種當(dāng)前流行的軟件分析方法.當(dāng)前有很多工作通過進(jìn)行動態(tài)污點(diǎn)分析來追蹤軟件中的隱藏漏洞[10,21-23].污點(diǎn)分析將可能包含惡意數(shù)據(jù)的外部輸入作為污點(diǎn)源,比如網(wǎng)絡(luò)數(shù)據(jù)包;然后,跟蹤這些污點(diǎn)數(shù)據(jù)如何在整個程序執(zhí)行過程中傳播;當(dāng)敏感數(shù)據(jù)(如堆棧中的返回地址或用戶特權(quán)設(shè)置)被污點(diǎn)數(shù)據(jù)污染時執(zhí)行相應(yīng)的處理操作.

與動態(tài)污點(diǎn)分析相比,靜態(tài)污點(diǎn)分析以靜態(tài)方式追蹤源碼或二進(jìn)制文件中的污點(diǎn)信息.STILL[24]是一個基于靜態(tài)污染和初始化分析的防御機(jī)制,可以在各種互聯(lián)網(wǎng)服務(wù)中(例如Web 服務(wù)),檢測嵌入在數(shù)據(jù)流中的惡意代碼.為了減少污點(diǎn)分析的開銷,TaintPipe[9]借助輕量級的運(yùn)行時日志記錄來生成緊湊的控制流信息,并產(chǎn)生多個線程,以流水線的方式并行地執(zhí)行符號化污點(diǎn)分析.靜態(tài)污點(diǎn)分析面對的另一個問題是耗費(fèi)人力.大多數(shù)現(xiàn)有的靜態(tài)污點(diǎn)分析工具會在潛在的易受攻擊的程序位置報錯.這會導(dǎo)致需要開發(fā)者人工確認(rèn)報告,為此需要耗費(fèi)大量的人工成本.Ceara 等人[25]提出了一種污點(diǎn)依賴序列算子,主要基于細(xì)粒度的數(shù)據(jù)流和控制流污點(diǎn)分析,為程序員提供需要被分析的路徑的一些相關(guān)信息.

4.2 指針分析

Andersen 算法[26]和Steensgaard 算法[27]是最具代表性的流不敏感的指針分析算法.Andersen 指針分析方法[26]是一種基于包含的經(jīng)典的C 語言指針指向分析算法,該算法被認(rèn)為是最精確的流不敏感、上下文不敏感的指針指向分析算法.該算法將程序中的直接指向關(guān)系描述為變量與對象之間的約束關(guān)系集合,再通過求解約束關(guān)系集合的傳遞閉包,計(jì)算得到間接的指向關(guān)系,從而獲得所有變量的、完整的指向關(guān)系集合.這種基于包含的思想被廣泛應(yīng)用在后續(xù)的指針指向分析工作中[28].Steensgaard 算法[27]是一種基于等價的指針分析算法,其復(fù)雜度接近于線性復(fù)雜度.但是流不敏感的指針分析將會影響后續(xù)靜態(tài)分析的精度.目前也有一些流敏感的指針分析算法,這些方法通常是基于數(shù)據(jù)流分析[29],比如Emami 算法[30]、Lam 算法[31]、Chase 算法[32]等.本文的流敏感、上下文敏感指針分析是按需分析,即只針對所關(guān)心的數(shù)組名進(jìn)行指針分析.

4.3 數(shù)組越界檢查

Xu 等人[33]提出了一種可以直接在不受信任的機(jī)器碼上進(jìn)行分析的方法,該方法依賴于這些程序的初始輸入的類型狀態(tài)信息和線性約束.Detlefs 等人[34]提出了一種針對常見程序錯誤的靜態(tài)檢查器,包括數(shù)組下標(biāo)越界、空指針解引用和多線程程序中的并發(fā)類錯誤.該方法利用線性約束,自動合成循環(huán)不變量用于邊界檢查.Leroy 和Rouaix[35]提出了一個理論模型,系統(tǒng)地把基于類型的運(yùn)行時檢查放入主機(jī)代碼的接口程序中.Kellogg等人[36]提出了一種在編譯時檢測數(shù)組越界的輕量級驗(yàn)證方法,但是為了達(dá)到線性驗(yàn)證時間,該方法需要開發(fā)者預(yù)先注釋相關(guān)信息,例如程序邊界信息.相比之下,我們的方法能夠分析出程序邊界.ABCD[37]用于按需消除無用的數(shù)組邊界檢查.它平均能夠刪除45%的動態(tài)邊界檢查指令,有時可以實(shí)現(xiàn)接近理想化的優(yōu)化.

當(dāng)前也存在許多靜態(tài)的數(shù)組越界檢測工具[38-40].Chimdyalwar[8]對5 種用于檢查數(shù)組越界的靜態(tài)分析工具進(jìn)行了評估.其中,商業(yè)工具包括Polyspace 和Coverity;學(xué)術(shù)工具為ARCHER,其他兩個是開源工具UNO 和CBMC.Polyspace 是唯一無漏報的工具,但是由于它是內(nèi)存密集型分析,不能以同樣的高精度擴(kuò)展到大規(guī)模程序上.相比之下,Coverity 可以支持百萬行級別的代碼分析,但存在大量誤報.UNO 同時有誤報和漏報,并且不能應(yīng)用在大規(guī)模程序上.ARCHER 宣稱可以運(yùn)行在百萬行級別的代碼上,但是分析并不完善.CBMC 模型檢查器進(jìn)行了精確的分析,無法在大規(guī)模程序上達(dá)到相同精度.Nguyen 等人[39]提出了針對Fortran 語言的數(shù)組越界靜態(tài)檢查方法.Arnaud 等人[38]提出了針對嵌入式程序中數(shù)組越界檢查的靜態(tài)分析方法,該方法處理的程序規(guī)模為20+萬行,我們的方法可以處理百萬行程序.由于該文獻(xiàn)提供的工具CGS 是根據(jù)NASA 程序定制的閉源工具,并且使用了NASA 閉源程序作為被測對象,因此,我們在實(shí)驗(yàn)中沒有與該方法進(jìn)行比較.

4.4 針對數(shù)組越界的緩沖區(qū)溢出檢測

當(dāng)前有很多關(guān)于緩沖區(qū)溢出檢測的工作.大多數(shù)工作在檢測緩沖區(qū)溢出的同時也能檢測數(shù)組越界缺陷.

Tance[41]提出了一種黑盒組合測試方法檢測緩沖區(qū)溢出漏洞.Dinakar 等人[42]提出通過對內(nèi)存進(jìn)行細(xì)粒度的劃分等技術(shù)來降低C/C++程序動態(tài)數(shù)組越界檢查的運(yùn)行開銷.如Loginov[43]和rtcc[44]等基于插樁的方法能在運(yùn)行時檢測是否出現(xiàn)緩沖區(qū)溢出.但是這些方法會引入額外的運(yùn)行時開銷,從而降低測試的效率.例如,Loginov工具的額外開銷高達(dá)900%.SafeC[45]、Cyclone[46]和DangDone[47]使用擴(kuò)展的指針表示,這些擴(kuò)展包含每個指針值的合法目標(biāo)對象的對象基礎(chǔ)信息和大小.使用這些指針要對程序進(jìn)行大量修改以使用外部庫,這些外部庫函數(shù)通常是被包裝好的用于轉(zhuǎn)換指針的方法.此外,編寫這樣的封裝對于間接函數(shù)調(diào)用以及訪問全局變量或存儲器中其他指針的函數(shù)來說可能是難以實(shí)現(xiàn)的.

預(yù)防技術(shù)是一種用于防止數(shù)組下標(biāo)越界被利用的方法.例如,StackGuard[2]可能在檢測到堆棧上的返回地址被覆蓋后終止進(jìn)程.運(yùn)行時預(yù)防的現(xiàn)有方法具有顯著的運(yùn)行時開銷.除此之外,這些方法在可能有漏洞的程序部署完成后生效.CFI[48]檢查程序的控制流程是否在執(zhí)行期間被劫持.這與我們的工作形成對比,我們的工作目的是在部署之前發(fā)現(xiàn)程序中的數(shù)組越界缺陷.

4.5 針對數(shù)組越界的模糊測試

模糊(fuzzing)測試是安全測試中使用最為廣泛的黑盒測試方法之一.該方法在檢測數(shù)組越界或緩沖區(qū)溢出問題中也發(fā)揮著重要作用[49-57].它主要通過程序崩潰檢測數(shù)組越界缺陷.模糊測試通常從一個或多個合法輸入開始,然后隨機(jī)改變這些輸入以獲得新的測試輸入.高級模糊測試技術(shù)[50]是基于生成的模糊測試技術(shù),它為了解決具有復(fù)雜輸入結(jié)構(gòu)的程序的輸入生成問題,通過基于語法的輸入歸約定義有效輸入.Godefroid 等人[51]提出了一種替代的白盒模糊測試方法,結(jié)合符號執(zhí)行和動態(tài)測試生成.雖然模糊測試可以檢測到數(shù)組越界錯誤,但一個主要限制是代碼覆蓋率低.此外,一些數(shù)組越界的錯誤可能只讀取越界的區(qū)域,因此不會導(dǎo)致崩潰,這樣,模糊測試中的監(jiān)視器可能無法檢測到這種情況[52].我們的方法基于靜態(tài)方法,可以實(shí)現(xiàn)高代碼覆蓋,并且可以檢測不同類型的數(shù)組下標(biāo)越界.

5 結(jié)論和未來工作

本文提出了一種基于污點(diǎn)分析的數(shù)組越界缺陷的靜態(tài)檢測方法,并實(shí)現(xiàn)了一個可以在Windows 和Linux操作系統(tǒng)上運(yùn)行的自動化靜態(tài)分析工具——Carraybound.如果程序中存在數(shù)組越界缺陷,我們將報告相應(yīng)的數(shù)組位置和待添加的數(shù)組邊界條件.我們通過掃描一些真實(shí)程序的源代碼來評估Carraybound 工具.實(shí)驗(yàn)數(shù)據(jù)表明,Carraybound 可以快速報告在程序中沒有進(jìn)行數(shù)組邊界檢查的數(shù)組下標(biāo),在使用約束求解方法時,誤報率大約為16.3%.盡管Carraybound 有一些誤報和漏報,但它可以有效地減少程序員人工審查工作.我們的方法可以提供待增加的數(shù)組邊界檢查條件和位置,可以幫助程序員更加方便、快速地定位和確認(rèn)所報告的數(shù)組越界警報,也可以作為修復(fù)推薦建議提供給程序員來參考.

目前,Carraybound 由于庫函數(shù)等原因,可能導(dǎo)致誤報,對于庫函數(shù)有源碼的情況,可以考慮通過函數(shù)摘要等技術(shù)完成更高精度的數(shù)組越界缺陷檢測,對于庫函數(shù)無源碼的情況,可以考慮結(jié)合動態(tài)測試的方法來檢測;另一方面,數(shù)組越界缺陷是一類特殊的緩沖區(qū)溢出缺陷,我們可以考慮擴(kuò)展到對緩沖區(qū)溢出缺陷的檢測,對于常見的緩沖區(qū)溢出相關(guān)API,如strcpy、memcpy,可以通過定義總結(jié)其溢出條件,建立緩沖區(qū)溢出模型,再利用數(shù)據(jù)流分析檢測程序中是否有相應(yīng)的越界檢查語句,從而檢測緩沖區(qū)溢出缺陷.