使用類型限定的系統(tǒng)依賴圖檢測整型錯誤

摘要：目前大多數(shù)的源碼安全審計工具在整型錯誤的檢測上具有局限性，往往只能檢測整型溢出類型的漏洞。針對這個問題，對已有的系統(tǒng)依賴圖（system dependence graph，SDG）檢測模型進(jìn)行了改進(jìn)，結(jié)合類型限定理論提出了基于類型限定的系統(tǒng)依賴圖（type－qualified SDG， QSDG）檢測模型。該模型不僅可以用來檢測C代碼中潛在的絕大多數(shù)整型錯誤，而且還能根據(jù)其出錯原因?qū)⑵浞诸惖剿x的八種錯誤類型。與SDG檢測模型僅采用圖同構(gòu)算法進(jìn)行檢測相比，先使用類型推斷算法再對QSDG進(jìn)行檢測可以降低檢測所花費的時間。

關(guān)鍵詞：類型限定； 類型推斷； 系統(tǒng)依賴圖； 整型錯誤

中圖分類號：TP393．08

文獻(xiàn)標(biāo)志碼：A

文章編號：1001－3695(2008)06－1850－03

0引言

近年來，越來越多的整型錯誤的安全漏洞被發(fā)現(xiàn)，而且危害巨大。流行的服務(wù)器如IIS、Apach、Sendmail等都曾出現(xiàn)了由于整型溢出而導(dǎo)致的緩沖區(qū)溢出問題，OpenSSH、IE、Linux內(nèi)核中也發(fā)現(xiàn)了多處該類型漏洞。2005年微軟發(fā)布的安全公告中MS05－002、MS05－053、MS05－046以及2006年發(fā)布的MS06－002等都是針對整型溢出漏洞所做的修補(bǔ)。其中，MS05－053在修補(bǔ)的GDI32.DLL中增加了50多處對于整型溢出的檢查。由此可見，整型錯誤已經(jīng)成為一種非常嚴(yán)重的安全隱患。可是到目前為止，專門研究整型錯誤檢測的文章并不多見，大多數(shù)人關(guān)注的焦點仍然集中在與緩沖區(qū)溢出相關(guān)的整型溢出問題的研究上。本文所研究的整型錯誤檢測方法不僅可用于檢測整型溢出問題，還可用于檢測其他類型的整型錯誤。

與本文研究相關(guān)的工作主要包括類型限定理論和整型錯誤的靜態(tài)檢測兩方面。在類型限定詞的研究方面，最早D. Evans[1]在開發(fā)Lclint工具時引入了大量與限定詞類似的注記符，用于檢測C語言中內(nèi)存使用的錯誤。Foster等人[2]較為完整地提出了類型限定詞理論，并描述了一個支持多態(tài)機(jī)制的類型限定詞框架，同時還實現(xiàn)了一個對C語言類型系統(tǒng)進(jìn)行擴(kuò)展的原形系統(tǒng)—cqual。U. Shankar等人[3]將類型限定的方法引入格式化字符串類型漏洞的檢測中，并參考了perl中污點檢查[4]的做法，在C語言的類型系統(tǒng)加入tainted和untainted類型限定詞，通過基于約束的類型推斷來判斷printf函數(shù)的格式串參數(shù)是否能夠通過類型一致性的檢查，如果不能則報告存在格式化字符串漏洞。D. Greenfieldboyce等人[5]在cqual工具的基礎(chǔ)上開發(fā)了一個Eclipse的插件，將類型推斷過程可視化，方便了對程序的理解和漏洞的發(fā)現(xiàn)。

