基于形式化規(guī)約的缺陷規(guī)則庫(kù)構(gòu)建與檢測(cè)方法

佟超，王建新，齊建東

北京林業(yè)大學(xué)信息學(xué)院，北京100083

1 引言

程序缺陷分析是軟件質(zhì)量保證的重要組成部分，它能夠在程序交付測(cè)試之前檢測(cè)出影響系統(tǒng)及其運(yùn)行環(huán)境的一般缺陷、惡意代碼及后門(mén)程序，能發(fā)現(xiàn)編譯器不能捕獲的錯(cuò)誤，很大程度上降低了程序的出錯(cuò)率。但隨著軟件系統(tǒng)日趨復(fù)雜，一般缺陷分析方法已不能滿(mǎn)足用戶(hù)日益增長(zhǎng)的需求，其中有兩方面的需求尤為突出。首先，一般缺陷分析方法都將缺陷規(guī)則內(nèi)置在缺陷分析工具之中，用戶(hù)只能選擇工具已有的缺陷，不能自行定義缺陷規(guī)則；其次，傳統(tǒng)缺陷分析方法一般只指出了缺陷發(fā)生的最終位置[1]，無(wú)法確定實(shí)際缺陷與模式缺陷之間的詳細(xì)對(duì)應(yīng)情況，開(kāi)發(fā)人員仍需手動(dòng)調(diào)試以確定導(dǎo)致缺陷的路徑，不能很好地幫助其對(duì)錯(cuò)誤進(jìn)行快速排查和修正。

本文結(jié)合形式化規(guī)約及模型檢測(cè)中的反例輸出技術(shù)提出了一種缺陷規(guī)則庫(kù)構(gòu)建與源碼檢測(cè)方法。利用形式化規(guī)約中的模型規(guī)約對(duì)程序進(jìn)行建模，用性質(zhì)規(guī)約抽象化待檢測(cè)缺陷，即從一般控制流結(jié)構(gòu)中提取出適用于缺陷分析的通用原子命題，結(jié)合分支時(shí)序邏輯CTL的量詞集合，構(gòu)建缺陷規(guī)則庫(kù)元數(shù)據(jù)。用戶(hù)可按照分支時(shí)序邏輯CTL的語(yǔ)法規(guī)則選取原子命題構(gòu)建積木式靜態(tài)缺陷集。規(guī)則庫(kù)引擎從缺陷集中拆分出元數(shù)據(jù)以設(shè)計(jì)表示靜態(tài)缺陷的CTL判定公式，形成相關(guān)原子命題，從源程序中抽取控制流信息并激活相關(guān)原子命題的標(biāo)記模塊，并將控制流信息轉(zhuǎn)換為模型檢測(cè)可接受的K ripke結(jié)構(gòu)。最后，結(jié)合NuSMV模型驗(yàn)證器對(duì)轉(zhuǎn)換所得的有限狀態(tài)系統(tǒng)進(jìn)行檢測(cè)，若存在某種缺陷，則返回帶有源程序行信息的反例路徑。

2 缺陷規(guī)則庫(kù)整體框架

作為一種形式化的自動(dòng)驗(yàn)證方法，模型檢測(cè)將“一個(gè)有限狀態(tài)系統(tǒng)是否滿(mǎn)足某種規(guī)范”抽象為“一個(gè)結(jié)構(gòu)是否滿(mǎn)足某個(gè)命題邏輯公式”，若不滿(mǎn)足則返回導(dǎo)致該錯(cuò)誤的反例[2]。其一般過(guò)程分為三步：對(duì)系統(tǒng)進(jìn)行建模；對(duì)規(guī)約進(jìn)行時(shí)態(tài)邏輯描述；利用模型檢測(cè)工具結(jié)合以上兩步實(shí)現(xiàn)驗(yàn)證。模型檢測(cè)需要對(duì)有限狀態(tài)系統(tǒng)進(jìn)行狀態(tài)檢索，經(jīng)過(guò)對(duì)各類(lèi)程序分析方法的研究[3]，本文采用程序控制流分析手段，展開(kāi)基于形式化規(guī)約的缺陷規(guī)則庫(kù)構(gòu)建。

圖1給出了規(guī)則庫(kù)模型的整體框架，從功能角度可將其流程概括為三個(gè)步驟，每個(gè)步驟涉及到框架中模塊間的通信和交互：

步驟1 用戶(hù)通過(guò)元數(shù)據(jù)自定義所需分析的缺陷規(guī)則，加入規(guī)則庫(kù)。

步驟2 導(dǎo)入待檢測(cè)程序，由規(guī)則庫(kù)引擎抽取其控制流結(jié)構(gòu)，同時(shí)從規(guī)則集中取得待分析缺陷，經(jīng)過(guò)命題動(dòng)態(tài)匹配和模型轉(zhuǎn)換兩個(gè)模塊實(shí)現(xiàn)程序建模以及規(guī)則集中缺陷的實(shí)例化，得到模型驗(yàn)證器可接受的有限狀態(tài)系統(tǒng)。

步驟3 通過(guò)NuSMV模型驗(yàn)證器對(duì)有限狀態(tài)系統(tǒng)進(jìn)行檢驗(yàn)，通過(guò)檢測(cè)結(jié)果轉(zhuǎn)換與輸出模塊返回檢測(cè)結(jié)果及導(dǎo)致缺陷的反例路徑。

