基于污點分析的數組越界缺陷的靜態檢測方法?

(南京大學 計算機科學與技術系,江蘇 南京 210023)

(計算機軟件新技術國家重點實驗室(南京大學),江蘇 南京 210023)

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

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

Fig.1 Statistics of the number of common types of CVE vulnerabilities圖1 CVE 常見類型漏洞的數目統計

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

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

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

本文的主要貢獻包括:

·提出流敏感、上下文敏感的按需指針分析方法,實現數組長度區間分析;提出按需污點分析方法,實現數組下標和數組長度污染情況的計算.

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

·實現了一個靜態分析工具Carraybound,檢測C 程序中的數組越界缺陷(包括由循環導致的數組越界缺陷),并通過實驗展示了工具的有效性.

本文第1 節介紹我們工作的背景知識.第2 節介紹所提出的基于污點分析的數組越界的靜態檢測方法.第3節介紹實現工具Carraybound,并通過實驗展示該工具的有效性和效率,同時討論該工具的不足之處.第4 節介紹相關工作.第5 節進行總結,并提出未來工作展望.

1 背景知識

1.1 數組越界

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

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

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

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

② 緩沖區溢出:包括API 調用和數組下標訪問寫越界導致的緩沖區溢出.比如strcpy(dest,src)和a[5]=0.

本文方法目前側重于數組下標越界(包含循環導致的數組下標越界)問題.對于由API 調用導致的緩沖區溢出問題,我們的另一項緩沖區溢出靜態警報確認的工作重點關注了該類問題[5].

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

①idx=idx % size;

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

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

程序中也可能存在一些復雜的約束和表達式實現了對數組下標的范圍限制,比如按位操作、包含多個運算符的線性運算,甚至是非線性約束.這些情況會加大分析難度,導致傳統方法無法精準地檢查出程序中的數組越界缺陷.

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

Fig.3 Buffer overflow vs.array index out of bound圖3 緩沖區溢出和數組下標越界關系圖

1.2 污點分析

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

1.3 數據流分析

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

1.4 指針分析

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

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

1.5 SMT可滿足性問題

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

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

2 Carraybound:基于污點分析的數組越界缺陷的靜態檢測方法

2.1 方法框架

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

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

2.2 數組長度區間分析

首先,定位數組下標訪問語句,然后,通過后向數據流分析得到所關注數組名的別名,進而定位到數組聲明語句,每一個數組聲明語句對應一個相應的數組長度.由于一個數組可能對應多個數組聲明語句,因此,這一過程將分析得到數組的長度區間,具體步驟如下.

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

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

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

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

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

·p=q將AliasSet中的p替換為q,后續數據流分析繼續分析q的別名.

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

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

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

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

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

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

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

2.3 按需污點分析

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

T(v)∈{tainted,untainted}.

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

2.3.1 污點傳播規則

對于污點分析中遇到的每條語句,將按照如下污點傳播規則計算該語句的污點值.

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

T(c)=untainted.

類型轉換.類型轉換后的表達式CastExpr(e)的污點值與原來類型的表達式e的污點值一致.

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

數組下標表達式.將被當作一個整體,數組的某一個元素被污染,則整個數組為污染的.結構體同理.

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

一元運算表達式.op expr的污點值等于其中表達式expr的污點值.

T(op expr)=T(expr).

二元運算表達式.expr1op expr2 的污點值等于子表達式expr1 和expr2 的污點值之和.

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

三元運算表達式.expr1?expr2:expr3 的污點值等于子表達式expr2 和expr3 的污點值之和.

賦值表達式.賦值語句expr1=expr2 將把右側表達式的污點值傳遞給左側變量.

T(expr1)=T(expr2).

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

函數調用語句.設函數f有n個參數,對f的調用語句將把第i個實參pi的污點值傳遞給第i個形參ai.

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

同時,函數調用語句將把被調用函數返回值的污點狀態傳遞給調用者被賦值的變量.

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

2.3.2 按需過程內污點分析

污點分析前,首先統計程序中所有與數組下標和數組長度相關的函數,以及直到入口函數的所有調用者函數,構成數組相關函數集合FS.過程內的污點分析是對FS中的每個函數進行前向數據流分析.對于函數中的每個基本塊,使用InState表示一個基本塊在該基本塊入口時的污點狀態,是其所有前驅基本塊的OutState的并集,代表在該基本塊執行前所有表達式的污點狀態;OutState表示一個基本塊在該基本塊出口時的污點狀態,是在該基本塊的InState的基礎上,由該基本塊中的語句按照上一節中的污點傳播規則更新表達式的污點狀態的結果,其中,Kill將消除表達式的污點狀態,Gen將生成表達式的污點狀態:

對于包含循環的函數,將迭代計算每個基本塊的InState和OutState,直到該基本塊的InState和OutState的狀態不再改變.函數的污點狀態與函數出口基本塊的OutState相同.這樣,就可以得到函數內所有表達式與相應函數形參之間的污點關系,即為該函數f的污點摘要TS(f).

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

2.3.3 按需過程間污點分析

首先將入口函數的參數標記為污染的.然后從入口函數開始,對FS的所有函數依據調用圖上的拓撲順序分析,通過函數調用語句,在調用點將實參的污點值傳遞給函數形參,計算得到FS中每個函數形參的污點值.如果有多個函數調用同一函數,則被調用函數的參數污點值是其所有調用者實參的污點值之和.

對于函數f的第i個形參,其污點值是f所有調用者Caller1,…,Callerj相應實參pi的污點值之和,即

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

2.3.4 示例解析

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

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

2.4 數組越界缺陷檢測

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

判定規則1.對于數組訪問語句arr[idx],如果數組下標idx為非污染的,數組長度列表中任意一個長度為污染的,則該數組訪問語句會導致數組越界.

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

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

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

Table 1 Types of statements related to array out-of-bound checking表1 數組越界檢測相關的語句類型

算法1.數組越界檢測算法.

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

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

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

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

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

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

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

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

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

循環越界檢測.如果在“for”或“while”條件中找不到對相應數組邊界的檢查,那么我們將檢查數組下標是否是循環變量.如果“for”或“while”條件與模式idx

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

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

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

因此,當使用簡單匹配方法進行判斷時,無法匹配可以處理的模式,將會報告:

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

3 實現和實驗評估

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

Fig.6 Architecture of Carraybound圖6 Carraybound 工具架構

3.1 實現優化

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

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

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

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

·時間限制.程序中可能存在一些按位操作及一些其他操作語句,對應到Z3 約束求解時可能比較耗時.因此,我們為Z3 提供了timeout的配置項.

3.2 實驗評估

我們對Carraybound 的實驗評估主要試圖回答以下幾個問題.

Q1:Carraybound 的有效性?

Q2:Carraybound 的效率?

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

Q4:Carraybound 發現真實缺陷(CVE)的能力如何?

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

Table 2 Warnings of Carraybound and the compared tools表2 Carraybound 與對比工具的警報統計

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

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

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

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

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

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

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

·HP Fortify:如圖3 所示的示例,Fortify 只報告test.c 中第11 行p.noisy[n]為緩沖區溢出警報點,而該警報實際為誤報;并且漏報了test.c 中第15 行arr[i]會因為第12 行的循環導致數組越界/緩沖區溢出.表3 所示的被測程序,該工具報告了大量緩沖區溢出警報,我們人工篩選出其中與數組越界相關的警報,經過人工確認發現多數為誤報,并且多數情況下,無法處理和循環相關的數組下標訪問問題.

Q4 對已知CVE 缺陷的報告比較.見表4,Carraybound 可以對缺陷版本的程序報告相應的數組越界警報,而對修復后的版本的程序將不再報告數組越界警報.Cppcheck 和Checkmarx 對修復前后的版本均未報告相應的數組越界警報.而HP Fortify 對Sendmail 程序的修復前后的版本的報告是正確的,對file 程序的前后版本均未報告,對openjpeg 程序未檢查出該缺陷已被修復.

3.3 實驗討論

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

我們的工具采用數組長度區間分析、按需污點分析、精確的數據流分析和約束求解,所以有相對更少的誤報和漏報.但在人工確認這些靜態分析工具報告的警報時,我們也發現了本文工具Carraybound 在實現上的一些不足,主要包括可擴展性和準確性兩方面的不足.

可擴展性.由于約束求解比較耗時,尤其是求解一些復雜約束,比如一些按位運算時,約束求解器將無法在較短的時間內給出求解結果.這將會限制我們工具的可擴展性.在實驗時只能通過設置timeout 時間來跳過一些復雜的約束求解,但是這樣做又可能會導致該工具的誤報和漏報.

準確性.影響本文工具Carraybound 準確性的問題主要包括:

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

(2)復雜循環越界:有些情形下很難分析出數組下標和循環上界的關系,這會導致工具的誤報和漏報.

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

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

4 相關工作

4.1 污點分析

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

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

4.2 指針分析

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

4.3 數組越界檢查

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

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

4.4 針對數組越界的緩沖區溢出檢測

當前有很多關于緩沖區溢出檢測的工作.大多數工作在檢測緩沖區溢出的同時也能檢測數組越界缺陷.

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

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

4.5 針對數組越界的模糊測試

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

5 結論和未來工作

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

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