在整型錯誤的檢測方面，人們主要研究了整型溢出的相關(guān)問題。Blexim[6]將整型溢出分為寬度溢出（widthness overflows）、運算溢出（arithmetic overflows）、符號錯誤（signedness bugs）三類，并分別給出這些漏洞的利用方法。O.Horovitz[7]開發(fā)了一個GCC的補(bǔ)丁，增加blip編譯選項，使之能夠檢測與整型值控制的循環(huán)拷貝操作。該方法雖然簡單易行，但有兩方面的不足：會產(chǎn)生大量誤報；不能檢測其他類型的整型錯誤，如設(shè)計缺陷或者缺乏驗證所造成的問題。R. Wojtczuk[8]在UQBT[9]的基礎(chǔ)上開發(fā)了UQBTng工具，用來檢測Win 32的二進(jìn)制文件中存在的整型溢出。UQBTng工具在檢測中為了借助CBMC[10]進(jìn)行屬性檢查，去掉了二進(jìn)制文件中的循環(huán)，導(dǎo)致可能產(chǎn)生誤報，而且與很多其他工具一樣，UQBTng只能檢測整型溢出的類型，使用范圍受限。J.Wilander[11]最先將整型錯誤采用依賴圖的形式進(jìn)行描述，并借助CodeSurfer工具[12]構(gòu)造的系統(tǒng)依賴圖進(jìn)行檢測。他采用的方法是將整型錯誤的分析轉(zhuǎn)換為圖的同構(gòu)問題。眾所周知，該問題是一個NP完全問題。本文提出的方法與J.Wilander的方法[16]不同之處有以下幾點：首先，本文對于整型錯誤模式的描述采用的是基于類型限定的系統(tǒng)依賴圖（本文對基本的系統(tǒng)依賴圖的一個擴(kuò)展）；其次，沒有采用圖同構(gòu)的方法進(jìn)行分析檢測，而是引入類型限定詞對C語言的類型系統(tǒng)作了擴(kuò)展，在對代碼類型推斷的結(jié)果上產(chǎn)生基于類型限定的系統(tǒng)依賴圖；最后分析算法直接對該圖進(jìn)行分析，找出其中可能存在的整型漏洞。

1類型限定

引入tainted和untainted兩個限定詞，對C語言類型系統(tǒng)作適當(dāng)?shù)臄U(kuò)展。將程序中所有數(shù)據(jù)根據(jù)其來源，分別標(biāo)記為tainted和untainted；來自于不可信源的數(shù)據(jù)被標(biāo)記為tainted，而程序內(nèi)部的數(shù)據(jù)則被標(biāo)記為untainted。例如untainted int， tainted char*等。

1．1限定詞格

限定詞tainted和untainted組成格〈L，≤〉。其中：L={tainted， untainted}；偏序關(guān)系T1≤T2表示在期望T1類型對象使用的地方，T2類型對象都可以使用，為了方便，本文也稱T1是T2的子類型。在L中，untainted≤tainted。

1．2類型推斷

筆者的目標(biāo)是將程序所有表達(dá)式中所出現(xiàn)的類型均注釋tainted或者untainted。顯然，這個工作量是巨大的。程序員只可能在程序中關(guān)鍵位置添加一定的注釋，但讓程序員在程序中所有的位置都添加并且維護(hù)注釋是不現(xiàn)實的。所以，必須能夠進(jìn)行類型推斷。

為方便進(jìn)行類型推斷，可以引入兩個推斷規(guī)則：(Q1≤Q2)/(Q1int≤Q2int)（規(guī)則1）；(Q1≤Q2T1=T2)/[Q1ptr(T1)≤Q2ptr(T2)]（規(guī)則2）。其中，對于指針類型采用規(guī)則2進(jìn)行推斷，其他類型則使用規(guī)則1進(jìn)行推斷。

為了進(jìn)行類型推斷，還需引入限定詞變量。首先，在每個出現(xiàn)類型的位置（包括類型定義、變量定義等）都引入限定詞變量。對于函數(shù)而言，函數(shù)f的第i個參數(shù)與限定詞變量f_argi關(guān)聯(lián)，函數(shù)的返回值具有限定詞變量f_ret。特別地，對于指針類型，產(chǎn)生兩個限定詞變量。例如char*x，產(chǎn)生變量x，表示對*x類型的限定；變量x_ p表示對指針的限定。

1．3函數(shù)注釋及多態(tài)性

對于標(biāo)準(zhǔn)庫函數(shù)進(jìn)行注釋，采用cqual的預(yù)包含文件。但對于其他由系統(tǒng)提供的調(diào)用或者應(yīng)用程序所依賴的其他庫函數(shù)則需要由用戶來提供注釋信息。