圖1 整體框架圖

步驟1與步驟2是本文的重點(diǎn)。其中，用戶(hù)通過(guò)自定義缺陷規(guī)則形成缺陷規(guī)則集，該功能的實(shí)現(xiàn)采用了積木式設(shè)計(jì)模式，并設(shè)計(jì)了相應(yīng)的匹配機(jī)制和邏輯描述形式，使缺陷的抽象化更為靈活。規(guī)則庫(kù)引擎負(fù)責(zé)元數(shù)據(jù)匹配機(jī)制的動(dòng)態(tài)喚醒和程序與實(shí)際缺陷的關(guān)系建模，同時(shí)完成了模型結(jié)構(gòu)的轉(zhuǎn)換。

3 積木式缺陷規(guī)則庫(kù)模型

缺陷規(guī)則庫(kù)模型的構(gòu)建基礎(chǔ)是對(duì)單一缺陷規(guī)則的抽象化描述。本文采用時(shí)態(tài)邏輯描述系統(tǒng)所要滿(mǎn)足的規(guī)范，在此基礎(chǔ)上對(duì)缺陷的行為邏輯進(jìn)行分析，取得構(gòu)成規(guī)則集的通用原子命題集和邏輯量詞集，為規(guī)則庫(kù)的積木式構(gòu)建準(zhǔn)備元數(shù)據(jù)。

3.1 缺陷的行為抽象

時(shí)態(tài)邏輯是一種包含有時(shí)間概念的邏輯，是在命題邏輯的基礎(chǔ)上加入了時(shí)態(tài)算子而形成的邏輯，其基本組成元素為：原子命題、邏輯連接詞、時(shí)態(tài)連接詞[4]。CTL即分支時(shí)序邏輯，是一種典型的時(shí)態(tài)邏輯，缺陷規(guī)則庫(kù)的構(gòu)建需要用戶(hù)理解缺陷抽象為CTL公式的過(guò)程以實(shí)現(xiàn)缺陷自定義，通過(guò)分析M itre通用缺陷列表[5]（Common Weakness Enumeration，CWE），不難發(fā)現(xiàn)程序缺陷產(chǎn)生的原因與人為因素、編程語(yǔ)言以及缺陷本身都具備一定關(guān)聯(lián)，即缺陷的產(chǎn)生與缺陷本身具備一定的規(guī)律性，對(duì)靜態(tài)缺陷而言，該特點(diǎn)在缺陷的語(yǔ)法及語(yǔ)義特征上尤為明顯。根據(jù)該特征與CTL分支時(shí)序邏輯的相似性，同時(shí)考慮到缺陷間不可提取的非共性因素，本文定義了靜態(tài)缺陷的一般缺陷模式，使針對(duì)缺陷的CTL抽象過(guò)程更為清晰，同時(shí)為構(gòu)造規(guī)則庫(kù)的元數(shù)據(jù)集提供研究基礎(chǔ)。

3.1.1 靜態(tài)缺陷的一般缺陷模式

通過(guò)對(duì)靜態(tài)缺陷語(yǔ)法及語(yǔ)義特征的分析，本文將靜態(tài)缺陷的一般缺陷模式定義如下：

定義1 基于語(yǔ)法及語(yǔ)義的靜態(tài)缺陷模式是一個(gè)三元組，M=(S，T，C)，其中S表示一個(gè)或多個(gè)狀態(tài)，T表示由狀態(tài)和狀態(tài)存在性構(gòu)成的事件，C表示事件發(fā)生的范圍。

定義2 狀態(tài)存在性包括：不存在、存在、狀態(tài)組合邏輯（例如狀態(tài)間的與或關(guān)系）下的存在性。

定義3 缺陷有關(guān)事件發(fā)生的范圍可劃分為：全局范圍，在某事件之前，在某事件之后，在事件A與事件B之間，直到發(fā)生某事件。

以Java語(yǔ)言中的空指針異常為例，其缺陷的語(yǔ)義描述為“對(duì)一個(gè)不存在的對(duì)象調(diào)用其屬性或方法而導(dǎo)致的異常”，從該描述中可以提取出缺陷模式的基本表示S={s1，s2}，s1表示對(duì)象值為null，s2表示調(diào)用對(duì)象的屬性或方法；T={t1，t2}，t1表示“存在”s1，t2表示“存在”s2；C表示事件t1出現(xiàn)在事件t2之前。

3.1.2 缺陷模式與CTL

作為一種非線(xiàn)性的時(shí)態(tài)邏輯，CTL在命題邏輯的基礎(chǔ)上加入了時(shí)態(tài)算子，同時(shí)解決了線(xiàn)性時(shí)序邏輯中對(duì)所有路徑做全程量詞的限制。CTL的組成元素包括：原子命題、邏輯連接詞、時(shí)態(tài)連接詞及路徑量詞，其巴克斯范式如下：

其中，F(xiàn)指某個(gè)未來(lái)狀態(tài)，X表示下一個(gè)狀態(tài)，G指所有未來(lái)狀態(tài)，U指直到，A指所有路徑，E指存在一條路徑；?則指某個(gè)原子命題，它是CTL的基本單位[6]。舉例說(shuō)明CTL的用法：以started表示開(kāi)始狀態(tài)，ready表示就緒狀態(tài)。則語(yǔ)句“存在一個(gè)某未來(lái)狀態(tài)，使得開(kāi)始狀態(tài)成立且就緒狀態(tài)不成立”的CTL描述為：

