鮑鐵勻, 高鳳娟, 周 嚴, 李 游, 王林章, 李宣東

?

基于目標制導符號執(zhí)行的靜態(tài)緩沖區(qū)溢出警報自動確認技術

鮑鐵勻1,2,3, 高鳳娟1,2,3, 周 嚴1,2,3, 李 游1,2,3, 王林章1,2,3, 李宣東1,2,3

1計算機軟件新技術國家重點實驗室(南京大學) 南京 中國 2100232江蘇省軟件新技術與產業(yè)化協(xié)同創(chuàng)新中心 南京 中國 2100233南京大學計算機科學與技術系 南京 中國210023

緩沖區(qū)溢出漏洞是一類嚴重的安全性缺陷。目前存在動態(tài)測試和靜態(tài)分析技術來檢測緩沖區(qū)溢出缺陷: 動態(tài)測試技術的有效性取決于測試用例的設計, 而且往往會引入執(zhí)行開銷; 靜態(tài)分析技術及自動化工具已經被廣泛運用于緩沖區(qū)溢出缺陷檢測中, 然而靜態(tài)分析由于采取了保守的策略, 其結果往往包含數(shù)量巨大的誤報, 需要通過進一步人工確認來甄別誤報, 但人工確認靜態(tài)分析的結果耗時且容易出錯, 嚴重限制了靜態(tài)分析技術的實用性。符號執(zhí)行技術使用符號代替實際輸入, 能系統(tǒng)地探索程序的狀態(tài)空間并生成高覆蓋度的測試用例。本文提出一種基于目標制導符號執(zhí)行的靜態(tài)緩沖區(qū)溢出警報確認方法, 使用靜態(tài)分析工具的輸出結果作為目標, 制導符號執(zhí)行確認警報。我們的方法分為3步: 首先在過程間控制流圖中檢測靜態(tài)分析警報路徑片段的可達性, 并將可達的警報路徑片段集合映射為用于確認的完整確認路徑集合; 其次在符號執(zhí)行中通過修剪與溢出缺陷疑似語句無關的路徑, 指導符號執(zhí)行沿特定確認路徑執(zhí)行; 最后在溢出缺陷疑似語句收集路徑約束并加入溢出條件, 通過約束求解的結果, 對靜態(tài)分析的警報進行分類?；谏鲜龇椒ㄎ覀儗崿F(xiàn)了原型工具BOVTool, 實驗結果表明在實際開源程序上BOVTool能夠代替人工減少檢查59.9%的緩沖區(qū)溢出誤報。

符號執(zhí)行; 緩沖區(qū)溢出; 警報確認; 目標制導

1 引言

軟件安全漏洞一般是由于程序員的疏忽或者編程語言的局限性等原因遺留在代碼中的特殊的缺陷。這些漏洞一旦被攻擊者利用會造成非常嚴重的后果, 能夠極大削弱軟件安全性。緩沖區(qū)溢出漏洞已經成為當前威脅極大的軟件漏洞之一, 據(jù)CVE (Common Vulnerabilities and Exposures)公共漏洞數(shù)據(jù)庫統(tǒng)計2011年和2013年發(fā)現(xiàn)的軟件漏洞中緩沖區(qū)溢出漏洞占到了19%和17%左右[1]。緩沖區(qū)溢出漏洞在代碼層面上屬于內存操作類缺陷。造成緩沖區(qū)溢出缺陷的原因是程序的緩沖區(qū)中可以寫入超出其長度的數(shù)據(jù), 沒有進行越界檢查而造成溢出, 從而有可能破壞程序的堆棧, 造成程序崩潰或使程序執(zhí)行攻擊者的指令, 存在很高的安全隱患。

目前普遍主要采用兩種方式來檢測程序中的緩沖區(qū)溢出缺陷: 靜態(tài)分析[2-15]和動態(tài)測試[16-22]。動態(tài)測試指的是通過設計測試用例使得程序執(zhí)行特定的路徑以測試是否存在缺陷。動態(tài)測試因為其特性, 檢測的精準性高, 但其弊端在于依賴測試用例以及需要執(zhí)行開銷。靜態(tài)分析是指不運行軟件的前提下對軟件代碼進行分析的過程[23]。緩沖區(qū)溢出缺陷問題往往發(fā)生在特定的控制流路徑上, 所以靜態(tài)分析工具一般來說是路徑敏感的。靜態(tài)分析往往事先設定緩沖區(qū)溢出特征, 掃描待測試程序的源碼或者字節(jié)碼進行特征匹配, 所以靜態(tài)分析并不需要動態(tài)執(zhí)行測試程序, 因此不會引入運行時的開銷。由于上述特性, 靜態(tài)分析工具在學術界和在工業(yè)界更受歡迎。目前比較常見的靜態(tài)分析工具包括HP Fortify[24], Splint[25], Klockwork[26]以及Coverity[27]等等。