對于類似getenv函數(shù)比較容易注釋，注釋如下：tainted char *getenv(const char *name)。該定義表示，無論從環(huán)境變量中取任何字符串都是不可信的，返回值必定為tainted。在處理strcat之類的函數(shù)來說，就遇到一點麻煩。這是因為在調(diào)用strcat時，如果傳入的第二個參數(shù)是tainted類型，那么第一個參數(shù)也應(yīng)該是tainted，但反過來，并不存在這種約束。所以文獻(xiàn)[2，13]引入了函數(shù)多態(tài)性。多態(tài)表示函數(shù)不止有一種類型，它是一種上下文相關(guān)的形式。采用多態(tài)的方法，strcat可以定義如下：αchar * strcat(αchar *dst，βconst char* src);where (α≥β)。

其中：α、β、δ都是限定詞變量。關(guān)于函數(shù)的多態(tài)問題以及多態(tài)的原型和內(nèi)部實現(xiàn)的一致性檢查問題在文獻(xiàn)[2，13]中有更詳細(xì)的論述。

1．4類型推斷算法

給定固定大小的限定詞格和n個形如l≤q，q≤l，或者q1≤q2的約束，這里l∈L是一個格元素，而q、q1和q2都是限定詞變量，使用文獻(xiàn)[14]中的算法可以在O(n)中計算出約束。函數(shù)proc的代碼如下：

對proc函數(shù)內(nèi)部代碼使用類型推斷之后，產(chǎn)生的新的帶類型限定的C代碼的示意代碼如下：

2類型限定的系統(tǒng)依賴圖

2．1程序依賴圖

程序依賴圖（program dependence graph，PDG）用于表示intra－procedural的中間形式。在依賴圖中，頂點表示語句和預(yù)測（也就是程序點）；邊表示控制依賴和數(shù)據(jù)依賴關(guān)系?？刂埔蕾囘吺褂糜邢虻膶嵕€邊表示，而數(shù)據(jù)依賴邊使用有向的虛線邊表示。

2．2系統(tǒng)依賴圖

SDG（system dependence graphs）圖最早是由Horwitz等人[15]提出的，其實就是PDG的interprocedural版本。與PDG相比，增加了interprocedural的控制和依賴關(guān)系。對于從函數(shù)A到B的調(diào)用，在A中增加一個call節(jié)點，在B中增加一個入口節(jié)點，并且在A與B之間增加一條interprocedural的控制依賴邊。對于A調(diào)用B傳入和傳出的參數(shù)，分別增加actual－in和actual－out節(jié)點。對于B中所定義的形參則增加formal－in和formal－out參數(shù)，并且增加它們之間的interprocedural數(shù)據(jù)依賴邊。

2．3類型限定的系統(tǒng)依賴圖的定義

QSDG定義為G(VO，VD，VV，VU，VT，ED，EC，EP)。其中：VV、VD、VU分別表示對tainted整型進(jìn)行驗證、定義（也稱做賦值）、使用節(jié)點的集合；VT表示tainted整型的集合；ED表示數(shù)據(jù)依賴邊的集合；EC表示控制依賴邊的集合；EP表示從VV、VD、VU到VT的邊的集合。

圖1是proc函數(shù)代碼的QSDG圖。具體描述如下：VO={V1，V2，V4，V6，V7，V8}，VD={V3，a}，VV={V5}，VU={V7}，VT={V9}，ED={E1，E2，E3，E4，E5，E10，E11}，EC={E6，E7，E8，E9}，EP={E12，E13，E14}。

3整型錯誤

3．1正確編碼模式

現(xiàn)在有不少漏洞都是由于程序?qū)φ偷氖褂貌划?dāng)造成的。這類問題包括符號問題、整型溢出等。而且都被證明可能存在嚴(yán)重的安全隱患。為了正確地使用整型，所有來自外部的整型輸入在使用之前都必須進(jìn)行定義和驗證。也就是所有帶tainted限定詞的整型的使用必須：數(shù)據(jù)依賴于定義；控制依賴于驗證。關(guān)于整型正確使用的編碼模式的QSDG圖如圖2所示。

