周寬久，楊 廣，賴曉晨，崔 凱，姚艷雙

（大連理工大學(xué) 軟件學(xué)院，遼寧 大連116620）

0 引 言

軟件代碼中的缺陷是導(dǎo)致軟件故障和漏洞問題的主要原因［1］，國家自然科學(xué)基金委也設(shè)立可信軟件重大研究計劃專門解決軟件可信性問題，通常的軟件缺陷如緩沖區(qū)溢出、格式字符串、內(nèi)存泄漏等無法通過安全子集檢測出來，而又是影響軟件可信性的主要原因，因此文章重點解決上述這些缺陷，從而達到提高軟件可信性的目的。

對于軟件代碼漏洞缺陷檢測的研究，國內(nèi)外成果很多，Koushik Sen最早提出了concolic（一種白盒測試方法）單元測試的概念［2］，通過符號執(zhí)行來計算程序的執(zhí)行路徑，研究如何賦初值的問題。Gulwani S提出一種基于有限回溯符號執(zhí)行（symbolic execution）的缺陷自動驗證方法，結(jié)合路徑條件和缺陷觸發(fā)條件進行缺陷自動驗證［3］。Froihofer L等人則通過源碼插樁方式得到程序動態(tài)運行的輸出信息和日志，可以有效分離系統(tǒng)的業(yè)務(wù)邏輯與檢測邏輯，增加程序動態(tài)分析的可靠性［4］。針對代碼檢測誤報率過高的問題，肖慶，官云戰(zhàn)等人提出了使用多項式時間復(fù)雜度的路徑敏感算法實現(xiàn)對代碼缺陷的靜態(tài)檢測，該方法通過控制流圖實現(xiàn)屬性狀態(tài)條件的合并，判斷不可達性，降低誤報率［1］。近年來模型驗證也成為代碼診斷領(lǐng)域研究的熱點，卞磊，劉超等人使用有窮狀態(tài)機模型對過程內(nèi)變量數(shù)據(jù)流異常進行檢測，根據(jù)數(shù)據(jù)項的狀態(tài)遷移判斷過程內(nèi)的數(shù)據(jù)流是否異常［5］。周寬久等人提出了一種基于XML中間模型的代碼安全規(guī)范檢測方法，使用GJB安全子集對代碼安全進行分析［6］。陳忠湘，詹瑾瑜等人提出一種帶控制流的函數(shù)分析模型，對函數(shù)間調(diào)用次序以及邏輯設(shè)計復(fù)雜度都有描述，輔助程序設(shè)計人員進行分析［7］。

針對C/C＋＋的代碼檢測技術(shù)很多，多為通過抽象語法樹AST來獲取檢測信息，因此實現(xiàn)復(fù)雜、擴展性差。文章在XML中間模型［6］的基礎(chǔ)上，提出控制流提取模型，獲取檢測信息，簡化控制流圖的獲取，降低路徑分析復(fù)雜度；將安全子集檢測與數(shù)據(jù)流異常檢測相結(jié)合，并將數(shù)據(jù)流分析擴展到過程間、模塊間，從而提高代碼缺陷的檢測能力。

1 控制流提取模型

控制流提取模型將調(diào)用關(guān)系用ID節(jié)點表示，將ID屬性attributes中的IDTYPE記錄為 “CALL”，LINENUMBER記錄為進行函數(shù)調(diào)用的行號，NAME同級增加FUNLINE，表示被調(diào)用函數(shù)的定義行號。屬性ASSIGNMENT表示為變量的相關(guān)賦值語句行號，形如line1：m1，line2：m2…line n：mn，m1…mn代表所賦具體值?？刂屏魈崛∧Ｐ凸?jié)點表示如圖1所示。

圖1 控制流提取模型節(jié)點表示

部分標(biāo)識定義為：

（1）訪問標(biāo)號ACCESS：記錄類、結(jié)構(gòu)體和聯(lián)合體成員的訪問標(biāo)號。