然而, 靜態(tài)分析工具在程序規(guī)模與結果精準性之間很難取得平衡, 以Fortify靜態(tài)分析工具為例, 掃描CVE公共漏洞數(shù)據(jù)庫中存在緩沖區(qū)溢出缺陷的程序, 如表1所示, 分析結果中包含了大量的警報需要人工確認, 警報數(shù)量也隨著程序規(guī)模上升而急劇增加。除此以外, 靜態(tài)分析工具常常產生大量的誤報, 其中可能包含真正的緩沖區(qū)溢出缺陷, 人工確認這些警報非常耗費時間與精力。確認靜態(tài)警報通常需要人工閱讀相關代碼片段并依據(jù)審閱者自身經驗判斷, 整個過程依賴于審核者的專業(yè)能力, 不易自動化, 隨著警報個數(shù)的增加, 人工確認流程成本增高, 并且極有可能引入誤判。

表1 實際程序使用Fortify掃描結果

符號執(zhí)行技術是一種傳統(tǒng)的軟件測試和分析技術, 最早提出于1976年[28], 該技術使用符號代替具體輸入, 能夠系統(tǒng)地探索程序的狀態(tài)空間并生成高覆蓋度的測試用例。從原理上看, 符號執(zhí)行收集所有可行的路徑條件并生成測試用例。然而符號執(zhí)行技術還存在一些不足: 比如與環(huán)境(操作系統(tǒng), 網絡, 數(shù)據(jù)庫等)交互, 路徑爆炸(可行路徑的數(shù)量隨著路徑長度的增長而呈指數(shù)增長的趨勢[29]), 以及浮點數(shù)運算等問題。目前存在多種測試工具是基于符號執(zhí)行的思想實現(xiàn)的, DART[30]結合隨機測試和模型檢查技術, 檢測每條路徑上的不同的錯誤類型, 然而其對于指針以及循環(huán)等結構無法有效處理。KLEE[31]能夠模擬環(huán)境來解決環(huán)境交互的問題, 然而其無法模擬整個環(huán)境執(zhí)行。S2E[32]采用選擇符號執(zhí)行的技術, 能夠自動減少需要符號執(zhí)行的代碼數(shù)量, 在確保穩(wěn)定的情況下執(zhí)行流程透明地在符號領域和實際領域往返。

本文提出一種靜態(tài)分析制導符號執(zhí)行的緩沖區(qū)溢出警報自動確認技術。我們基于靜態(tài)測試工具警報, 首先在控制流圖上進行可達性分析, 可達的前提下獲取達到特定目標的路徑集合; 然后指導符號執(zhí)行沿特定路徑執(zhí)行; 最后當符號執(zhí)行到達溢出疑似位置, 分析是否觸發(fā)緩存區(qū)溢出缺陷, 并產生相應的測試用例。我們的確認技術能夠將缺陷疑似路徑分成不可執(zhí)行路徑、安全路徑、可溢出路徑以及未知路徑, 并在路徑分類的基礎上將靜態(tài)分析警報分為溢出、誤報以及無法確認三類。

本文的貢獻主要在于:

(1) 提出面向緩沖區(qū)溢出缺陷的靜態(tài)分析警報驅動的自動動態(tài)確認技術;

(2) 提出可達性分析用于篩選靜態(tài)警報確認路徑, 提出符號執(zhí)行目標制導機制用于縮減符號執(zhí)行狀態(tài)空間以及基于符號執(zhí)行的緩沖區(qū)溢出檢測機制用于警報確認;

(3) 基于上述方法實現(xiàn)緩沖區(qū)警報確認工具BOVTool, 在正確性驗證程序和大規(guī)模實際程序兩組基準程序上進行實例研究, 實驗數(shù)據(jù)表明BOVTool能夠利用目標制導機制有效引導確認路徑執(zhí)行, 并大量減少緩沖區(qū)溢出警報的人工確認數(shù)量。