從CTL的基本描述可以分析得出其與缺陷模式M的對(duì)應(yīng)關(guān)系：S映射為原子命題?，T映射為S與邏輯連接詞的組合關(guān)系，C映射為T(mén)與時(shí)態(tài)連接詞和路徑量詞的組合關(guān)系。根據(jù)這一對(duì)應(yīng)關(guān)系結(jié)合CTL的邏輯規(guī)則，即可實(shí)現(xiàn)缺陷模式的CTL抽象[7]。以靜態(tài)缺陷分析中的文件輸入流關(guān)閉異常和空指針異常為例，本文通過(guò)以下兩步來(lái)抽象化缺陷。

步驟1 根據(jù)缺陷含義分析缺陷模式，獲取相關(guān)原子命題。兩種缺陷的具體含義為：

（1）文件輸入流關(guān)閉異常，指在開(kāi)啟了輸入流后，沒(méi)有對(duì)其進(jìn)行關(guān)閉而導(dǎo)致的異常。

（2）空指針異常，指對(duì)一個(gè)不存在的對(duì)象（其指針為null）調(diào)用其屬性或方法而導(dǎo)致的異常。

與以上兩種缺陷相關(guān)的原子命題，如表1所示。

表1 缺陷及相關(guān)原子命題表示

步驟2 根據(jù)缺陷模式，確定所要采用的邏輯連接詞、時(shí)態(tài)連接詞以及路徑量詞，得到最終的CTL公式表示形式如下所示。

文件輸入流關(guān)閉異常：

AG(malloc_fin_s→AF free_fin_s)

該公式的含義：對(duì)于任意路徑下的所有狀態(tài)，若某一狀態(tài)開(kāi)啟了文件輸入流s，則任意路徑的所有未來(lái)狀態(tài)會(huì)存在針對(duì)s的文件流關(guān)閉操作。

空指針異常：

AG(assign_null_s→!(EFinvoked_s))

該公式的含義：對(duì)于任意路徑下的所有狀態(tài)，若某一狀態(tài)將對(duì)象s賦值為null，則不存在未來(lái)狀態(tài)中會(huì)調(diào)用s的屬性或方法的路徑。

以上兩個(gè)步驟可以成功地抽象出缺陷的規(guī)則化描述，并能分析出與該規(guī)則有關(guān)的原子命題和邏輯量詞。通過(guò)分析缺陷的一般模式，發(fā)現(xiàn)大部分原子命題都存在一定的復(fù)用性，若在分析過(guò)程中進(jìn)行統(tǒng)一管理與匹配，將顯著提高靜態(tài)缺陷分析的可擴(kuò)展性，這一發(fā)現(xiàn)正是積木式規(guī)則庫(kù)構(gòu)建的出發(fā)點(diǎn)，也是規(guī)則庫(kù)中元數(shù)據(jù)集的原型。

3.2 積木式構(gòu)建模式

規(guī)則庫(kù)中會(huì)內(nèi)置缺陷規(guī)則的元數(shù)據(jù)，因?yàn)槌绦蚍治鱿到y(tǒng)會(huì)涉及到大量的實(shí)時(shí)事件分析，若采用傳統(tǒng)的狀態(tài)機(jī)模式處理，會(huì)將元數(shù)據(jù)的事件關(guān)聯(lián)全部寫(xiě)入基本處理邏輯之中，使得程序臃腫不堪，同時(shí)嚴(yán)重影響到規(guī)則庫(kù)引擎的響應(yīng)與處理速度。因此，本文采取積木式構(gòu)建模式改進(jìn)這種不足。

積木式構(gòu)建模式將事件分層，通過(guò)簡(jiǎn)單事件來(lái)搭建復(fù)雜事件。其特點(diǎn)是通過(guò)有限種基本事件模型和有限種組合形式，構(gòu)造復(fù)雜的事件。這使得在處理事件的過(guò)程中不用考慮事件間復(fù)雜的因果關(guān)系，符合人們處理事務(wù)時(shí)由簡(jiǎn)單到復(fù)雜的行為習(xí)慣，使事件的處理更為清晰，更專(zhuān)注于事件的關(guān)聯(lián)與匹配。本文利用積木式構(gòu)建模式的優(yōu)點(diǎn)，將與規(guī)則有關(guān)的所有原子命題和邏輯量詞作為底層元數(shù)據(jù)，通過(guò)積木式方法由用戶(hù)自定義缺陷規(guī)則并加入到缺陷規(guī)則集中，供規(guī)則庫(kù)引擎調(diào)用。

以3.1節(jié)中的兩種靜態(tài)缺陷為例，其構(gòu)成的簡(jiǎn)易積木式規(guī)則庫(kù)模型如圖2所示，其中原子命題集、邏輯量詞集、缺陷規(guī)則集均以XM L形式描述。原子命題集存儲(chǔ)了表1中與缺陷有關(guān)的所有原子命題，邏輯量詞集存儲(chǔ)了缺陷有關(guān)的所有邏輯量詞，缺陷規(guī)則集中存儲(chǔ)了CTL形式的由以上兩種元素組成的缺陷規(guī)則。與此同時(shí)，在規(guī)則庫(kù)引擎中會(huì)設(shè)計(jì)原子命題的匹配模塊，實(shí)現(xiàn)原子命題的動(dòng)態(tài)匹配。

