使用類型限定的系統依賴圖檢測整型錯誤

摘要：目前大多數的源碼安全審計工具在整型錯誤的檢測上具有局限性，往往只能檢測整型溢出類型的漏洞。針對這個問題，對已有的系統依賴圖（system dependence graph，SDG）檢測模型進行了改進，結合類型限定理論提出了基于類型限定的系統依賴圖（type－qualified SDG， QSDG）檢測模型。該模型不僅可以用來檢測C代碼中潛在的絕大多數整型錯誤，而且還能根據其出錯原因將其分類到所定義的八種錯誤類型。與SDG檢測模型僅采用圖同構算法進行檢測相比，先使用類型推斷算法再對QSDG進行檢測可以降低檢測所花費的時間。

關鍵詞：類型限定； 類型推斷； 系統依賴圖； 整型錯誤

中圖分類號：TP393．08

文獻標志碼：A

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

0引言

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

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

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

1類型限定

引入tainted和untainted兩個限定詞，對C語言類型系統作適當的擴展。將程序中所有數據根據其來源，分別標記為tainted和untainted；來自于不可信源的數據被標記為tainted，而程序內部的數據則被標記為untainted。例如untainted int， tainted char*等。

1．1限定詞格

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

1．2類型推斷

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

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

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

1．3函數注釋及多態性

對于標準庫函數進行注釋，采用cqual的預包含文件。但對于其他由系統提供的調用或者應用程序所依賴的其他庫函數則需要由用戶來提供注釋信息。

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

其中：α、β、δ都是限定詞變量。關于函數的多態問題以及多態的原型和內部實現的一致性檢查問題在文獻[2，13]中有更詳細的論述。

1．4類型推斷算法

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

對proc函數內部代碼使用類型推斷之后，產生的新的帶類型限定的C代碼的示意代碼如下：

2類型限定的系統依賴圖

2．1程序依賴圖

程序依賴圖（program dependence graph，PDG）用于表示intra－procedural的中間形式。在依賴圖中，頂點表示語句和預測（也就是程序點）；邊表示控制依賴和數據依賴關系。控制依賴邊使用有向的實線邊表示，而數據依賴邊使用有向的虛線邊表示。

2．2系統依賴圖

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

2．3類型限定的系統依賴圖的定義

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

圖1是proc函數代碼的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正確編碼模式

現在有不少漏洞都是由于程序對整型的使用不當造成的。這類問題包括符號問題、整型溢出等。而且都被證明可能存在嚴重的安全隱患。為了正確地使用整型，所有來自外部的整型輸入在使用之前都必須進行定義和驗證。也就是所有帶tainted限定詞的整型的使用必須：數據依賴于定義；控制依賴于驗證。關于整型正確使用的編碼模式的QSDG圖如圖2所示。

3．2錯誤編碼模式

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

4檢測模型

4．1模型的提出

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

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

4．2檢測算法

對SDG構造算法所生成的QSDG圖進行錯誤檢測，產生最終的分析結果。為了描述算法，首先需要對一些函數進行定義。

定義1get_use_t函數

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

定義2get_val函數

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

定義3get_val_t函數

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

定義4get_def函數

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

定義5get_def_t函數

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

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



對算法具體闡述如下：

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

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

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

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

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

5結束語

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

參考文獻:

[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，FAHNDRICH 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，FAHNDRICH 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.

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