（2）所屬結(jié)構(gòu)OWNER：成員的所在類、結(jié)構(gòu)體、聯(lián)合體或命名空間的名稱。

（3）虛函數(shù)標(biāo)記VIRTUAL：指示類成員函數(shù)是否是虛函數(shù)。

（4）運算符重載OPERATE：記錄重載操作符。

（5）基類PARENT：記錄派生類的繼承基類。

（6）模板TEMPLATE：模板定義和聲明的模板參數(shù)信息。

2 控制流抽取與分析

獲取控制流圖是進行控制流分析的基礎(chǔ)，更是進行數(shù)據(jù)流跟蹤的前提，只有獲取控制流，確定程序執(zhí)行路徑，才能跟蹤變量數(shù)據(jù)流。

2.1 控制流提取模型到控制流轉(zhuǎn)化

利用提取模型對過程間、模塊間數(shù)據(jù)流進行記錄，用ID節(jié)點中的LINENUMBER作為跳轉(zhuǎn)索引，實現(xiàn)控制流圖的構(gòu)建。過程間代碼到控制流提取模型的轉(zhuǎn)化，及提取模型到控制流圖的轉(zhuǎn)化都是通過對跳轉(zhuǎn)索引進行跟蹤實現(xiàn)的。

下文示例代碼包含了一些常見的控制流結(jié)構(gòu)和過程間調(diào)用，在描述過程間控制流與數(shù)據(jù)流關(guān)系方面，具有一定代表性。

篇幅所致，僅列出與示例代碼相應(yīng)的控制流節(jié)點ID，將與控制流無關(guān)的ID刪除，使用XQuery技術(shù)對中間代碼進行分析，獲得過程內(nèi)、過程間以及模塊間的控制流信息。

實際程序中轉(zhuǎn)移分支語句數(shù)目多、結(jié)構(gòu)復(fù)雜，對一些不可達路徑進行刪減顯得尤為重要。因此提出控制流切片及剪枝方法刪減代碼控制流圖數(shù)組信息。

2.1.1 控制流切片

程序切片是一種分析和理解程序的技術(shù)，通過從源程序中去除零條或多條語句來構(gòu)造，最早由Weiser于1979年提出，通過計算每個興趣點的切片來進行程序的分析與理解［8］。文章提出的控制流切片與程序切片的定義接近，為源程序控制流零條或多條分支組成的代碼單元，同時也是一個控制流分析單元。

定義1 代碼控制流圖定義為六元組G＝＜E，P，Estart，Eend，Eentry，Eexit＞ ，其中，E代表節(jié)點集，由LINENUMBER［6］標(biāo)識，P為路徑集合，由控制流圖數(shù)組記錄；Estart與Eend為控制流切片起、終點集合，Eentry與Eexit為轉(zhuǎn)移路徑起、終點集合。

定義2 控制流切片定義為由主函數(shù)路徑（i＝0）起始，并交于主函數(shù)的控制流圖子圖，表示為控制流切片起、終點為estart，eend，控制流切片內(nèi)分支結(jié)構(gòu)的起、終點為einstart，einend。

定義3 控制流切片的函數(shù)調(diào)用為轉(zhuǎn)移路徑，起、終點為eentry，eexit。（Pf表示產(chǎn)生的新增路徑集合。主函數(shù)路徑中轉(zhuǎn)移路徑情況例外，表示為定義2中控制流切片

定義4 并接符號Λ表示將兩個路徑集合并接，P1ΛP2：｛＜p1，p2＞｜p1∈P1，p2∈P2｝，即路徑集合P1中的每條路徑均可能成為P2中所有路徑的前段路徑，路徑｛p1，p2｝構(gòu)成完整路徑。實現(xiàn)為將兩個數(shù)組并接，在并接過程的同時，若超過存儲范圍，則停止檢測。