圖2 積木式缺陷規(guī)則庫(kù)模型示例圖

需要注意的是，與規(guī)則集有關(guān)的原子命題是原子命題集的一部分，前者由用戶(hù)輸入，后者由系統(tǒng)內(nèi)置。

規(guī)則庫(kù)引擎中的原子命題動(dòng)態(tài)匹配模塊也是積木式模式中的重要組成部分，將在后文中詳述。

4 規(guī)則庫(kù)引擎

規(guī)則庫(kù)引擎是缺陷規(guī)則庫(kù)的核心部分，其功能是將導(dǎo)入的待分析程序建模為K ripke結(jié)構(gòu)的有限狀態(tài)系統(tǒng)，在有限狀態(tài)系統(tǒng)上動(dòng)態(tài)匹配并標(biāo)記與規(guī)則集關(guān)聯(lián)的原子命題集，再將其轉(zhuǎn)換為模型驗(yàn)證器可接受的數(shù)據(jù)結(jié)構(gòu)。

4.1 控制流結(jié)構(gòu)抽取與分析

該步驟關(guān)聯(lián)框架中的控制流結(jié)構(gòu)抽取模塊和命題動(dòng)態(tài)匹配模塊。規(guī)則庫(kù)引擎中源程序的目標(biāo)模型是一種有限狀態(tài)系統(tǒng)，有限狀態(tài)系統(tǒng)的機(jī)制是通過(guò)狀態(tài)變量、輸入變量和常量來(lái)描述不同狀態(tài)下的不同變量；通過(guò)轉(zhuǎn)換關(guān)系來(lái)描述一個(gè)輸入如何導(dǎo)致系統(tǒng)從一個(gè)狀態(tài)轉(zhuǎn)換至多個(gè)狀態(tài)；通過(guò)條件來(lái)描述對(duì)系統(tǒng)各可用路徑的限制，它符合K ripke結(jié)構(gòu)。

4.1.1 控制流結(jié)構(gòu)與K ripke結(jié)構(gòu)

設(shè)計(jì)控制流結(jié)構(gòu)抽取模塊的原因在于源程序控制流結(jié)構(gòu)與K ripke結(jié)構(gòu)的相似性。程序的控制流圖可以用來(lái)表示程序的控制流信息，它是一個(gè)程序所有可能執(zhí)行路徑的抽象表示，基本元素是節(jié)點(diǎn)和有向邊，其中節(jié)點(diǎn)代表的是無(wú)跳轉(zhuǎn)的代碼塊，有向邊是各代碼塊之間的跳轉(zhuǎn)關(guān)系，其數(shù)據(jù)結(jié)構(gòu)為：

其中，V表示節(jié)點(diǎn)有限集，vs表示起始節(jié)點(diǎn)，vf表示終結(jié)節(jié)點(diǎn)，A代表節(jié)點(diǎn)間的有向邊集合。而K ripke結(jié)構(gòu)是添加了原子命題（AP）概念的有限自動(dòng)機(jī)的變種[8]，其結(jié)構(gòu)如下：

其中，S是有限狀態(tài)集；I是初始狀態(tài)集，I?S；R是表示狀態(tài)間轉(zhuǎn)換的二元關(guān)系，R?S×S；L是標(biāo)記方法，L:S→2AP，圖3是一個(gè)簡(jiǎn)單的K ripke結(jié)構(gòu)范例。

該K ripke結(jié)構(gòu)可描述為：

由此可見(jiàn)，將源程序轉(zhuǎn)換為K ripke結(jié)構(gòu)只需經(jīng)過(guò)兩個(gè)步驟，首先是從源程序抽取出控制流結(jié)構(gòu)，然后通過(guò)遍歷控制流節(jié)點(diǎn)，對(duì)原子命題集中的原子命題進(jìn)行動(dòng)態(tài)匹配，若某個(gè)節(jié)點(diǎn)滿(mǎn)足某一命題，則在該節(jié)點(diǎn)標(biāo)記該命題為真。

4.1.2 利用Soot抽取及分析控制流結(jié)構(gòu)

直接通過(guò)字節(jié)碼取得控制流會(huì)遇到表達(dá)式指令不夠清晰，表達(dá)式樹(shù)構(gòu)造過(guò)于復(fù)雜[9]等情況，本文以Java程序分析為例，選擇Soot代替手工分析字節(jié)碼來(lái)抽取和分析控制流。Soot是開(kāi)源的Java字節(jié)碼分析與轉(zhuǎn)換工具[10]，既可以作為單獨(dú)的類(lèi)優(yōu)化與檢查工具來(lái)使用，也可以作為Java字節(jié)碼的優(yōu)化與轉(zhuǎn)換框架，其最新版本可支持嵌入集成開(kāi)發(fā)環(huán)境，使得程序的分析更為易用和高效。本文在獲得控制流結(jié)構(gòu)的同時(shí)還需對(duì)控制流節(jié)點(diǎn)進(jìn)行分析，因此需要觸及到Soot的表現(xiàn)形式并深入到類(lèi)結(jié)構(gòu)。