3．2錯誤編碼模式

文獻(xiàn)[11]歸納了八種整型編碼的錯誤模式。圖3描述了其中三種。本文雖然采用了與文獻(xiàn)[11]相同的八種錯誤編碼模式，但在錯誤編碼模式的描述上是不同的。文獻(xiàn)[11]采用的是基本的SDG圖描述，而本文采用的是QSDG圖描述。

4檢測模型

4．1模型的提出

本文檢測模型主要包括解析器、類型推斷器、QSDG構(gòu)造和分析引擎四個部分。模型的輸入主要包括限定詞格、待分析的C代碼以及預(yù)包含文件。其中，限定詞格文件主要描述了用戶感興趣的類型限定詞。目前，限定詞格文件只包含了tainted和untainted組成的限定詞格，保留這樣一個配置文件的輸入接口是為了方便以后的擴(kuò)展。預(yù)包含文件中包含的是使用1.3節(jié)中所闡述的方法進(jìn)行注釋的函數(shù)聲明，可以是預(yù)定義的庫函數(shù)，也可以是用戶添加在待分析的C代碼中要用到的函數(shù)注釋聲明。模型的輸出信息包括整型類型錯誤的個數(shù)及在代碼中的位置信息。系統(tǒng)結(jié)構(gòu)如圖4所示。

整個模型的工作過程描述如下：用戶將限定詞格和C代碼以及預(yù)包含文件輸入解析器；在對代碼進(jìn)行詞法解析之后，類型推斷器依照1.4節(jié)中的類型推斷算法，對C代碼進(jìn)行類型推斷，并將推斷后的結(jié)果作為QSDG構(gòu)造算法的輸入；分析引擎讀取QSDG進(jìn)行檢測，輸出結(jié)果。

4．2檢測算法

對SDG構(gòu)造算法所生成的QSDG圖進(jìn)行錯誤檢測，產(chǎn)生最終的分析結(jié)果。為了描述算法，首先需要對一些函數(shù)進(jìn)行定義。

定義1get_use_t函數(shù)

get_use_t(x)={y|〈y，x〉∈EP and y∈VU}。其中：x∈VT，該函數(shù)表示得到使用tainted整型變量x的節(jié)點集合。

定義2get_val函數(shù)

get_val(x)={y|〈y，x〉∈EC and y∈VV}。該函數(shù)表示得到節(jié)點x的控制依賴節(jié)點集合與驗證節(jié)點集合VV的交集。

定義3get_val_t函數(shù)

get_val_t(x)={y|〈y，x〉∈EP and y∈VV}。該函數(shù)表示得到對tainted整型變量x進(jìn)行驗證的節(jié)點集合。

定義4get_def函數(shù)

 get_def(x)={y|〈x，y〉∈ED and y∈VD}。該函數(shù)表示得到節(jié)點x的數(shù)據(jù)依賴節(jié)點集合與定義節(jié)點集合VD的交集。

定義5get_def_t函數(shù)

get_def_t(x)={y|〈x，y〉∈EFandy∈VD}。該函數(shù)表示得到對tainted整型變量x進(jìn)行定義的節(jié)點集合。

采用QSDG圖進(jìn)行錯誤類型檢測，其分析算法主要步驟如下：



對算法具體闡述如下：

a）對于VT中的每個節(jié)點x，將VU中所有指向x的節(jié)點放入集合M。

b）對于M中的每個節(jié)點找出其控制依賴節(jié)點集合和VV中指向x的節(jié)點集合的交集L。

c）如果L不為空，則對于L中的每個節(jié)點λ找出其數(shù)據(jù)依賴節(jié)點集合和VD中指向x的節(jié)點集合的交集S。

d）如果S不為空，則對于S中的每個節(jié)點s驗證〈s， x〉是否是ED中的邊。如果都滿足則返回true；否則返回1。

e）其他情況，均返回1。返回1將進(jìn)一步進(jìn)行八種錯誤類型的判定，由于篇幅所限不再贅述。

5結(jié)束語