本文的組織結構如下: 第2節(jié)詳細描述我們的方法目標制導符號執(zhí)行的自動確認技術; 第3節(jié)介紹原型工具的實現(xiàn)并進行實驗和評估; 第4節(jié)分析靜態(tài)分析, 動態(tài)測試, 靜態(tài)結果驗證等相關工作, 第5節(jié)總結全文并討論未來的工作。

2 目標制導符號執(zhí)行的自動確認技術

2.1 方法架構

本文提出的基于目標制導符號執(zhí)行的緩沖區(qū)溢出確認方法如圖1所示, 首先使用靜態(tài)分析工具對待測試程序源代碼進行分析, 獲取程序中可能存在緩沖區(qū)溢出缺陷的語句類型, 位置以及潛在可能觸發(fā)缺陷的語句組合作為靜態(tài)分析警報。符號執(zhí)行的確認過程分為3個步驟: 可達性分析、目標制導以及警報確認。首先抽象程序, 建立程序控制流圖分析程序入口與靜態(tài)警報的目標缺陷語句之間的可達性, 如果可達抽取路徑信息構建制導信息表; 其次將制導信息表, 靜態(tài)警報的目標缺陷語句以及程序源代碼作為輸入提供符號執(zhí)行引擎, 指導符號執(zhí)行過程沿設定的確認路徑執(zhí)行; 最后監(jiān)測執(zhí)行流程, 判斷符號執(zhí)行是否到達缺陷疑似點, 通過語句類型提取溢出條件約束, 連同路徑約束進行約束求解, 分析求解結果, 最終得到靜態(tài)警報的分類結果。

下面將用一個示例程序來說明我們的想法:

1 . # define MAX_LEN 242. # define MIN_LEN 43. void usage ( ) {4. char des_buffer[MIN_LEN];5. char* src_buffer="source buffer";6. strcpy(des_buffer, src_buffer);7. }8. void initialize( char* argv_string){9. char mapped_argv[MIN_LEN];10. if( strlen(argv_string) == 0)11. return;12. if( strlen(argv_string) >= MAX_LEN)13. return;14. if(argv_string[0] != '-')15. strcat(mapped_argv,'-');16. strcpy(mapped_argv, argv_string);17. }18. int main (int argc, char **argv) {19. initialize (*argv);20.}

如圖2所示的代碼片段用靜態(tài)分析工具Fortify掃描后, 發(fā)現(xiàn)的緩沖區(qū)溢出靜態(tài)警報有3處, 分別是1:{4,6}; 2:{9,15}; 3: {18,19,9,16}, 這里大括號前面的內容表示警報編號, 大括號內的內容表示組成警報路徑片段的程序源碼語句行號。靜態(tài)警報路徑片段的起始點往往是緩沖區(qū)分配語句, 也有可能是函數(shù)調用語句, 終止點一般是緩沖區(qū)操作語句。由于程序中的大部分警報出現(xiàn)在initialize函數(shù)中, 我們?yōu)閕nitialize函數(shù)構造其函數(shù)內控制流圖以便更加清楚分析和展示我們的方法。如圖3所示, initialize函數(shù)(簡稱i)中存在4條路徑, 所有的分支以及分支約束都以標簽的形式加以區(qū)別:

①strlen(argv_string)≠0;

②strlen(argv_string) == 0;

③strlen(argv_string) < MAX_LEN;

④strlen(argv_string)>= MAX_LEN;

⑤argv_string[0] == '-'

⑥argv_string[0] ≠ '-';

如果我們構造全局過程間控制流圖, 第1條警報路徑片段, 第4行和第6行不會映射到控制流圖中, 因為他們所在的函數(shù)沒有被調用即無法執(zhí)行, 這里我們將其判斷為不可達路徑, 無需進行后續(xù)驗證。

對于第2條警報路徑片段{9,15}, 第9和15行分別映射到基本塊i.entry和 i.block4, 在控制流圖中能夠覆蓋警報路徑片段的基本塊路徑為

i.entry-> i.block1-> i.block2-> i.block4, 在確認該路徑的過程中, 我們將第15行溢出疑似語句的溢出條件加入到路徑約束中進行求解, 即strlen(argv_ string) ≠ 0 ^ strlen(argv_string) < MAX_LEN

