本站簡介作品介紹購買指南發布作品訂做說明專業誠信
本站收錄了大量的畢業設計和論文 [vison]       本站提供這些設計的初衷 [vison]      
管理系統 學生 計算機 教學 信息 電路 模具 汽車 網站 建筑
您現在的位置:首頁 >> 理工論文計算機信息

CBOC:一個C語言緩沖區溢出漏洞有效檢測工具

編輯:admin 來源:papersay.com

- 1 -
CBOC:一個C 語言緩沖區溢出漏洞有效檢測工具1
陳石坤 1,李舟軍2
1 國防科技大學計算機學院,長沙 (410073)
2 北京航空航天大學計算機學院,北京 (100191)
E-mail:[email protected]
摘要:沖區溢出是C 程序中很多安全問題的根源。本文給出一個C 語言緩沖區溢出漏洞
的有效檢測工具CBOC(C Buffer Overflow Checker)。該工具基于符號執行,并引入基址
安全表達式的概念,優化了符號執行過程。CBOC 以C 程序源代碼作為輸入,能夠自動檢
測程序中包含的緩沖區溢出漏洞。使用CBOC 對公開的基準程序測試包進行檢測,并在相
同條件下和主流的ANSI-C 限界模型檢驗工具CBMC 進行了比較。實驗表明:對于大多數
測試用例,CBOC 的性能優于CBMC,且CBOC 使用內存較少。在檢測精度的測試實驗中,
CBOC 誤報率約為0.34%,漏報率約為1.72%。
關鍵詞:緩沖區溢出; 符號執行; 基址安全表達式
1. 引言
緩沖區溢出發生在將數據D寫入到緩沖區B,而D的長度比分配給緩沖區B的長度大的時
候。在沒有顯式邊界檢查的編程語言中,緩沖區可能被不受限制地越界讀寫。C語言允許直
接操作指針而不作邊界檢查,標準C庫中包含很多函數,如果使用不當,它們就可能導致緩
沖區溢出問題。這使得緩沖區溢出成為C語言程序中很多安全問題的根源。
緩沖區溢出漏洞主要被攻擊者利用來執行任意的代碼(比如,一個具有管理員權限的
shell)。在C語言中,函數調用時,被調函數的參數、返回地址以及函數內部定義的局部變
量將先后被壓入棧中,棧由高地址向低地址增長。當函數中的一個局部緩沖區溢出時,它將
會由低地址向高地址覆蓋相鄰的數據,這將有可能覆蓋函數的返回地址。攻擊者可以精心設
計一段數據來覆蓋棧空間,改寫函數的返回地址,讓返回地址指向一段打開shell的代碼,從
而獲取管理員的權限。
緩沖區溢出漏洞檢測方法一般分為動態[1,2]和靜態[3-8]兩類。動態檢測方法,需要在程序
中插入動態檢測代碼或斷言,在程序的執行過程中及時發現緩沖區溢出漏洞。這類方法增加
了程序的執行開銷,也不能證明系統中不存在緩沖區溢出漏洞。而靜態方法從分析程序的源
代碼入手,在軟件發布和運行之前就能發現和確定軟件的安全漏洞,可直接應用到軟件開發
階段,以提高軟件質量。
目前,主要的靜態分析方法通常將緩沖區溢出問題轉換為約束求解問題:例如,將緩沖
區溢出問題轉換為整數范圍分析問題[3]。受限于整數范圍分析的精度,這種方法可能產生大
量的誤報,同時,這種方法幾乎完全沒有考慮指針別名,這也會導致大量的誤報或漏報;將
緩沖區溢出問題轉換為整數線性規劃問題[4]。由于流敏感的指針分析計算復雜度較高,該方
法采用了流不敏感的指針分析算法,并最終導致系統產生大量誤報。在上述兩種分析方法中,
所發現的緩沖區溢出問題必須通過進一步的手工檢測來驗證其是否確實是一個真實的漏洞。
CSSV [5]是一個緩沖區溢出檢測工具,利用它可以發現程序中包含的所有由字符串操作
1本課題得到高等學校博士學科點專項科研基金(項目編號:20070006055)的資助。
計算機畢業設計網http://www.pdzuhx.tw
- 2 -
導致的緩沖區溢出漏洞。該工具對軟件中的每個函數單獨進行分析,需要程序員為每個函數
提供前置條件、后置條件以及可能的副作用。該方法僅產生少量的誤報。然而,它的分析過
程需要手工為函數提供合同(前置、后置以及副作用申明),難以保證函數與它的合同的一
致性,并且不能全自動地進行檢測。
模型檢驗方法具有可靠性和完備性,理論上能保證沒有誤報和漏報,并且能全自動地實
行。文獻[6,7] 嘗試使用模型檢測工具ComFoRT來證明軟件系統中不包含緩沖區溢出漏洞。
然而,ComFoRT本身對指針提供的支持也很有限 [6]。
CBMC [8]是目前使用較為廣泛的C語言限界模型檢驗工具。它支持ANSI-C的所有特性,
包括指針操作,復雜的數據結構,存儲空間動態分配,函數遞歸調用等。它能夠對程序中的
一些安全屬性進行檢測,包括數組越界訪問,除0錯誤,空指針,算術溢出以及用戶自定義
的斷言等。然而,對一些常用的C語言指針表達式(可能不符合ANSI-C標準,但對緩沖區溢
出檢測至關重要),CBMC沒有提供充分的支持。例如:設x是一個類型為struct {int a; int b;}
的結構體變量,CBMC最近版本(2.8版)將認為表達式*((int*)((char*)&x+sizeof(int)))是非法
的。實際上該表達式常被用于訪問x.b。
從以上分析可以看出,C程序中的指針和指針表達式給C語言程序分析工具帶來很大挑
戰。實際上,即使對最常用的數組,常用的C語言模型檢驗工具SLAM[9]和BLAST[10]都不能
提供很好的支持。
本文給出一個C語言緩沖區溢出檢測工具CBOC(C Buffer Overflow Checker)。該工具
使用符號執行[11]的方式檢測C程序中的緩沖區溢出漏洞。使用經典的符號執行算法處理C語
言程序時,同樣會遇到一些與指針相關的棘手問題,包括:數組元素的混淆,復雜的數據結
構,指針與引用的混淆等,也難以處理程序中出現的循環。CBOC引入基址安全表達式的概
念,基址安全表達式的等價性可以方便的從形式上進行判斷,依據這一特性CBOC對符號執
行過程進行了優化,從而緩解了指針、數組等給程序分析帶來的復雜度。使用公開的緩沖區
溢出漏洞測試包對CBOC進行評測,并在相同條件下和CBMC進行比較。實驗結果表明:對
于大多數測試用例,CBOC的性能都優于CBMC,且CBOC使用內存較少。采用一個包含1164
個代碼片段的緩沖區溢出漏洞測試包對CBOC的誤報率和漏報率進行評測,結果表明:CBOC
的誤報率和漏報率都很低。
本文以下章節安排如下:第二節簡單介紹緩沖區溢出的形成機理;第三節介紹CBOC的
系統結構;第四節介紹CBOC中使用的關鍵技術;第五節給出一些實驗分析結果;最后一節
總結全文。
2. 緩沖區溢出漏洞
緩沖區溢出通常可以分為棧溢出、堆溢出、格式化串溢出等多種類型,而按照溢出產生
的原因往往還可以進一步分為整數寬度溢出、整數算術溢出、整數符號問題以及數組越界等
多種類型。本節以棧溢出為例,介紹緩沖區溢出漏洞的形成機理。
棧溢出發生在函數調用過程中,通過覆蓋函數的返回地址重定向程序的控制流。程序執
行過程中,通常將局部數據和函數調用現場保存在棧中。棧由高地址向低地址增長(與字符
串增長方向相反)。函數調用過程大致如下:(1)