本文模型在檢測八類整型使用錯誤時，依據(jù)的是〈use〉〈def〉〈val〉之間的依賴關(guān)系，但并沒有對〈val〉節(jié)點中的驗證進(jìn)行有效性判定。也就是說，〈val〉進(jìn)行的驗證是否真正有意義，或者說是否充分并不知道，這就需要引入整型范圍約束分析進(jìn)行進(jìn)一步的研究。另外還有一個問題，在類型推斷時采用上下文無關(guān)的分析。下一步還要研究如何改進(jìn)類型推斷的算法，使之做到上下文相關(guān)分析，進(jìn)一步提高分析的精度。

參考文獻(xiàn):

[1]EVANS D. Static detection of dynamic memory errors[C] //Proc of the 11th ACM SIGPLAN Conference on Programming Semantics. Philadelphia:[s.n.]，1996:44－52.

[2]FOSTER J S，F(xiàn)AHNDRICH M，AIKEN A. A theory of type quali－fiers[C] //Proc ofACM SIGPLAN Conference onProgramming Language Design and Implementation(PLDI’ 99). Atlanta:[s.n.]， 1999:192－203.

[3]SHANKAR U，TALWAR K， FOSTER J S， et al. Detecting format string vulnerabilities with type qualifiers[C] //Proc of the 10th Usenix Security Symposium. Washington D C: [s.n.]， 2001:23－32.

[4]Perl security[EB/OL].[2004－07]. http://www.perl.com/pub/doc/manual/html/pod/perlsec.html.

[5]GREENFIELDBOYCE D， FOSTER J S.Visualizing: type qualifier inference with Eclipse[C] //Proc of OOPSLA， Workshop on eclipse Technology Exchange. 2004.

[6]BLEXIM. Basic integer overflows[EB/OL]. (2002－08－04) [2007－05－30]. http://www.theparticle.com/files/txt/hacking/phrack/p60－0x0a.txt.

[7]HOROVITZ O. Big loop integer protection[EB/OL]. (2002－08－04) [2007－05－30]. http://www.theparticle.com/files/txt/hacking/phrack/p60－0x09.txt.

[8]WOJTCZUK R. UQBTng: a tool capable of automatically finding integer overflows in Win32 binaries[EB/OL]. (2005－11－13) [2007－06－03]. http://events.ccc.de/congress/2005/fahrplan/attachments/552－Paper_ATool Capable Of Automatically Finding Integer OverflowsIn Win32－Binaries.pdf.

[9]CIFUENTES C， EMMERIK M Van. UQBT: a resourceable and retargetable binary translator[EB/OL].[2007－04－07]. http://www.itee.uq.edu.au/~cristina/uqbt.html.

[10]KROENIN D. Bounded model checking for ANSI－C[EB/OL]. [2007－05－22].http://www.cs.cmu.edu/~modelcheck/cbmc.

[11]WILANDER J.Modeling and visualizing security properties of code using dependence graphs[C] //Proc of the 5th Conference on Software Engineering Research and Practice(SERPS’05). Vasteras:[s.n.]，2005:28－37.

[12]GrammaTechInc. CodeSurfer[EB/OL].[2007－06－28].http://www.grammatech.com.

[13]REHOF J，F(xiàn)AHNDRICH M. Type－based flow analysis:from polymorphic subtyping to CFL reachability[C] //Proc of the 28th Annual ACM SIGPLAN－SIGACT Symposium on Principles of Programming Languages. London:[s.n.]， 2001.

[14]HENGLEIN F，REHOF J. The complexity of subtype entailment for simple types[C] //Proc of the 12th Annual IEEE Symposium on Logic in Computer Science. Warsaw:[s.n.]， 1997:352－361.

[15]HORWITZ S，REPS T， BINKLEY D. Interprocedural slicing using dependence graphs[J]. ACM Trans on Programming Languages and Systems， 1990， 12(1):26－60.

[16]WILANDER J， FAK P. Pattern matching security properties of code using dependence graphs[C] //Proc of the 1st International Workshop on Code Based Software Security Assessments(CoBaSSA). Pittsburgh:[s.n.]， 2005:5－8.

注：本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文