^argv_string[0] ≠ '-' ^ strlen('-') +

strlen (argv_string)>size(mapped_argv), 我們無法找到滿足這樣的約束條件的mapped_argv, 所以我們認為第2條靜態(tài)分析警報安全路徑, 而且由于第15行所在的語句只有一條路徑能夠到達, 所以我們認為第15行語句是誤報。在實際程序中對于某個靜態(tài)警報可能會包含多個可達路徑, 只有每一條路徑都被確認為安全路徑, 我們的工具才會判定該缺陷語句為誤報點。對于第3條警報路徑片段第9和16行分別映射到基本塊i.entry和i.block5, 在控制流圖中存在兩條可達路徑i.entry-> i.block1-> i.block2-> i.block3-> i.block5以及i.entry-> i.block1-> i.block2-> i.block4-> i.block3-> i.block5, 出于確認正確性考慮, 兩條路徑都需要被驗證, 這里我們選擇前者為例, 路徑約束和溢出條件為strlen(argv_string) ≠ 0^ strlen (argv_string) < MAX_LEN^ argv_string[0] == '-'^

strlen(argv_string)>size(mapped_argv), 我們可以找到滿足該約束的argv_string以及mapped_argv。事實上argv_string來自于main函數(shù)參數(shù), 沒有越界檢查確實有可能超過緩沖區(qū)mapped_argv的最大長度, 所以我們認為第3條警報路徑片段是可溢出路徑。靜態(tài)分析的結果中只要有某條可達路徑為可溢出路徑, 我們的工具就會判定該缺陷語句為溢出點。在確認過程中, 我們的目標制導機制則用于解決如何避免執(zhí)行示例中的1條無用路徑, 而選擇需要確認的3條路徑執(zhí)行。

2.2 可達性分析

控制流圖構建 我們首先利用編譯器為待測試程序生成中間指令集合, 并根據(jù)指令之間的跳轉關系劃分基本塊, 生成函數(shù)內的控制流圖; 其次我們從函數(shù)內控制流圖出發(fā), 依據(jù)函數(shù)調用指令分析調用關系構造過程間的完整控制流圖; 最后我們逆轉基本塊的指向關系構造雙向控制流圖, 進行此步驟的目的出于對大規(guī)模程序的分析效率的考慮, 因為我們后續(xù)的路徑尋找基于深度優(yōu)先搜索, 從缺陷語句所在的基本塊開始反向搜索能夠有效減少遍歷節(jié)點的數(shù)目。

算法1: 從函數(shù)內控制流圖集合生成過程間控制流圖

輸入: 函數(shù)內控制流圖集合以及函數(shù)的入口基本塊

輸出: 過程間完整雙向的控制流圖

ConstructRCFG(BasicBlock B)1: CFGNode current = initialize(B)2: FOR each Instruction in B 3: IF current instruction is function call (f is callee)THEN4: current->addSucc(f->entryBlock()) 5: f->entryBlock()->addPrev(current)6: IFf->entryBlock()has not been visitedTHEN7: ConstructRCFG (f->entryBlock()) 8: END IF9: current = f->returnBlock()10: END IF11: END FOR12: FOR each succ in B->succSet DO13: current->addSucc(succ) 14: succ->addPrev(current)15: IF succ has not been visited THEN16: ConstructRCFG (succ) 17: END IF18: END FOR

該算法描述了從函數(shù)內控制流圖構建完整雙向過程間控制流圖的過程, 在實現(xiàn)過程中, 我們能夠利用編譯器獲取函數(shù)內的控制流圖, 圖中的每個節(jié)點為稱為,只存在后繼關系, 為了能夠構建過程間的雙向控制流圖, 我們將其封裝為, 能夠表示節(jié)點之間的前驅和后繼關系,為我們下文中所說的基本塊。我們用指向當前遍歷的控制流圖節(jié)點(第1行),函數(shù)將封裝為。在遍歷當前節(jié)點的所有后繼節(jié)點之前, 我們首先遍歷基本塊中的每條指令檢測是否存在函數(shù)調用指令(第2-11行), 如果存在的話(假設f為被調用函數(shù)), 將的后繼指向被調用函數(shù)的入口基本塊(第4行), 隨后如果該函數(shù)還沒有訪問過, 遞歸訪問被調用函數(shù), 當被調用函數(shù)返回的時候, 將指向被調用函數(shù)的返回基本塊(第9行), 這樣被調用函數(shù)的返回基本塊的后繼指向調用指令所在基本塊的后繼, 算法的12-18行描述將的后繼指向基本塊的后繼, 并對于每一個后繼遞歸調用, 此時指向的可能是基本塊, 也可能是基本塊中調用函數(shù)的返回基本塊。這里我們在構建過程間完整控制流圖的同時就已經添加反向指針(第5行, 第14行), 而非構建完成后再次遍歷添加。