www.pdzuhx.tw
函數入口參數逆序入棧;(2) 指令指針EIP
入棧,作為函數的返回地址RET;(3) 當前棧頂指針EBP入棧,以便在函數調用返回時恢復
棧狀態;(4) 函數局部變量入棧;(5) 執行函數體;(6) 函數返回。圖 1 給出一個典型的棧
溢出例子:當函數func中的strcpy執行完后,str中的內容(128個字符)將覆蓋由buf_dest開
計算機畢業設計網http://www.pdzuhx.tw
- 3 -
始的128個字節,函數func的返回地址將被覆蓋。通過精心設計str的內容,可將函數func的
返回地址覆蓋為一段惡意代碼的地址。函數返回時控制流就會定向到惡意代碼上。
圖1 棧溢出
Fig.1 Stack overflow
C庫中的一些函數,如果使用不當,它們將可能導致緩沖區溢出。這類函數包括gets,
strcpy, strcat, sprintf,memcpy, strncpy等。
3. CBOC 的系統結構
CBOC使用Ocaml語言開發,運行在Window平臺上(需要Cygwin支持),也可以編譯為
linux的可執行程序。CBOC提供命令行執行方式,同時以Eclipse插件的方式提供了一個圖形
界面。圖形界面需要Eclipse(v3.42)和CDT(v5.02)支持。
CBOC包括如下六個主要的功能模塊:
1)存儲表達式簡化模塊Simplemem,其主要功能為:通過合理地引入臨時變量對程序
進行變換,在變換后的程序代碼中,表達式中的每一個變量至多只會包含一重間接訪問,并
使用明確的常數來替換sizeof、alignof等系統相關的常量。
2)無關語句裁剪模塊Astslicer和Slicer,其主要功能為:裁剪未被調用的函數及與緩沖
區溢出無關的語句。
3)表達式規范模塊Normalexp,用于將程序中的表達式化為規范型表達式。
4)文法轉化模塊Csg,它是一個輔助模塊,使用一種簡潔的表達式文法來存儲和索引
符號執行過程中的表達式。
5)順序語句序列符號化執行模塊Secsg,該模塊是CBOC的重要模塊之一,它根據變量
及函數的定義建立緩沖區初始化信息,符號執行不包含分支的順序路徑,在符號執行過程中,
判定路徑是否可達,并判定路徑中的斷言是否成立。在它提供的主接口中,有2個接口是關
鍵接口,分別是assign和assume。接口assign為當前正在執行的符號化路徑增加一條待執行的
賦值語句。接口assume為當前正在執行的符號化路徑的路徑條件增加一個新的斷言;
6)程序執行路徑動態擴展模塊Symex,該模塊是CBOC的另一個重要模塊,它動態地進
行循環展開和函數內嵌,擴展程序執行路徑,并調用Secsg模塊完成程序的符號化執行,根
據Secsg的反饋來判斷路徑是否可達,當發現路徑不可達時停止對當前路徑進行擴展,轉而
執行一條新的符號化路徑。當Secsg報告溢出漏洞時,記錄Secsg反饋的錯誤路徑。
計算機畢業設計網http://www.pdzuhx.tw
- 4 -
圖2給出CBOC進行漏洞檢測的工作流程。CBOC首先讀入待檢測的C程序源文件列表,
啟動GCC對列表中的程序文件進行預處理,主要是進行宏擴展。隨后CBOC讀入預處理后得
到的程序代碼文件,進行必要的變量重命名,將這些文件合并成為一個程序文件,進行無關
語句裁剪,表達式化簡。最后,對程序進行符號執行,檢測程序中的緩沖區溢出漏洞。
圖2 CBOC 工作流程
Fig.2 Workflow of CBOC
4. 關鍵技術
4.1 程序代碼預處理技術
CBOC中使用的很多關鍵技術均假設程序代碼已經做過必要的預處理。這里對CBOC中
需要作的預處理加于說明。
C語言是一種非常靈活的編程語言,它可以方便地執行直接面向硬件的操作,這些特性
同時也導致C語言難于理解和分析。將C語言轉化為一種方便分析的中間語言,可以使程序
分析工具從靈活而復雜的C語言語法中解脫出來。CIL(C Intermediate Language) [12]是berkeley
大學開發的開源軟件。CIL定義了C語言的一個簡潔(clean)、規范的子集,支持ANSI-C的
全部特性,并為GCC和MSVC提供部分擴展支持。CBOC采用CIL作為前端,對C程序進行解
析,并作必要的預處理。首先CBOC調用編譯器GCC或CL對程序進行宏擴展。程序中通常
采用#define,#ifdef等指令定義一些宏,使用編譯器提供的宏擴展功能(例如,-E參數可以
讓gcc提供宏擴展功能)可以將代碼中的宏替換成其對應的常量或語句。隨后,CBOC對程
序中的控制流結構和表達式進行簡化。CBOC借助CIL提供的庫函數來實現這些功能。CIL
提供了幾個比較重要的功能,包括:消除表達式的副作用:將局部變量定義中的初始化轉化
為等價的賦值語句;將條件表達式 “?:”轉化為等價的if…else結構;將各種循環(while,for
以及do)統一轉換為while循環;進行必要的變量重命名,將多個程序文件合并為一個;通過
合理地引入臨時變量對程序進行變換,消除程序中的多重指針解引用。消除多重解引用后,
對任意的程序變量x,只允許x,&x和*x出現在程序中,而**x,***x…等都被等價的表達式
計算機畢業設計網http://www.pdzuhx.tw
- 5 -
所替換。CBOC還借助CIL將Switch語句轉化為if..else if…else..結構,將break轉化為等價的
goto語句,將continue轉化為一個等價的goto語句。
4.2 循環處理技術
CBOC借鑒限界模型檢驗中的思想,即只檢查有限長的路徑上的狀態來發現錯誤。因此,
程序中的循環將被展開,并用if…else語句替換。對于while循環W,若W的循環的遍數是常
量或常量表達式n,就將W的循環體復制n遍。否則,展開的遍數可以用事先設定的參數控制。
例如,假設循環為while(cond) { Body; },參數設定的展開次數為2,我們將循環體復制2遍。
變換后代碼為:if(cond) { Body; if(cond) { Body; assert(!cond); } } 。其中assert(!cond)稱為展
開斷言,如果循環展開不充分(實際的循環遍數大于2),程序驗證時,該展開斷言將被違
背。利用該斷言,可以通過逐步調整參數,加大展開遍數,在更長的路徑上查找錯誤。對于
向后的goto語句(跳轉目標在該goto語句之前),使用類似while循環的方式展開。向前的goto
可以使用等價的if…else語句替換。CBOC在實現時并不靜態地復制程序代碼來展開循環,而
是由symex模塊