首先，要抽取出控制流結(jié)構(gòu)，需要認(rèn)識(shí)Soot的中間表示——IR。Soot提供了四種用于代碼分析的中間表現(xiàn)形式，它們分別是：Baf、Grimp、Jimple、Shim ple[11]。每種IR都針對(duì)不同的分析做了不同程度的抽象，其中，Jimple是Soot的最主要IR，也是本文抽取和分析控制流信息時(shí)的主要操作對(duì)象。

由于待分析程序結(jié)構(gòu)的多樣化，控制流的抽取也需針對(duì)不同場(chǎng)景[12]，Soot構(gòu)建了五種場(chǎng)景結(jié)構(gòu)：Scene、SootClass、SootM ethod、SootField及Body，分別表示待檢測(cè)程序本身、某個(gè)待檢測(cè)類(lèi)、類(lèi)中的某個(gè)方法、類(lèi)中的某個(gè)成員、函數(shù)體。Body與不同的IR相對(duì)應(yīng)，本文分析采用了Jimple作為IR，故使用Jim pleBody作為方法的主要載體，以方法為單位，抽取程序的控制流信息。

目前人們多通過(guò)Soot的命令行工具和Eclipse插件來(lái)查看程序的控制流結(jié)構(gòu)[13]，這不利于在抽取過(guò)程中對(duì)控制流節(jié)點(diǎn)進(jìn)行分析，因此本文采用了繼承Soot的Transformer類(lèi)并重寫(xiě)其InternalTransform方法來(lái)解決該問(wèn)題，流程如下：

（1）根據(jù)取得的JmpleBody，通過(guò)getMethod方式取得method。

（2）以Body為參數(shù)，通過(guò)BriefUnitGraph構(gòu)建Unit-Graph，得到控制流圖的基本結(jié)構(gòu)。

（3）遍歷UnitGraph，對(duì)每個(gè)節(jié)點(diǎn)使用getSuccsof遍歷分支節(jié)點(diǎn)。

由此即可實(shí)現(xiàn)控制流結(jié)構(gòu)的抽取及遍歷，為下一步原子命題的動(dòng)態(tài)匹配提供基礎(chǔ)。

4.2 動(dòng)態(tài)匹配原子命題

原子命題的動(dòng)態(tài)匹配是控制流結(jié)構(gòu)轉(zhuǎn)換的輔助模塊，它是在遍歷程序控制流節(jié)點(diǎn)的過(guò)程中，對(duì)與規(guī)則集相關(guān)的原子命題按照一定的匹配規(guī)則進(jìn)行動(dòng)態(tài)匹配。下面將從匹配規(guī)則和動(dòng)態(tài)匹配機(jī)制兩方面介紹該模塊。

4.2.1 原子命題匹配規(guī)則

圖3 K ripke結(jié)構(gòu)

本文詳細(xì)分析了Jimple之后，發(fā)現(xiàn)可以通過(guò)Jim ple的聲明（Statement）實(shí)現(xiàn)原子命題的匹配，因?yàn)镴imple是類(lèi)型化的基于聲明的IR，與Java字節(jié)碼中約200個(gè)指令數(shù)相比，Jimple只需掌握15種Statement就能更加方便、標(biāo)準(zhǔn)地描述程序。在遍歷控制流節(jié)點(diǎn)過(guò)程中，針對(duì)每個(gè)節(jié)點(diǎn)，取得其Statement類(lèi)型，以此為基礎(chǔ)取得命題匹配條件以及標(biāo)記命題所需的其他參數(shù)，完成原子命題的匹配。

對(duì)不同的原子命題而言，其匹配條件也各有不同，前文已經(jīng)提到，完善功能的系統(tǒng)中會(huì)內(nèi)置與一般缺陷或某一類(lèi)缺陷有關(guān)的所有原子命題，構(gòu)成原子命題集。因此，需要為原子命題集中的每種命題定義匹配規(guī)則。以圖2中的原子命題集為例，其對(duì)應(yīng)的匹配條件如表2。

表2 原子命題的Jim ple匹配條件

文中，原子命題的匹配與缺陷類(lèi)型是分開(kāi)的，在原子命題集體積較小時(shí)，原子命題的匹配機(jī)制并不會(huì)對(duì)規(guī)則庫(kù)引擎的處理速度造成很大影響，但隨著原子命題集涵蓋范圍逐漸變廣，則需要定義更為高效的動(dòng)態(tài)匹配機(jī)制。

4.2.2 改進(jìn)的原子命題匹配機(jī)制

常見(jiàn)的元素匹配機(jī)制是通過(guò)分支判定語(yǔ)句if-else進(jìn)行逐層比對(duì)，直至進(jìn)入判定結(jié)果為真的分支，該做法存在三方面的隱患：

（1）當(dāng)待判定元素過(guò)多時(shí)，將會(huì)相應(yīng)產(chǎn)生更多的判定語(yǔ)句，這可能會(huì)導(dǎo)致某些元素要經(jīng)過(guò)很長(zhǎng)的時(shí)間才能進(jìn)入其判定分支，影響處理速度。

（2）若判定分支中的處理語(yǔ)句過(guò)于復(fù)雜，當(dāng)判定元素過(guò)多時(shí)，會(huì)造成判定程序體積過(guò)大。