基本塊映射 我們首先給出緩沖區(qū)溢出缺陷的靜態(tài)分析警報w的概念, 其中使用標簽集合L標記和識別程序中的語句集合,w由三元組構成(l,< l,l,…,l> , l), 其中l,l,…,l?,l為緩沖區(qū)定義語句的標簽,l為緩沖區(qū)操作語句的標簽, 通常為缺陷疑似語句,< l,l,…,l>為一系列靜態(tài)分析與緩沖區(qū)相關的中間語句標簽,< l,l,…,l>可以為空, 它們與標簽l以及l代表的語句共同構成緩沖區(qū)溢出警報路徑片段。我們的方法能夠處理的靜態(tài)分析輸出結果格式為可擴展標記語言(XML), 是大部分靜態(tài)分析工具都能夠支持的。

我們將緩沖區(qū)溢出警報路徑片段中語句標簽映射到雙向控制流圖的基本塊中。我們以三元組(l,< l,l,…,l> , l)標記靜態(tài)分析警報, 對于其中的語句標簽我們以二元組唯一標記, 其中和分別為程序的文件名和行號。源代碼中每個語句標簽的二元組信息與每個基本塊中的指令集合的靜態(tài)信息進行匹配即可映射。我們記錄被映射到的基本塊, 由于這些基本塊之間不一定可達, 下一部分我們進行可達性分析。

可達性分析 我們已經將靜態(tài)警報片段中的語句位置映射到雙向控制流圖的基本塊中, 我們需要確認映射到的基本塊之間的可達性以及程序入口至基本塊之間的可達性, 基本的搜索策略采用深度優(yōu)先搜索, 我們在映射到的基本塊兩兩之間, 以及程序入口基本塊與l所在基本塊之間調用進行可達確認。具體的算法如算法2所示:

算法2: 生成起始基本塊和終止基本塊之間所有基本塊路徑集合

輸入: 控制流圖中的起始節(jié)點和目標節(jié)點,為深度優(yōu)先遍歷中的當前路徑,為用于保存的路徑的集合

輸出:和之間所有基本塊路徑集合

SearchPaths(CFGNode v, CFGNode des, SethPath TempSet , Path temp)1: IF visited(v)==TRUETHEN2: return3: END IF4: temp.push(v)5: IFv == desTHEN6: TempSet.add(temp)7: return8: ELSE9: visited(v) = TRUE10: FOR each succseeor siof vDO11: IFvisited(v)=FALSETHEN12: SearchPaths(si,des,TempSet,temp)13: temp.pop14: END IF15: visited(v)= FALSE16: END FOR

算法2描述了如何在過程間控制流圖中確認靜態(tài)路徑映射到的基本塊之間的可達性, 事實上我們通過搜索基本塊之間所有可達路徑, 如果可達路徑集合為空則說明不可達, 否則我們收集所有路徑并進行后續(xù)步驟。我們通過深度優(yōu)先搜索的策略遍歷每個基本塊節(jié)點。如果當前節(jié)點已經被訪問過, 那么直接返回(第1-2行), 否則把當前節(jié)點加入到當前路徑中(第4行)。如果當前節(jié)點為目標節(jié)點, 那么我們找到一條可達路徑, 將其加入路徑集合, 否則不為目標節(jié)點, 我們將其設為已經被訪問過, 對于當前節(jié)點的每一個后繼遞歸調用進行訪問。在一個節(jié)點的后繼都被訪問完成之后, 我們將其設為沒有被訪問過, 目的是為了搜索所有可達路徑。對于循環(huán)模塊表現(xiàn)為控制流圖中的環(huán), 我們的處理策略是在靜態(tài)分析時決定是否進入循環(huán), 而循環(huán)的次數(shù)將依賴于符號執(zhí)行支撐工具的處理。