www.pdzuhx.tw
動態產生符號化執行路徑。
4.3 函數調用的處理技術
對于有源代碼的函數調用,采用過程內嵌的方式進行處理,即,在函數調用的地方,復
制函數體,經過必要的變量重命名,使用函數體本身來代替函數調用。若函數將返回值賦給
一個左值表達式,則使用等價的賦值語句替換Return語句。遞歸函數可采用類似循環展開的
方式進行擴展,但目前的CBOC版本尚不支持函數遞歸調用。沒有源代碼的函數將被分為兩
類:一類是strcpy,strcat,fgets等字符串操作函數,以及malloc和free等存儲管理函數,為了
檢測緩沖區溢出漏洞,需要對此類函數提供特別的支持,我們將在后面的章節介紹對這些函
數的處理。另一類是普通函數,這類函數被處理成非解釋函數(uninterpreted functions),即,
對于函數F(x,y),僅有如下假設成立:若x1=y1且x2=y2,則F(x1,x2)=F(y1,y2)。這里CBOC沒
有考慮這類函數的副作用。
4.4 基址安全表達式
C語言程序中頻繁地使用到指針,指針和指針運算是緩沖區溢出漏洞中至關重要的因
素。指針變量的解引用可以通過指針分析來進行處理。如果計算出指針變量的指向關系,則
可在對指針進行解引用的地方進行指向集替換。例如,若已知p的指向集為{x,y},則*p可以
由&x,&y來替換,語句i=*p可以替換成 if(p==&x) i=x; else if(p==&y) i=y; else assert(0)。然
而,指針分析問題是NP-完全問題,當允許動態內存分配、遞歸數據結構、循環和分支時,
指針分析問題甚至是不可計算的。另外,C語言復雜的語義導致可靠的指針分析可能產生大
量虛假的指向關系。為了減少誤報,現有的很多軟件驗證工具常常使用不可靠的指針分析。
例如:在廣泛用于操作系統錯誤檢查的Metal編譯器和Intrinsa系統中,兩個指針互為別名,
當且僅當這兩個指針被證明指向相同位置或對象。在緩沖區溢出檢測中,很多檢測工具也遵
循了上述原則。然而,使用不可靠的指針分析導致緩沖器溢出檢測工具不能保證檢測的可靠
性(產生誤報)。
指針表達式解引用更加難以處理。指針的存在使得程序訪問的空間不是平坦的,考慮到
效率和可實現性等因素,很多程序分析工具都不支持或者僅有限支持指針和指針表達式。即
使最常用的數組也會給程序分析工具(尤其是基于謂詞抽象的工具,如:BLAST和SLAM)
帶來很大挑戰。包括CBMC在內的很多程序分析工具將數組看作一個整體進行更新,更新數
計算機畢業設計網http://www.pdzuhx.tw
- 6 -
組的一個元素時,需要對整個數組進行更新。例如,設A是一個包含兩個元素的數組。語句
A[x]=10將被替換成語句序列A[0]=(x==0)?10:A[0]; A[1]=(x==1)?10:A[1].來執行。
CBOC引入基址安全表達式的概念,基址安全表達式的等價性可以從形式上方便地進行
判斷,這就為符號執行過程提供了較大的優化空間。本節詳細討論基址安全表達式。
4.4.1 規范型左值表達式
C語言中,表達式分為左值表達式和右值表達式,左值表達式同時也是右值表達式。只
有左值表達式對應到程序中實際的存儲塊,可以出現在賦值符號的左邊。CBOC所采用的表
達式規范以CIL為基礎。圖3給出了CIL中表達式的定義。其中,exp定義了表達式的全集,lval
定義了左值表達式,constant定義了常量表達式,lhost定義了左值表達式引用的存儲塊的起
始地址,offset定義了相對偏移,biop和unop分別定義了二元操作和一元操作,Var為變量集
合,typ為變量類型的集合,fieldinfo為結構體的域,偏移包括0偏移NoOffset,域偏移(結構
體)Field和索引偏移Index,CastE 為類型強制轉換符。StartOf(lval)表示數組的起始位置,
等同一個指針,AddrOf對應到C語言中的&操作符,Mem對應C語言中的*操作符,SizeOf,
SizeOfE,AlignOf,AlignOfE分別表示不同類型的變量及表達式的大小和對齊方式,SizeOfStr
表示常量字符串的長度。CIL還引入StartOf來簡化類型轉換規則。
圖3 CIL 中表達式的定義
Fig.3 definition of expressions in CIL
C語言中的表達式都可以寫成CIL的文法形式。例如,左值表達式*((int*)100)可以寫成
(Mem CastE(intType, (integer 100))),其中intType是TInt(IInt,[])的縮寫,integer 100是Const
(CInt64(Int64.of_int 100, IInt, None))的縮寫,x.b可以寫成(x,Field(b,NoOffset))。為了敘述方
便,在不引起混淆時,本文使用原始的C表達式作為CIL文法形式的表達式的簡寫。
定義1:不含域偏移(Filed)和索引偏移(Index)的CIL 表達式稱為規范型表達式。也
就是說,規范型表達式中只包含0 偏移NoOffset。
借助指針運算,很多表達式都可以變換為等價的規范型表達式(這里討論等價時,不考
慮編譯過程由于對齊方式導致的差異,這種差異不影響溢出檢測結論。因此,不要求表達式
在編譯后仍然等價,只需要在源碼中表達式語義相同)。例如,假設x為struct { int a[3]; int b[2];}
類型的變量,則表達式x.a[1]等價于*((int*)((unsigned)&x+sizeOf(int))),表達式x.b[1]等價于
*((int*)((unsigned)&x+4* sizeOf(int)))。但是,結構體中的bit域(“bit field”)相對結構體起始
地址的偏移不是整數個字節,沒有規范型表達式與之等價。bit域是結構體(或聯合體)中
的特殊的成員,它占用的空間以位(而不是字節)為單位。幸運的是,利用C語言中固有的
位操作符可以消除結構體中bit域在程序中的出現。具體方法是:為每一個bit域b關聯一個掩
模字段bm,假設b有n位,是bh的成員,且相對于bh的偏移為o位。對給定的結構體變量bh和成
計算機畢業設計網http://www.pdzuhx.tw
- 7 -
員b,o可以在編譯時計算出來。不失一般性,設sizeOf(unsigned)等于32,且n+o小于32。掩
模bm是一個無符號整數“b31b30…….b0”,其中,當o ≤ i < n+o時,bi=0,其它情況下bi=1。在
需要對b進行讀操作時,使用“(*(unsigned*

www.pdzuhx.tw
)(&bh) & (~bm)) >> o”代替b,在需要將w寫入到
b中時,使用“*(unsigned*)(&bh) = ((*(unsigned*)(&bh ) & bm) | (~bm & (w << o)))”來替換這
次寫操作。其中“~”是按位取非操作,二元操作符“&”是按位與操作,“|”是按位或操作,“<<”
和“>>”分別是按位左移和按位右移操作。圖4給出一個消除bit域的例子。
圖4 消除bit 域的出現
Fig.4 eliminate “bit field”
定理1:任意一個不包含bit 域的CIL 表達式,一定存在一個規范型表達式與之等價。
上述定理可以用結構歸納法加以證明。對應于該結構歸納證明,任意一個不含bit域的
左值表達式,都可以使用一個遞歸算法將其化為等價的規范型表達式。右值表達式中包含的
左值表達式都規范化后就得到該右值表達式對應的規范表達式。限于篇幅,本文僅給出將不
含bit域的左值表達式化為規范型的算法,如圖5所示。其中,函數offsetToInt遞歸地計算表
達式中包含的偏移量,它以一個類型t和一個偏移o作為輸入,返回偏移量的符號表達式。例
如,給定類型struct { int a[3]; char b[2];}和偏移Field(b,Index(1, Nooffset)),它將返回3×
sizeOf(int)+sizeOf(char)。函數normalLval調用offsetToInt將表達式化為規范型。這里的算法
假設表達式已經進行了必要的化簡,將對指針變量的索引操作化為指針運算。例如,設x定
義為int* x,盡管C語言中允許使用x[2]來代替*(x+2),但CBOC預先將x[2]化為*(x+2)的的形
式。
圖5 將表達式化為規范型
Fig.5 transform expression to its normalized form
任意一個表達式,可以消除表達式中的bit域,并使用normalLval將其規范化,表達式最
終都會被化為*e的形式。例如,設a和b分別是類型為 struct {int a[10];int b[5];}和struct {int*
a;int* b;}的結構體變量,并設sizeOf(int)等于32,a.b[2]和b.b[2]將分別被化為*((int
*)((unsigned)(&a) + 48)) 和*(*((int **)((unsigned)(&b) + 4)) + 2)。本文后面的章節將假設程
序中的所有左值表達式都具有*e的形式。
計算機畢業設計網http://www.pdzuhx.tw
- 8 -
4.4.2 基址安全表達式
C語言中的很多表達式,即使能通過編譯檢查,在使用的過程中也可能導致不可意料的
后果。例如,arr[(int)&x],*((int*)100)。這些左值表達式試圖訪問不確定的或受限制的地址
空間。在程序語句中使用這些表達式,如:arr[(int)&x]=10,*((int*)100)=10將會導致運行時
錯誤。本文認為這類表達式是不合法的,不應該在程序中使用。這里我們不考慮靜態規劃好
的數據區,例如,在嵌入式程序設計中,通常劃定一片空間為數據區,可以使用形如
*((int*)100) 的表達式對這些數據區進行訪問,此時,必須由程序員來保證訪問不超出數據
區,程序分析工具無法從源代碼中進行檢查。
事實上,程序中所有可以合法訪問的存儲塊包括三類:一類通過全局變量定義來靜態分
配空間,另一類通過局部變量定義動態地在執行棧里分配空間。還有一類通過malloc,free
等存儲管理函數來動態地在堆空間中分配和釋放(為方便敘述,本文使用malloc來統一表示
所有內存分配函數,使用free來統一表示所有內存釋放函數)。若g是全局變量,可以用&g
來標記分配給g的存儲塊的起始地址,并作為該存儲塊的ID。對函數進行內嵌處理后,分配
給局部變量l的存儲塊的起始地址及ID可以用&l來標記。在進行循環展開和函數內嵌后,動
態分配的存儲塊的個數也可以通過計算代碼中malloc出現的次數得到。為每個動態分配的存
儲塊b引入一個虛擬變量vb,并用&vb表示存儲塊b的起始位置并作為b的ID。那么,所有可
以合法訪問的存儲塊都以&x開始,所有可以訪問的存儲地址都可以用一個形如*(&x+O)的規
范型表達式來表示,其中x為程序中定義的某個變量或虛擬變量,O是一個表達式,表示該
存儲地址相對宿主存儲塊的整數字節偏移。當O為0時,*(&x)就是x。因此,合法的存儲地
址都可以通過形如*(&x+O)的表達式進行訪問。前一節我們已經討論過,每一個C語言左值
表達式都可以化為*e的規范形式。這里,我們引入基址安全(site-safe)表達式的概念來進
一步對表達式加以限制。
定義2:對程序位置L處的左值表達式lv,從程序開始位置對程序進行符號執行,當符號
執行到達程序位置L時,若lv可以化簡成為*(&x+z)的形式,其中,x是程序變量或虛擬變量,
z為整數,則稱lv是基址安全(site-safe)的左值表達式。表達式是基址安全的,當且僅當它
所包含的所有左值表達式都是基址安全的。
上面的定義基于這樣的考慮:若程序可能訪問的所有地址組成的集合與用戶的輸入有
關,則用戶可以采用精心構造的輸入來讓程序訪問非法的地址空間。定義 2 要求左值表達
式訪問的存儲塊有一個合法的起始位置,但沒有對偏移z的大小進行限制,因此,稱這樣的
表達式為基址安全表達式。
需要注意的是:判定表達式是否是基址安全的是在符號執行的過程中進行的,是一種動
態的行為,而不是依據表達式在程序代碼中的形式來靜態地進行判斷,也就是說基址安全是
相對于一條符號化執行路徑而言的。例如,對如下的程序片段:
int *p; L1: p=malloc(100); if(y){ L2: p=p+x-x+2;} else {L3: p=p+x;} L4: *p=10;
其中x,y是輸入變量,程序位置L4處的指針表達式*p相對于執行路徑L1;L2;L4來說是基址安
全的;而相對于執行路徑L1;L3;L4來說,則不是基址安全的。
對于不同變量x1和x2,它們的地址&x1和&x2在編譯時確定,且必然不相等,它們之間
也不存在確定的線性關系。因此,有如下推論:
推論1:基址安全的表達式*(&x1+z1)和*(&x2+z2)相等,當且僅當x1和x2是同一個變量,
且z1=z2。
計算機