情況3 如果控制流切片中分支結(jié)束，即轉(zhuǎn)移到einend，則圖2中（Pexit＝（Pstart，因為函數(shù)調(diào)用與內(nèi)嵌分支間沒有其他結(jié)構(gòu)，因此路徑集合不變。其中（Pin為嵌套分支路徑集合，（Pstart為進入分支嵌套結(jié)構(gòu)前的路徑集合。

根據(jù)程序控制流切片的定義及性質(zhì)，針對主程序的分支情況進行處理，對可能路徑進行合并，考慮到嵌套的有限性，對控制流切片內(nèi)部條件分支以及轉(zhuǎn)移進行同樣處理，以控制流切片為單位獲取代碼的可能執(zhí)行路徑，偽代碼描述如下：

可能執(zhí)行路徑獲取算法偽代碼：

圖2 控制流切片

使用上文闡述的可能路徑獲取算法，獲得示例代碼的可能執(zhí)行路徑，包括 ｛17，20，26｝，｛17，20，22，1，7，10，13，7，22，23，26｝， ｛17，20，22，1，7，10，13，14，7，22，23，26｝， ｛17，20，22，1，7，10，13，7，22，23，24，26｝， ｛17，20，22，1，7，10，13，14，7，22，23，24，26｝等。圖3描述示例代碼的控制流圖，基于提取模型，通過可能路徑獲取算法獲得代碼的可能執(zhí)行路徑信息，并保存在控制流圖數(shù)組中，利用數(shù)組信息對模型中CODELINE的屬性節(jié)點LINENUMBER進行追蹤，并記錄所跟蹤變量的狀態(tài)變化。

圖3 過程間代碼控制流程

可能路徑獲取算法并未描述break與switch語句的處理方式，switch語句處理需要解析表達式，獲取正確路徑，處理方法與下文控制流剪枝處理方法相似；break語句處理方式與分支語句結(jié)束標(biāo)簽處理方式相同。

2.1.2 控制流剪枝

上文中，控制流圖數(shù)組信息包含的路徑數(shù)目巨大，因此根據(jù)分支條件，合理對控制流進行剪枝具有重大意義。剪枝可用于包括if、while、for等的分支結(jié)構(gòu)中，主要分兩種情況：第一種情況，在條件語句中即可判斷真?zhèn)危鏵or（int i＝0；i＜＝10；i＋＋）。第二種情況，需要解析表達式，追蹤未知變量，如for（i＝p＊j；i＜＝10；i＋＋）中需追蹤p和j的賦值來判斷條件語句的真?zhèn)巍Ｌ幚矸绞饺缦拢?/p>

情況1 可直接從提取模型中獲取變量值，＜ASSIGNMENT＞23：0＜/ASSIGNMENT＞表示在第23行，局部變量賦值為0。由于0＜＝10，因此必定進入for模塊中，對該分支節(jié)點剪去一枝。

情況2 根據(jù)for節(jié)點ID行號LINENUMBER［6］標(biāo)識23（假設(shè)23行定義for）以及i的ID節(jié)點中＜ASSIGNMENT＞23：p＊j＜/ASSIGNMENT＞，發(fā)現(xiàn)相應(yīng)賦值為p＊j，經(jīng)過表達式解析分別查找p的ID節(jié)點以及j的ID節(jié)點，并在其ID節(jié)點的ASSIGNMENT內(nèi)尋找小于并最接近23的行號，發(fā)現(xiàn)p＝2，j＝k＋1，同理尋找k的ID節(jié)點，發(fā)現(xiàn)小于并最接近j＝k＋1行號的賦值記錄為k＝5；通過層層遞歸即可實現(xiàn)條件剪枝，圖4通過遞歸及簡單表達式解析求得12大于10，因此不執(zhí)行for循環(huán)，對該分支節(jié)點剪去一枝。情況2剪枝原理如圖4所示。

圖4 控制流剪枝情況2