路徑選擇與拼接 上個步驟中我們通過得到各個基本塊之間, 程序入口至路徑起始基本塊的所有路徑片段。這些路徑片段由控制流圖的基本塊所組成, 我們需要從多個路徑片段中選擇確認的路徑, 我們認為這些路徑片段對于確認效果來說是等價的, 可以根據(jù)實際情況設定不同的選擇策略?？紤]在確認過程中盡可能減少誤報情況的出現(xiàn), 我們的方法則是保留了所有可能的路徑組合。拼接上述路徑集合即可得到從待測試程序入口到缺陷疑似語句的完整可達路徑。

制導信息表構建 制導信息表由潛在溢出缺陷路徑r集合組成,r可以理解為從程序入口至緩沖區(qū)溢出點所在的基本塊之間的可達路徑所抽取出的分支入口信息。由于某個警報的缺陷語句可能存在多條可達路徑, 那么w和r存在一對多的對應關系。制導信息表作為符號執(zhí)行的額外輸入,r才是我們在真正確認驗證的路徑。最后警報分類的結果是基于r的分類結果, 這將在2.4章節(jié)說明。

2.3 目標制導

符號執(zhí)行是一種傳統(tǒng)的用于軟件測試和分析的技術[28], 其目的是盡可能的遍歷程序的狀態(tài)空間, 并產生高覆蓋度的測試用例。符號執(zhí)行的基本思想是用符號代替實際輸入, 在執(zhí)行過程中遇到分支則復制已有的環(huán)境信息, 并收集相關路徑約束。當執(zhí)行到程序出口或發(fā)現(xiàn)錯誤時, 根據(jù)收集到的約束條件求解, 產生相應的測試用例。符號執(zhí)行的整個執(zhí)行過程實際上就是選擇下一個執(zhí)行狀態(tài)并對該狀態(tài)中所包含的指令進行解釋的過程, 符號執(zhí)行中的某條路徑可以認為是由多個有序執(zhí)行狀態(tài)以及約束組成的集合。傳統(tǒng)的搜索策略描述符號執(zhí)行過程中如何選擇下一個執(zhí)行狀態(tài), 關注于如何提高程序覆蓋度, 我們的目的則是探索并執(zhí)行靜態(tài)分析中的緩沖區(qū)潛在溢出缺陷路徑。隨著程序規(guī)模的增大, 符號執(zhí)行存在狀態(tài)爆炸的問題。為了使得符號執(zhí)行能夠避免路徑爆炸, 也使得其能夠確認特定的缺陷疑似路徑, 我們設計了一種輕量型的機制能夠實現(xiàn)目標制導, 這種機制的基本思想在于無用路徑剪枝, 實現(xiàn)該機制的關鍵則在于如何確定無用路徑以及如何盡早修剪無用路徑。前者依據(jù)靜態(tài)警報的結果, 與潛在溢出缺陷路徑不相匹配的即為無用路徑, 而符號執(zhí)行中路徑是由多個符號執(zhí)行狀態(tài)組成的, 即轉換為不相匹配的狀態(tài)檢測。如果僅僅只有靜態(tài)警報片段, 符號執(zhí)行只有在某條路徑執(zhí)行完成之后才能判斷是否覆蓋了警報片段, 我們將潛在溢出缺陷路徑作為額外輸入提供給符號執(zhí)行引擎, 在分支指令處分裂新的狀態(tài)時抽取r的信息比較, 刪除不相匹配的狀態(tài)。

算法3描述了目標制導的符號執(zhí)行技術路徑剪枝算法, 在符號執(zhí)行的過程中需要維護一個狀態(tài)池用于保存當前所有執(zhí)行的狀態(tài), 整個符號執(zhí)行過程的終止條件為狀態(tài)池中已經沒有狀態(tài)可以選擇或者到達了設定的時間閾值(第2行), 每次執(zhí)行的過程分為3個步驟(第4-6行): 首先從狀態(tài)池中選擇下一個狀態(tài), 然后解釋狀態(tài)內部指令, 在解釋指令的過程中會有狀態(tài)增加或者刪除操作,和分別用于臨時保存即將變更的狀態(tài), 最后操作更新狀態(tài)池。對于某條指令的解釋過程體現(xiàn)在算法的第7-16行, 首先判定該指令的類型是否為退出或者錯誤觸發(fā)類型, 是則將其加入并根據(jù)路徑約束條件求解得到測試用例(第8-11行), 否則繼續(xù)判斷其類型是否為分支指令, 復制當前狀態(tài), 添加相反約束, 將新的狀態(tài)加入, 調用模塊進行路徑剪枝(第12-16行)。具體的路徑剪枝過程在算法17-27行, 我們將兩個相反分支的入口信息與制導信息表中的信息對比, 刪除不符合潛在溢出缺陷路徑的分支(第21-25行)。