www.pdzuhx.tw
畢業設計網http://www.pdzuhx.tw
- 9 -
這一推論說明:任意兩個基址安全的左值表達式是否相等可以方便地從形式上進行判
斷。正是基址安全表達式的這一優點,使得CBOC能夠極大的簡化緩沖區溢出漏洞的檢測過
程,并提高檢測效率。
基址安全表達式要求符號執行過程中左值表達式中的偏移部分是整數,而不是可以包含輸入
符號的普通表達式。這使得該定義對表達式的限制太強,難以處理實際程序中一類典型的情
況:程序員可能會使用用戶輸入作為偏移量來索引程序中的數組,并且采用條件判斷語句對
用戶輸入進行檢查,保證程序不會越界訪問。這類情況需要結合路徑條件進行處理。但是,
基址安全表達式保證了左值表達式的偏移部分是整數,使得左值表達式的等價性判斷非常容
易,這就允許我們采用優化的符號執行過程來進行緩沖區溢出漏洞檢測。本文第五節的實驗
結果也顯示:很多包含緩沖區溢出的實際應用程序,其表達式都是基址安全的,優化的符號
執行算法能高效地發現這些代碼中包含的緩沖區溢出。因此,相對于基址安全表達式給檢測
算法在性能上所帶來的優化和提升,基址安全表達式的負面效果是可以接受的。
4.5 優化的符號執行過程
符號執行的主要思想是使用符號值而不是實際的數據來代表程序輸入,并在執行過程中
產生關于輸入符號的代數表達式。符號執行每一步的狀態包括三個內容:路徑條件 ( Path
Condition, PC)、程序計數器與程序變量的符號值。PC是基于輸入符號的布爾型公式,它積
累程序執行的每一步輸入變量必須滿足的約束。當PC表達的約束可滿足時,說明對應該PC
的路徑是可達的。否則,對應該PC的路徑不可達。程序計數器定義了下一個要執行的語句,
通常用程序位置表示。
CBOC利用符號執行技術檢測C程序中的緩沖區溢出漏洞。使用經典的符號執行算,難
以解決數組元素的混淆,復雜的數據結構,指針與引用的混淆等問題。基址安全表達式可以
方便的進行等價性判斷,這為CBOC的符號執行過程提供了優化的空間。優化主要體現在指
針的解引用上,兩個指針是否指向相同的存儲位置可方便地通過表達式的等價判斷得出。因
此,CBOC可以使用哈希表來維護基址安全的左值表達式(而不是變量)和其符號值的對應
關系。每個基址安全的左值表達式對應一個存儲地址,在哈希表中,每個表達式只會有一個
對應的符號值。假如哈希表中的左值表達式不是基址安全的,很難判斷兩個表達式是否等價
(互為別名),這樣可能導致哈希表中同一存儲地址有多個符號值,且不能同步更新。
4.5.1 賦值語句
圖6給出了CBOC中符號執行賦值語句lv=e的算法,其中lv是左值表達式,e是普通表達
式。函數assign以lv和e作為輸入,將賦值語句執行后的程序狀態更新到state中。state是一個
全局的哈希表,它將基址安全的表達式映射到表達式當前的符號化值。顯然,基址安全表達
式高效的等價性判斷是建立哈希表state的前提。函數symbVal以表達式e為參數,計算e的符
號化值,計算過程中可能會引入虛擬變量(遇到用戶輸入變量時),并將虛擬變量的符號化
值更新到state中。算法假設程序已經經過預處理:所有的表達式都是規范型表達式,變量初
始化已經轉化為等價的賦值語句。算法的主要思想是:從程序入口點開始符號執行,將對左
值表達式的修改更新到state中,在對未賦值的左值表達式lv進行讀操作時,需要引入一個新
的輸入符號,表示lv的符號值并將其對應關系更新到state中。對已經賦值的左值變量進行讀
操作時,從state中獲得變量的當前值。可以看出,該算法僅需要維護被使用過的變量的當前
值,而無需像CBMC一樣,當更新數組中的一個元素時,需要同時更新整個數組的問題。
計算機畢業設計網http://www.pdzuhx.tw
- 10 -
圖6 符號執行賦值語句
Fig.6 Symbolic execute an assignment
4.5.2 存儲空間動態分配
為了檢測緩沖區溢出漏洞,我們使用哈希表aloc維護存儲塊的相關信息,aloc將存儲塊
的ID映射到該存儲塊的長度。根據變量的定義信息對aloc進行初始化。例如,對程序中定義
的每一個全局變量(或每一個局部變量的實例)v,需要在aloc中添加一條記錄,將&v映射
到存儲塊的長度sizeOf(typeOf(v))。動態分配的存儲塊的信息同樣維護在aloc中。圖7給出處
理動態存儲空間分配的算法。函數doMalloc和函數doFree分別對應存儲空間的分配和釋放。
算法的主要思想是:當符號執行到動態存儲分配語句lv=malloc(e)時,引入一個新的虛擬變
量x作為該存儲塊的ID,在aloc中添加一條記錄,將x映射到對應存儲塊的長度e。當符號執
行到存儲空間釋放語句free(e)時,symbVal (e)必須是某個存儲塊的ID,將該ID對應的存儲塊
的長度更新為0即可。
圖7 符號執行動態內存分配語句
Fig.7 Symbolic execution of dynamic allocation
4.5.3 越界訪問檢查
有了aloc,越界訪問的檢查相當簡單。左值表達式*(&x+z)將引用ID為&x的存儲塊中偏
計算機畢業設計網http://www.pdzuhx.tw
- 11 -
移量為z的存儲地址。使用&x在aloc中查詢到存儲塊的長度,記為len,若z>len可滿足(使用
SMT求解器[13]對表達式的可滿足性進行判斷),則說明*(&x+z)引用的存儲地址可能超過了
存儲塊&x的邊界。
4.5.4 字符串操作函數導致的溢出檢查
C庫中的一些函數,如果使用不當,它
們將可能導致緩沖區溢出。這類函數包括
gets,strcpy, strcat, sprintf,memcpy, strncpy
等。這些函數的源代碼往往不公布,基于源
代碼的漏洞檢測工具不能直接處理這類函
數。CBOC采用一種直觀的方式來處理這類
函數:為這些函數提供簡單的源代碼來刻畫
這些函數的操作過程,然后將這些函數當作
用戶定義的普通函數來處理,這樣字符串操
作函數導致的緩沖區溢出問題就被轉化為
越界訪問問題。作為例子,圖8給出了函數
strlen和strcpy的簡單代碼。
圖8 strlen 和 strcpy
Fig.8 strlen and strcpy
5. 實驗結果
與CBMC一樣,CBOC使用一個循環展開參數(-unwind)來控制循環展開的遍數。CBMC
報告兩種類型的錯誤:overflow和non-site-safe。當報告overflow時