（3）判定程序與各原子命題的匹配方法耦合性過(guò)高，無(wú)法有效地管理每種元素的判定規(guī)則。

為解決該匹配機(jī)制造成的隱患，本文結(jié)合IOC思想設(shè)計(jì)了一種新的匹配方式，基于接口依賴(lài)注入的原子命題動(dòng)態(tài)匹配機(jī)制。

IOC即控制反轉(zhuǎn)，其中心思想是通過(guò)面向?qū)ο蠓▌t來(lái)解耦程序，也稱(chēng)依賴(lài)注入[14]，它通過(guò)外部實(shí)體調(diào)控系統(tǒng)內(nèi)所有對(duì)象，在對(duì)象創(chuàng)建時(shí)返回該對(duì)象所依賴(lài)的引用。本文實(shí)現(xiàn)該機(jī)制的方法與規(guī)則庫(kù)的積木式模式相輔相成，為規(guī)則庫(kù)原子命題集中的每個(gè)原子命題定義匹配對(duì)象APmodelImp，且所有對(duì)象都實(shí)現(xiàn)通用接口Base-APmodel及其方法checkAP（），作為對(duì)應(yīng)的原子命題匹配方法。在主程序中只需遍歷原子命題集，根據(jù)命題集中的匹配對(duì)象名反射出對(duì)象的引用，賦值給通用接口，由通用接口調(diào)用匹配方法，具體實(shí)現(xiàn)見(jiàn)程序1。

程序1原子命題動(dòng)態(tài)標(biāo)記算法偽代碼

輸入：程序控制流信息，原子命題集

輸出：標(biāo)記原子命題的控制流

Begin

for控制流節(jié)點(diǎn)node do

for原子命題集元素ap do

根據(jù)ap的名稱(chēng)反射出ap對(duì)應(yīng)的匹配類(lèi)APModelImp；

將APModelImp實(shí)例化所得引用賦給BaseAPModel；

i

f BaseAPModel.checkAP（）為真then

創(chuàng)建原子命題標(biāo)記對(duì)象APObject；

關(guān)聯(lián)node與APObject；

將APObject加入標(biāo)記對(duì)象集合APLlist；

end if

end for

end for

end

4.3 模型轉(zhuǎn)換

規(guī)則庫(kù)引擎中模型轉(zhuǎn)換模塊的最終目標(biāo)，是將前兩個(gè)功能模塊所得的K ripke結(jié)構(gòu)轉(zhuǎn)換為NuSMV模型驗(yàn)證器所接受的SMV語(yǔ)言[15]的同時(shí)保留程序的控制流節(jié)點(diǎn)信息及行信息，構(gòu)造缺陷集中各缺陷的實(shí)例，實(shí)現(xiàn)對(duì)缺陷和缺陷檢測(cè)結(jié)果的管理。

由此可見(jiàn)，該模塊首先要定義符合規(guī)則庫(kù)模型的SMV語(yǔ)言結(jié)構(gòu)，同時(shí)需要設(shè)計(jì)大量數(shù)據(jù)結(jié)構(gòu)與相應(yīng)的轉(zhuǎn)換算法。

規(guī)則庫(kù)引擎將本文分析缺陷所需的SMV結(jié)構(gòu)定義為以下四部分，以缺陷實(shí)例的構(gòu)造為入口，設(shè)計(jì)了對(duì)應(yīng)的數(shù)據(jù)結(jié)構(gòu)，見(jiàn)表3。這四部分的構(gòu)造方式如下：

（1）遍歷輸出NodeLink中的所有控制流節(jié)點(diǎn)S；

表3 數(shù)據(jù)結(jié)構(gòu)

（2）取NodeLink頭節(jié)點(diǎn)作為初始節(jié)點(diǎn)I，遍歷并輸出NodeLink中每個(gè)節(jié)點(diǎn)的后繼節(jié)點(diǎn)，得到狀態(tài)轉(zhuǎn)換關(guān)系R；

（3）遍歷APList得到原子命題集合L；

（4）遍歷BugList，取出每個(gè)BugObject中的AssertionString，獲得CTL形式的斷言集合A。

以上數(shù)據(jù)結(jié)構(gòu)均通過(guò)在動(dòng)態(tài)匹配模塊中遍歷控制流節(jié)點(diǎn)，分析元數(shù)據(jù)中的原子命題集與規(guī)則集實(shí)現(xiàn)其構(gòu)造。

5 原型系統(tǒng)與實(shí)驗(yàn)結(jié)果

依據(jù)圖2中的積木式規(guī)則庫(kù)模型，實(shí)現(xiàn)了原型系統(tǒng)以驗(yàn)證本文提出的構(gòu)造方法的可行性與有效性。首先是規(guī)則集的構(gòu)建，如圖4，用戶(hù)根據(jù)元數(shù)據(jù)來(lái)自定義缺陷，同時(shí)指定缺陷名稱(chēng)，加入規(guī)則集，圖中三個(gè)列表分別代表從XM L文件轉(zhuǎn)換而來(lái)的原子命題集、邏輯量詞集和缺陷規(guī)則集。列表頂部為編輯區(qū)域，用于規(guī)則的添加和更新。缺陷規(guī)則列表中顯示了規(guī)則名稱(chēng)和規(guī)則的邏輯公式，可以通過(guò)點(diǎn)擊“edit”或“del”按鈕實(shí)現(xiàn)規(guī)則的編輯和刪除；點(diǎn)擊“添加規(guī)則”按鈕，實(shí)現(xiàn)規(guī)則的添加。