算法3: 符號執(zhí)行的目標制導算法

Vector addedStates //符號執(zhí)行過程中增加狀態(tài)集合Vector removedStates //符號執(zhí)行過程中刪除狀態(tài)集合Vector ESVector //保存所有符號執(zhí)行狀態(tài)的集合executionState initialState; //符號執(zhí)行的初始化狀態(tài)Vector ValidatingPath; 1. ESVector.add(initialState);2. WHILE ESVector.size>0 || !TIME OUTDO3. executionState ES = selectState()4. ES.executeInstruction()5. updateStates(ESVector, addedStates, removedStates)6. END WHILE7. executeInstruction()8. IFES.instructionType = EXIT || FoundErrorTHEN9. generateTestCase();10. removedStates.add(ES);11. END IF12. IF ES.instructionType = FORKTHEN13. ES2=fork(ES);14. addedStates.add(ES2);15. GuidedExecution(ES, ES2);16. END IF17. GuidedExecution (executionState ES, executionState ES2)18. IFES! =NULL && ES2 ! =NULLTHEN19. =BranshesDebugInfo(ES); 20. =BranshesDebugInfo(ES2);21. IF ValidatingPath.contain() && ! ValidatingPath.contain()THEN22. removedStates.add(ES2);23. END IF24. IF! ValidatingPath.contain () && ValidatingPath.contain()then25. removedStates.add(ES);26. END IF27. END IF

為了確保剪枝過程的正確性, 即不存在誤刪的情況, 當相反分支的入口信息都出現(xiàn)或者都不出現(xiàn)在制導信息表中時, 我們都不做處理。原因有以下兩點: (1)我們的目標制導技術目前無法處理庫函數(shù)調用, 因為這部分信息在控制流圖上是缺失的, 庫函數(shù)中的路徑我們無法選擇如何刪減; (2)某種缺陷的觸發(fā)依賴于循環(huán)的迭代次數(shù), 而我們的溢出確認路徑不含包含循環(huán)信息。如果靜態(tài)分析警報的溢出疑似位置出現(xiàn)在某個循環(huán)內部, 那么符號執(zhí)行在達到缺陷語句后繼續(xù)執(zhí)行直到下一次循環(huán), 之后的制導信息存在缺失的情況。

由于路徑剪枝機制的局限性, 我們目前只能夠實現(xiàn)目標的近似制導, 而非精確制導, 實際情況可能是一組路徑片段中包含了與靜態(tài)結果相匹配的某條路徑。但是從實驗結果來看, 我們實現(xiàn)的機制與傳統(tǒng)的符號執(zhí)行相比已經能夠大大提高時間和空間效率, 至于如何實現(xiàn)更加精確的制導以及控制符號執(zhí)行過程中循環(huán)的執(zhí)行次數(shù), 我們考慮將其作為后續(xù)工作。

2.4 緩沖區(qū)溢出警報確認

2.4.1 緩沖區(qū)溢出模型

為了擴展符號執(zhí)行緩沖區(qū)溢出確認的功能, 我們首先定義了緩沖區(qū)溢出模型。緩沖區(qū)溢出主要分為相關API的調用以及緩沖區(qū)直接訪問兩類。

緩沖區(qū)相關的API調用 為了使得我們的緩沖區(qū)溢出模型涉及的操作更具實用性和普遍性, 我們參照了C99標準中可能存在緩沖區(qū)溢出缺陷的操作和Linux中常見系統(tǒng)調用, 并根據(jù)參數(shù)的格式分成8個類型, 在表2顯示了不同類別的緩沖區(qū)操作的溢出條件。我們構造緩沖區(qū)溢出條件的基本思路是寫入的字符串長度是否大于緩沖區(qū)本身的長度, 但是在實際實現(xiàn)的過程中, 我們很難獲取符號化字符串的長度信息, 我們使用表示字符串的字節(jié)長度,滿足", 0≤＜,P[] ≠'