www.pdzuhx.tw
,說明在程序中發現了一
個真實的緩沖區溢出漏洞,當報告non-site-safe時,說明在程序中存在某些表達式不是site-safe
的。當程序中的某些循環展開不充分時,CBOC還會發出警告:unwinding assertion violation。
此時,需要增大循環的展開遍數來查找更長的路徑中包含的緩沖區溢出漏洞.。
表1 實驗數據
Table 1 Experiment results
CBOC CBMC
軟件名稱 漏洞編號
循環
展開
遍數
時間
(1/10s)
空間
(MB)
時間
(1/10s)
空間
(MB)
SpamAssassin BID-6679 10 6 5.4 124 132.3
bind CA-1999-14 10 10 5.4 13 11.8
sendmail CVE-1999-0047 5 7 5.4 341 244.5
sendmail CVE-1999-0206 5 5 5.4 22 30.9
wu-ftpd CVE-1999-0368 10 7 3.9 6 4.6
bind CVE-2001-0011 15 5 5.4 12 11
sendmail CVE-2001-0653 15 5 5.4 32 16.3
sendmail CVE-2002-0906 5 5 5.4 7 7.3
sendmail CVE-2002-1337 15 5 5.4 12 12.8
sendmail CVE-2003-0161 5 5 5.4 5 5.6
wu-ftpd CVE-2003-0466 10 11 5.4 9 8.2
sendmail CVE-2003-0681 5 5 5.4 11 11.1
apache CVE-2004-0940 4 162 5.4 12 12.4
計算機畢業設計網http://www.pdzuhx.tw
- 12 -
apache CVE-2006-3747 15 10 5.4 17 18.4
MADWiFi CVE-2006-6332 5 5 5.4 4 3.4
NetBSD-libc CVE-2006-6652 5 5 5.4 >50000 >900
OpenSER CVE-2006-6749 5 7 5.4 35 14.1
OpenSER CVE-2006-6876 10 5 5.4 7 6.4
edbrowse CVE-2006-6909 4 64 5.4 178 166.4
gxine CVE-2007-0406 5 5 5.4 4 3.4
samba CVE-2007-0453 5 5 5.4 11 3.6
libgd CVE-2007-0455 5 5 5.4 >878 >900
使用Kelvin Ku等人[14]提供的測試包對CBOC進行了驗證。該測試包收集了來自apache,
bind,sendmail,NetBSD-libc,gxine等12個著名的開源軟件的298個真實代碼片段,包含了
22個CVE[15]發布的緩沖區溢出漏洞。測試使用的硬件環境為:1.66GHz Intel Core2 處理器,
1G內存。我們使用工具run[16]對工具的運行時間和內存使用情況進行統計,并設置工具運行
的時間上限為50000秒,內存占用上限為900MB。在相同的條件,我們將CBOC和CBMC進
行比較。表1給出詳細的比較結果。可以看到,在大多數測試中,CBOC的性能都優于CBMC。
特別地,CBOC使用內存很少,因為CBOC執行過程中只維護棧頂的一個程序狀態,而像
CBMC這樣的模型檢驗工具通常同時保存訪問過的所有狀態。
在測試過程中,CBOC準確地定位了測試包中除CVE-2002-0906之外的21個緩沖區溢出
漏洞,而漏洞CVE-2002-0906被報告為一個non-site-safe錯誤。可見,實際應用中的很多包含
緩沖區溢出程序,其表達式都是基址安全的,CBOC優化的符號執行算法能高效地發現這些
代碼中包含的緩沖區溢出。因此,相對于基址安全表達式給檢測算法和工具在性能上所帶來
的優化和提升,基址安全表達式所帶來的負面效果是可以接受的。
在測試過程中,CBOC還發現了因測試包作者的疏忽所導致的兩個問題。一個問題出現
在CVE-2006-6652的測試代碼中,文件glob3_int_bad.c,第69行。指針表達式*pathlim試圖訪
問整數數組A中偏移量為44字節的存儲空間。但A中只包含3個元素(12字節)。圖9是從文
件glob3_int_bad.c中抽取的一段代碼。在圖9中第10行,sizeof(A)的值為12,因此,變量bound
的值將為A+11。但pathlim是一個整數指針,它將引用從A開試偏移11個整數(也就是44字
節)的地方。這個漏洞并不是開源軟件中真實存在的,而是由于測試包的作者在編寫測試程
序過程中的疏忽導致的。
另一個問題出現在CVE-2006-6876的測試代碼中,文件loops_bad.c被標記為包含了緩沖
區溢出漏洞。使用CBOC進行檢查時沒有發現漏洞。通過人工檢查,該文件確實不包含緩沖
區溢出漏洞。
圖9 測試包中的一個錯誤
Fig.9 a mistake in the benchmark
計算機畢業設計網http://www.pdzuhx.tw
- 13 -
CBOC通過遍歷程序的所有有限長的路徑來查找程序錯誤。理論上不存在誤報,也能發
現有限長的路徑中包含的所有緩沖區溢出漏洞。然而在具體實現的過程中,可能會存在誤報
和漏報,原因包括:由于C語言的語義極為復雜,為兼顧效率,設計過程中可能會作一些近
似;某些API調用(如pthread_create,fork,setitimer等)導致的多線程和控制流變化;shmget
等API函數導致的內存共享;以及工具原型尚未刻畫的函數,如:fgets,getcwd等。
我們使用Kendra Kratkiewicz[17]提供的一個測試包對CBOC的漏報率和誤報率進行了詳
細考察。該測試包收集了1164個精心編制的代碼片段,覆蓋了多種類型的緩沖區溢出漏洞。
其中,291個片段沒有溢出漏洞,其余的873個代碼片段中包含漏洞。使用CBOC的檢測結果
顯示:工具正確區分出290個沒有漏洞的代碼片段,誤報1個,誤報率約為0.34%,準確定位
了858個溢出漏洞,漏報15個,漏報率約為1.72%。
6. 總結
本文給出一個基于符號執行的C語言緩沖區溢出漏洞檢測工具CBOC。CBOC通過引入
基址安全表達式的概念,對CBOC的符號執行過程進行了優化,從而緩解