將剪枝方法應(yīng)用到控制流抽取中，可以解決常見控制流抽取方法中路徑眾多的問題，在控制流切片起始點estart進行控制流剪枝，解決了控制流圖數(shù)組元素過多的問題。

剪枝算法偽代碼描述：

算法中FUNCTION2函數(shù)為變量追蹤函數(shù)，追蹤變量的最近賦值記錄。使用剪枝算法對上文示例代碼的可能執(zhí)行路徑進行剪枝，main函數(shù)中for（int i＝2；i＜＝3；i＋＋）的條件表達式i＜＝3為真，函數(shù)f2中for（int i＝1；i＜＝q；i＋＋）的條件表達式i＜＝q無法判斷，因為引入函數(shù)參數(shù)變量，main函數(shù)的if分支的條件無法判斷。剪枝算法處理后的可能執(zhí)行路徑為 ｛17，20，22，1，7，10，13，7，22，23，26｝， ｛17，20，22，1，7，10，13，14，7，22，23，26｝， ｛17，20，22，1，7，10，13，7，22，23，24，26｝， ｛17，20，22，1，7，10，13，14，7，22，23，24，26｝等。

2.2 安全規(guī)則子集

控制流異常與數(shù)據(jù)流異常是軟件運行異常的兩個主要原因，控制流異常主要是由控制結(jié)構(gòu)的使用不當(dāng)帶來的，GJB安全子集中包含了大量描述代碼控制流安全的規(guī)則，文獻［6］中指出在 《GJB 5369－2005航天型號軟件C語言安全子集》中代碼控制流相關(guān)規(guī)則（程序風(fēng)格類，宏指令類以及過程類）所占比例已超過61%，還有一部分描述變量定義與數(shù)據(jù)操作的安全規(guī)則，因此文章使用GJB安全子集對代碼控制流進行安全性檢測。安全子集中對代碼安全隱患描述詳盡，但無法檢測出變量的狀態(tài)變化，更無法對變量數(shù)據(jù)流進行跟蹤，挖掘數(shù)據(jù)流錯誤，安全子集中關(guān)于數(shù)據(jù)變量的安全缺陷描述僅限于數(shù)據(jù)變量的定義和操作，因此將變量數(shù)據(jù)流跟蹤與GJB安全子集檢測相結(jié)合，從安全缺陷檢測及數(shù)據(jù)流異常檢測兩個角度挖掘代碼的安全隱患，增強代碼缺陷的挖掘能力。

此外，采用的控制流提取模型還增添了對 《MIRA C＋＋：2008》的支持，將代碼安全缺陷檢測擴展到過程間、模塊間。

3 數(shù)據(jù)流異常分析

通過控制流提取模型獲取控制流圖，從而得到代碼的可能執(zhí)行路徑，實現(xiàn)對數(shù)據(jù)變量的跟蹤，檢測數(shù)據(jù)流異常。

3.1 數(shù)據(jù)流異常檢測狀態(tài)機

數(shù)據(jù)流異常可分為過程內(nèi)、過程間以及模塊間數(shù)據(jù)流異常。與控制流異常相比，數(shù)據(jù)流異常更為常見，由數(shù)據(jù)流異常導(dǎo)致的錯誤要占到錯誤總數(shù)的15%以上［5］。文獻［9］指出使用數(shù)據(jù)流分析方法可以精確地分析程序，檢測程序信息流安全，并且寬容性更大。文獻 ［5］使用有窮自動機對過程內(nèi)的一般變量進行數(shù)據(jù)流檢測，在一定程度上提高了過程內(nèi)數(shù)據(jù)流異常審查效率。文章提出控制流提取模型，基于該模型獲取代碼可能執(zhí)行路徑，并使用有窮狀態(tài)機對變量數(shù)據(jù)流進行跟蹤。