圖4 原型系統(tǒng)-規(guī)則庫(kù)管理

添加規(guī)則成功后，即可進(jìn)入原型系統(tǒng)的檢測(cè)界面，如圖5，左側(cè)是被檢測(cè)的源程序，首先根據(jù)缺陷集和元數(shù)據(jù)集對(duì)源程序進(jìn)行建模，得到SMV結(jié)構(gòu)的有限狀態(tài)系統(tǒng)，建模結(jié)果如程序2（由于建模結(jié)果較長(zhǎng)，只截取其中代表性的部分）。建模結(jié)果的VAR標(biāo)簽下輸出源程序的全部控制流節(jié)點(diǎn)，ASSIGN標(biāo)簽下輸出控制流節(jié)點(diǎn)的轉(zhuǎn)換關(guān)系，DEFINE標(biāo)簽下輸出已標(biāo)記的原子命題同時(shí)指出原子命題標(biāo)記的控制流節(jié)點(diǎn)。

程序2建模結(jié)果

MODULE main

VAR

state：{stat0，stat1，…，stat15}；

ASSIGN

圖5 原型系統(tǒng)-輸入流關(guān)閉異常的反例路徑

init（state）：=stat0；

next（state）：=case

state=stat0：{stat1}；

state=stat1：{stat2}；

state=stat2：{stat3}；

state=stat3：{stat4，stat6}；

state=stat4：{stat5}；

...

state=stat14：{stat15}；

TRUE：state；

esac；

DEFINE

param_r0：=state in{stat0}；

assign_null_n0：=state in{stat1}；

invoked_r0：=state in{stat2}；

invoked_n0：=state in{stat6}；

malloc_fin_r1：=state in{stat7}；

free_fin_r1：=state in{stat10}；

if_null_r0：=FALSE；

圖5中右側(cè)為檢測(cè)結(jié)果，源程序共檢測(cè)出三個(gè)缺陷，分別為空指針異常NullException，文件輸入流關(guān)閉異常InputException以及入?yún)⑴锌债惓aram IfNullException。點(diǎn)擊缺陷條目，在“Counter Example”區(qū)域會(huì)顯示反例路徑，同時(shí)代碼區(qū)域會(huì)標(biāo)記反例行信息。反例路徑中的每個(gè)節(jié)點(diǎn)以按鈕方式顯示，以節(jié)點(diǎn)名加行號(hào)作為按鈕名稱(chēng)，通過(guò)點(diǎn)擊節(jié)點(diǎn)按鈕，可以定位到代碼中該節(jié)點(diǎn)對(duì)應(yīng)的行，從而實(shí)現(xiàn)反例重現(xiàn)。從反例路徑可以很容易得出導(dǎo)致輸入流未關(guān)閉異常的原因：在行12處開(kāi)啟了輸入流后，跳轉(zhuǎn)至catch塊繼續(xù)執(zhí)行至結(jié)束，因而導(dǎo)致輸入流未關(guān)閉。

空指針異常的反例路徑如圖6所示?？梢缘贸鰧?dǎo)致缺陷的原因是在行5處將變量賦值為null，當(dāng)args.length小于或等于0時(shí)，程序運(yùn)行到行9，造成空指針異常。

圖6 原型系統(tǒng)-空指針異常的反例路徑

入?yún)⑴锌债惓５姆蠢窂饺鐖D7，其含義是指“因方法入?yún)⒆兞吭谝们拔催M(jìn)行判空而可能引發(fā)的空指針異?！?，其CTL公式的表示形式為：

AG(param&EF invoked-＞A[!invoked U if_null])其中原子命題param表示方法的輸入?yún)?shù)，invoked指引用對(duì)象的屬性或方法，if_null表示判斷對(duì)象是否為空值。該CTL描述的語(yǔ)義是“對(duì)任意路徑下的所有狀態(tài)，若某一個(gè)狀態(tài)定義了方法的入?yún)⒆兞壳椅磥?lái)存在一個(gè)狀態(tài)對(duì)該變量進(jìn)行了引用，則直到對(duì)變量判空之前不會(huì)對(duì)該變量進(jìn)行引用”。由圖7可以得出，方法入?yún)rgs在第6行引用其length屬性之前沒(méi)有進(jìn)行判空，若傳入的args為空則會(huì)導(dǎo)致空指針異常。

圖7 原型系統(tǒng)-入?yún)⑴锌债惓５姆蠢窂?/p>

為進(jìn)一步驗(yàn)證方法的適用性，以開(kāi)源軟件JBoss中的部分代碼作為檢測(cè)范例。從圖8中可以發(fā)現(xiàn)，原型系統(tǒng)檢測(cè)出一條空指針異常。導(dǎo)致缺陷的原因是：在行20處將對(duì)象response置為null后，在行27調(diào)用了其方法，由此引發(fā)空指針異常。

圖8 原型系統(tǒng)-JBoss代碼檢測(cè)結(jié)果