www.pdzuhx.tw
了指針、數組等給
程序分析帶來的復雜度,提高了檢測效率。實驗表明:相對于基址安全表達式給檢測工具帶
來的巨大優化空間,基址安全表達式所帶來的負面效果是可以接受的。這說明基址安全表達
式的引入對大概率出現的事件給予了更多優化,符合“大概率事件優先”的原則。在大多數
測試中,CBOC的性能都優于著名的C語言限界模型檢驗工具CBMC,且CBOC使用內存較少,
誤報率和漏報率都很低。CBOC可用于發現緩沖區溢出漏洞,給出錯誤路徑,幫助開發人員
理解和分析漏洞。
CBOC采用符號執行技術,存在如下固有的局限性:
1) 不能克服分支和循環等導致的路徑數目指數級增長的問題,難以對大規模軟件系統
進行檢測;
2) 循環展開次數不易確定。如果程序中包含不終止的循環,參數調整的過程可能不收
斂。
參考文獻
[1] Bodik R, Gupta R, Sarkar V. ABCD: Eliminating array-bounds checks on demand [A]. Programming
Language Design and Implementation (PLDI), Vancouver: ACM, 2000: 321-333.
[2] Condit J, Harren M, McPeak S, et al. CCured in the real world [A]. Programming Language Design and
Implementation (PLDI), San Diego: ACM, 2003: 232-244.
[3] D. Wagner, J. Foster. A first step towards automated detection of buffer overrun vulnerabilities [A].
Network and Distributed System Security Symposium (NDSS), San Diego: CA, 2000: 3-17.
[4] Ganapathy V, Jha S, Chandler D, et al. Buffer overrun detection using linear programming and static analysis
[A]. Computer and Communications Security (CCS), Washingtion: ACM, 2003: 345-354.
[5] Dor N, Rodeh M, Sagiv S. CSSV: towards a realistic tool for statically detecting all buffer overflows in C [A].
Programming Language Design and Implementation (PLDI), San Diego: ACM, 2003: 155-167
[6] Chaki S, Hissam S. Precise Buffer Overflow Detection via Model Checking [R]. SEI, CMU, 2005.
[7] Chaki S, Hissam S. Certifying the Absence of Buffer Overflows [R]. CMU/SEI-2006-TN-030, SEI, CMU,
2006.
[8] Clarke E, Kroening D, Lerda F. A Tool for Checking ANSI-C Programs [A]. Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), Barcelona: Paris: Springer, 2004: 168-176.
[9] Thomas Ball, Sriram K. Rajamani. The SLAM Toolkit [A]. Computer Aided Verification (CAV), LNCS,
2001:260–264.
[10]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, et al. Lazy Abstraction [A]. SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL), Portland: ACM, 2002:58–70.
[11]James C. King. Symbolic Execution and Program Testing [J].Commun. ACM 19(7): 385-394, 1976
[12]Necula G, McPeak S, Rahul S, et al. CIL: Intermediate Language and Tools for Analysis and Transformation
of C Programs [A]. Compilier Construction (CC), Grenoble: Springer, 2002: 213-228.
計算機畢業設計網http://www.pdzuhx.tw
- 14 -
[13]Moura M, Dutertre B, Shankar N. A Tutorial on Satisfiability Modulo Theories [A]. Computer Aided
Verification (CAV), Trento: Springer, 1999 2007: 20-36
[14]Ku K, Hart T, Chechik M, et al. A buffer overflow benchmark for software model checkers [A]. Automated
Software Engineering (ASE), Atlanta: IEEE/ACM, 2007: 389-392
[15]http://cve.mitre.org/. National Cyber Security Division of the U.S. Department of Homeland Security, 2009.
[16]J. K. U. Armin Biere, ETH Zurich. http://fmv.jku.at/run/, 2008.
[17]Kratkiewicz K. Evaluating Static Analysis Tools for Detecting Buffer Overflows in