指針變量具有特殊性，可定義為空指針，同時與有效指針狀態(tài)所能進行的轉(zhuǎn)化不同，不能進行正常的引用及刪除。當(dāng)引用指向空地址單元的指針時，會產(chǎn)生嚴(yán)重的空指針引用故障［10］。同時，數(shù)組訪問越界、懸空指針訪問等安全隱患通常也是黑客利用的手段［11］。文章在文獻 ［5］狀態(tài)機的基礎(chǔ)上，將指針單獨劃出，將變量類型C分為指針型變量P以及一般型變量G，解決空指針狀態(tài)跟蹤問題。

定義5 文章引用Mealy狀態(tài)機的形式定義［5］M＝（Q，Σ，Δ，δ，λ，qs），其中，Mealy機的狀態(tài)集合Q＝｛＜q，c＞｜q∈S，c∈C｝，S＝｛qs，qn，qd，qr，qk，E｝，C＝｛P，G｝。其中，qs為被跟蹤變量的首次出現(xiàn)，qn表示將指針變量賦值為空，qd為定義或賦值后的狀態(tài)，qr為引用或解引用后的狀態(tài)，qk表示釋放變量空間后的狀態(tài)，E為數(shù)據(jù)流異常狀態(tài)。輸入字母表Σ＝｛d，r，k，n｝，d代表變量定義，r變量引用，k清除變量，n設(shè)置空指針。狀態(tài)轉(zhuǎn)移函數(shù)δ：（Q，Σ）→Q。輸出函數(shù)λ：（Q，Σ）→Δ，輸出字母表Δ＝｛E，R｝，R表示在某一檢測點非E的任何狀態(tài)，即暫時正確狀態(tài)。錯誤狀態(tài)集ES＝｛＜q，c＞｜q∈S－｛R｝，c∈C｝，錯誤狀態(tài)為穩(wěn)定狀態(tài)，即產(chǎn)生錯誤后不能進入其他狀態(tài)。

定義6 基于上文定義5中的Mealy狀態(tài)機，定義數(shù)據(jù)流異常，定義檢測主體集合M＝｛a1，a2，…，an｝，a∈Q，a為檢測主體，檢測變量。客體集合N＝｛n1，n2，…，nn｝，n∈Σ。因此變量的生存序列（狀態(tài)輸出布爾值序列）為L＝｛λ｛a，n1｝，λ｛a，n2｝，…λ｛a，nn｝｝。將數(shù)據(jù)流異常定義為L∩｛E｝≠Φ。即在變量的生存序列中出現(xiàn)不合法行為，正是對數(shù)據(jù)流檢測的重點。

3.2 數(shù)據(jù)流異常檢測狀態(tài)機

狀態(tài)遷移表示變量當(dāng)前狀態(tài)與類型的笛卡爾乘積到下一狀態(tài)的轉(zhuǎn)化，依據(jù)文獻［5］中對狀態(tài)變遷的描述，將變量分為一般變量及指針變量，具體如下：

根據(jù)變量的狀態(tài)集合及變遷條件可得Mealy機的狀態(tài)遷移圖如圖5和圖6所示。

4 構(gòu)建系統(tǒng)框架原型

系統(tǒng)通過對源代碼文件進行詞法、語法分析獲得控制流提取模型，基于該模型，設(shè)立兩個主線程，分別用來對代碼進行安全子集檢測和數(shù)據(jù)流異常檢測，并將檢測結(jié)果以異常報表的形式輸出，系統(tǒng)設(shè)計原型如圖7所示。

圖7 系統(tǒng)結(jié)構(gòu)框架模型

5 相關(guān)實驗

為驗證所提方法，修改文獻 ［6］中靜態(tài)檢測工具，自行設(shè)計面向?qū)ο笳Z言的檢測系統(tǒng)CPP－CSV。引入控制流切片模型，同時結(jié)合數(shù)據(jù)流異常檢測算法對linux－0.11內(nèi)核kernel目錄下的3個常用文件signal.c，panic.c，printk.c進行檢測，其中，signal.c主要負責(zé)對信號進行判斷，在系統(tǒng)調(diào)用等方面作用巨大。panic.c中包含一些處理系統(tǒng)運行故障的函數(shù)，如Panic（）等。printk.c包含一些內(nèi)核態(tài)輸出函數(shù)，廣泛用于嵌入式開發(fā)中。