實(shí)驗(yàn)結(jié)果表明，可以利用元數(shù)據(jù)集合中的原子命題將缺陷成功抽象為CTL表示，實(shí)現(xiàn)積木式缺陷規(guī)則集的構(gòu)建；待檢測(cè)程序經(jīng)過(guò)模型抽取、標(biāo)記與轉(zhuǎn)換過(guò)后能夠成功檢測(cè)出存在的缺陷，實(shí)現(xiàn)反例路徑跟蹤。

同時(shí)，在分析實(shí)驗(yàn)結(jié)果的過(guò)程中也發(fā)現(xiàn)，與其他基于靜態(tài)分析技術(shù)的源碼檢測(cè)工具類(lèi)似，本文提出的方法不能處理動(dòng)態(tài)代碼關(guān)聯(lián)的原子命題，因此不可避免地會(huì)出現(xiàn)檢測(cè)結(jié)果的漏報(bào)與誤報(bào)。此外，檢測(cè)的準(zhǔn)確性還依賴(lài)于控制流圖的準(zhǔn)確構(gòu)建及狀態(tài)到原子命題的映射?？赏ㄟ^(guò)使用高效且準(zhǔn)確的控制流抽取方法以及清晰的控制流節(jié)點(diǎn)的中間表示形式從外部來(lái)降低這兩種依賴(lài)性帶來(lái)的隱患；細(xì)化原子命題匹配規(guī)則及缺陷的邏輯描述，減少靜態(tài)分析方法可控范圍內(nèi)的漏報(bào)與誤報(bào)。

6 結(jié)束語(yǔ)

從形式化規(guī)約的角度出發(fā)，構(gòu)建積木式缺陷規(guī)則庫(kù)，在研究過(guò)程中實(shí)現(xiàn)了規(guī)則集的自動(dòng)構(gòu)建；源程序到有限狀態(tài)系統(tǒng)的動(dòng)態(tài)建模；結(jié)合規(guī)則集和NuSMV模型檢測(cè)器進(jìn)行模型檢查，返回帶有源程序行信息的缺陷路徑，實(shí)現(xiàn)原型系統(tǒng)驗(yàn)證了本文方法的有效性。

在當(dāng)前的基礎(chǔ)上，仍需進(jìn)一步研究的問(wèn)題是：對(duì)不同原子命題的匹配規(guī)則進(jìn)行分析，提取共性部分，為存在共性的原子命題制定通用轉(zhuǎn)換規(guī)則，提高匹配效率及匹配準(zhǔn)確性；擴(kuò)充原子命題集，以擴(kuò)大缺陷檢測(cè)的覆蓋率，進(jìn)一步提升軟件的可用性。

[1]A rtzi S，Kiezun A，Dolby J，et al.Finding bugs in Web applications using dynamic test generation and explicitstate model checking[J].IEEE Transactions on Software Engineering，2010，36（4）：474-494.

[2]Ball T，Levin V，Rajamani S K.A decade of software model checking with SLAM[J].Communications of the ACM，2011，54（7）：68-76.

[3]Yoo J，Jee E，Cha S.Formal modeling and verification of safety-critical software[J].Software，2009，26（3）：42-49.

[4]Choppy C，K lai K，Zidani H.Formal verification of UML state diagrams：a petri net based approach[J].ACM SIGSOFT Software Engineering Notes，2011，36（1）：1-8.

[5]Sl?tten V，K raemer F A，Herrmann P.Towards automatic generation of formal specifications to validate and verify reliable distributed systems：a method exemplified by an industrial case study[J].ACM SIGPLAN Notices，2012，47（3）：147-156.

[6]Cordeiro L，F(xiàn)ischer B，Marques-Silva J.SMT-based bounded model checking for embedded ANSI-C software[J].IEEE Transactions on Software Engineering，2012，38（4）：957-974.

[7]Ljungkrantz O，Akesson K，F(xiàn)abian M，et al.Formal specification and verification of industrial control logic components[J].IEEE Transactions on Automation Science and Engineering，2010，7（3）：538-548.

[8]Fioravanti F，Pettorossi A，Proietti M，et al.Generalization strategies for the verification of infinite state systems[J].TPLP，2013，13（2）：175-199.

[9]Liu P，Zhang C.Pert：the application-aware tailoring of java object persistence[J].IEEE Transactions on Software Engineering，2012，38（4）：909-922.

[10]FitzRoy-Dale N，Kuz I，Heiser G.Architecture optimisation with currawong[J].ACM SIGCOMM Computer Communication Review，2011，41（1）：115-119.

[11]Zhou C，F(xiàn)rankl P.JDAMA：Java database application mutation analyser[J].Software Testing，Verification and Reliability，2011，21（3）：241-263.

[12]Eichberg M，Sewe A.Encoding the Java virtual machine’s instruction set[J].Electronic Notes in Theoretical Computer Science，2011，264（4）：35-50.

[13]Girard A，Pola G，Tabuada P.Approximately bisimilar symbolic models for incrementally stable switched systems[J].IEEE Transactions on Automatic Control，2010，55（1）：116-126.

[14]Chang C，Lu C.Pattern-based framework for modularized software development and evolution robustness[J].Information and Software Technology，2011，53（4）：307-316.

[15]A rcaini P，Gargantini A，Riccobene E.A model advisor for NuSMV specifications[J].Innovations in Systems and Software Engineering，2011，7（2）：97-107.