www.pdzuhx.tw
C Code [D]. USA:Harvard
University 2005.
CBOC : An efficient tool to detect buffer overflows in C
source code
Chen Shi-Kun1, L i Zhou-Jun2
1(School of Computer Science, National University of Defense Technology, Changsha 410073)
2(Computer Science and Engineering School, Beihang University, Beijing 100191)
Abstract
Buffer overflows are the source of a vast majority of security issues in C program. This paper
presents a tool called CBOC (C Buffer Overflow Checker) to detect buffer overflows in C source code.
It bases on symbolic execution and introduces the notion of site-safe expression to optimize the
process of symbolic execution. CBOC takes as input source code, and can identify buffer overflows in
the source code automatically. CBOC was applied to a publicly-available benchmark and compared
against state-of-the-art ANSI-C bounded model checker CBMC. Experiments show that CBOC
exceeds CBMC in most of the test cases and the memory usage of CBOC is very low. In the accuracy
test experiments, the false alarm rate of CBOC is about 0.34% and omission rate is about 2.08%.
Keywords: buffer overflow; symbolic execution; site-safe expression
作者簡介:
陳石坤(1980-),男,博士研究生,主要研究領域為信息安全,軟件驗證;
李舟軍(1963-),男,博士,教授,主要研究領域為高可信軟件技術,網絡與信息安全技術,智能信
息處理技術
計算機畢業設計網http://www.pdzuhx.twwww.pdzuhx.tw
精准三肖中特