表1 實驗結(jié)果數(shù)據(jù)

實驗結(jié)果分析：通過實驗得出如下分析結(jié)果，對3個Linux內(nèi)核文件進行檢測，共檢測出缺陷總數(shù)為38類161處，其中控制流相關(guān)缺陷為23類66處，數(shù)據(jù)定義類相關(guān)缺陷為12類84處，變量數(shù)據(jù)流異常為3類11處。

從圖8中的統(tǒng)計結(jié)果可以看出，程序中控制流缺陷種類較多，情況復(fù)雜，并不集中的表現(xiàn)為幾類缺陷。數(shù)據(jù)定義類缺陷具有類型集中，出現(xiàn)頻率高的特點，例如，在signal.c文件中僅6類數(shù)據(jù)定義類缺陷就出現(xiàn)了高達54次，給程序帶來了嚴(yán)重的安全隱患。圖8中可看出，數(shù)據(jù)流異常缺陷出現(xiàn)頻率和種類均比前兩類缺陷低，但部分數(shù)據(jù)流異常檢測在不進行跟蹤的前提下難以實現(xiàn)，如空指針引用等。這3個文件的數(shù)據(jù)流異常多表現(xiàn)為變量定義后未使用，并直接結(jié)束（kill）。此外，未定義便引用的情況，雖然少見但危險性極高、難以檢測。

控制流相關(guān)缺陷及數(shù)據(jù)定義類相關(guān)缺陷均為違反安全子集的情況，為不可忽略的安全隱患。變量數(shù)據(jù)流異常為Mealy機檢測出來的安全隱患，如signal.c文件中有7處對變量定義，但未使用就退出了，導(dǎo)致資源的浪費，使得程序晦澀難懂。由于系統(tǒng)仍處于開發(fā)階段，部分算法需要完善，難免帶來一些檢測的誤報漏報，通過人工分析對系統(tǒng)的誤報漏報進行修正，共發(fā)現(xiàn)系統(tǒng)漏報誤報總數(shù)為3類5處。如表1所示，3個文件的檢測準(zhǔn)確率分別為97.4%、90.0%、97.3%；實驗結(jié)果分析見表2。

圖8 實驗結(jié)果

表2 實驗結(jié)果分析

實驗結(jié)果的分析表明提出的方法具有可行性，保留了原有安全子集的檢測能力，同時提供變量的跟蹤能力。所提方法可有效解決變量跟蹤問題，檢測代碼中隱含的安全缺陷，在提高代碼安全性、可靠性等方面有著重要作用。

6 結(jié)束語

文章提出一種控制流提取模型，基于該模型可以方便構(gòu)造程序控制流圖，獲取程序可能執(zhí)行路徑，解決了常見的基于抽象語法樹獲取控制流圖難度大、擴展性差的缺點；在該模型的基礎(chǔ)上獲取控制流切片，同時增添對面向?qū)ο笳Z言及過程間調(diào)用的支持，在利用安全子集對代碼進行控制流規(guī)范檢測的同時，使對代碼數(shù)據(jù)流跟蹤成為可能，從而彌補了安全子集不能分析變量數(shù)據(jù)流的缺陷，解決了過程間、模塊間數(shù)據(jù)流異常難以分析的問題；此外，還提出了一種控制流化簡方法，采用控制流切片與剪枝手段減少控制流信息數(shù)組中元素數(shù)量，并使用Mealy機的方式對數(shù)據(jù)流進行分類跟蹤，解決了空指針跟蹤問題，提高異常檢測能力。利用該方法對實際Linux內(nèi)核文件進行檢測，取得了良好的效果，檢測準(zhǔn)確率達94.9%。

［1］XIAO Qing，GONG Yunzhan，YANG Zhaohong，et al.Path sensitive static defect detecting method ［J］.Journal of Software，2010，21（2）：210－217.［肖慶，官云戰(zhàn)，楊朝紅，等.一種路徑敏感的靜態(tài)缺陷檢測方法 ［J］.軟件學(xué)報，2010，21（2）：210－217.］

［2］SEN K，Agha G.CUTE：A concolic unit testing engine for C［C］.Proceedings of the 13th ACM SIGSOFT Symposium on Foundations of Software Engineering Held Jointly With 10th European Software Engineering Conference.Lisbon：ACM Press，2005：263－272.

［3］Gulwani S，Srivastava S，Venkatesan R.Program analysis constraint solving ［C］.Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation.Tucson，Arizona，2008：281－292.

［4］Froihofer L，Glos G，Osrael J，et al.Overview and evaluation of constraint validation approaches in Java ［C］.Minneapolis，MN，USA：Proceedings of the 29th International Conference on Software Engineering，2007：313－322.

［5］BIAN Lei，LIU Chao，JIN Maozhong.A method for intra—procedural data flow anomaly auto－detection facing to inspection［J］.Journal of Nanjing University（Natural Sciences），2010，46（1）：71－76.［卞磊，劉超，金茂忠.一種面向?qū)彶榈倪^程內(nèi)數(shù)據(jù)流異常自動檢測方法 ［J］.南京大學(xué)學(xué)報，2010，46（1）：71－76.］

［6］ZHOU Kuanjiu，ZHENG Hongbo，LAI Xiaochen，et al.Research on static analysis method for software security based on XML ［J］.Computer Engineering and Applications，2010，46（28）：64－69.［周寬久，鄭紅波，賴曉晨，等.基于XML的軟件安全靜態(tài)檢測方法研究 ［J］.計算機工程與應(yīng)用，2009，46（28）：64－69.］

［7］CHEN Zhongxiang，ZHAN Jinyu，HAO Zongbo.Method for static function call analysis with control flow ［J］.Computer Engineering，2011，37（9）：47－50. ［陳忠湘，詹瑾瑜，郝宗波.帶控制流的靜態(tài)函數(shù)調(diào)用分析方法 ［J］.計算機工程，2011，37（9）：47－50.］

［8］ZHAO Yunshan，GONG Yunzhan，LIU Li，et al.Improving the efficiency and accuracy of path－sensitive defect detecting ［J］.Chinese Journal of Computers，2011，34（6）：1110－1111. ［趙云山，官云戰(zhàn)，劉莉，等.提高路徑敏感缺陷檢測方法的效率及精度研究 ［J］.計算機學(xué)報，2011，34（6）：1100－1111.］

［9］HUANG Haijun，CHEN Yiyun.Data flow analysis for checking information flow security of programs ［J］.Journal of Chinese Computer Systems，2007，28（1）：102－106.［黃海軍，陳意云.用數(shù)據(jù)流分析方法檢查程序信息流安全 ［J］.小型微型計算機系統(tǒng)，2007，28（1）：102－106.］

［10］ZHANG Wei，LU Qingling，WAN Lin，et al.Research on faults model and testing method of null pointer dereference ［J］.Computer Engineering and Applications，2006，42（4）：71－73.［張威，盧慶齡，萬琳，等.空指針引用故障模型與測試方法研究 ［J］.計算機工程與應(yīng)用，2006，42（4）：71－73.］

［11］CHEN Yiyun，HUA Baojian，GE Lin，et al.A pointer logic for safety verification of pointer programs ［J］.Chinese Journal of Computers，2008，31（3）：372－380. ［陳意云，華保健，葛琳，等.一種用于指針程序安全性證明的指針邏輯［J］.計算機學(xué)報，2008，31（3）：372－380.］