黃吳丹，嚴(yán)俊琦

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院,江蘇 南京 210016)

路由協(xié)議的自動形式化驗證方法研究

黃吳丹，嚴(yán)俊琦

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院,江蘇 南京 210016)

路由協(xié)議被廣泛部署于因特網(wǎng)中用來進(jìn)行路由信息的交換與路徑的選擇，確保路由協(xié)議正確、安全的運行是計算機(jī)網(wǎng)絡(luò)的基礎(chǔ)問題之一。近年來，形式化驗證已成功應(yīng)用于協(xié)助路由協(xié)議的設(shè)計和實現(xiàn),形式化方法的使用能夠找到軟件測試過程中難以發(fā)現(xiàn)的系統(tǒng)缺陷，從而有效地提高系統(tǒng)的安全性。主要介紹了自動形式化驗證的幾類主要技術(shù)基礎(chǔ)：模型檢驗、定理證明和等價性驗證。總結(jié)了自動形式化驗證路由協(xié)議的方法和優(yōu)缺點以及它們在各個方面的研究進(jìn)展和使用狀況，為相關(guān)方向的研究者在使用形式化方法驗證路由協(xié)議時提供了參考依據(jù)。最后總結(jié)了該領(lǐng)域的研究狀況，并對未來研究熱點進(jìn)行了預(yù)測和展望，提出了一些可行的研究方向。

路由協(xié)議;形式化驗證;模型檢驗;定理證明

0 引 言

路由協(xié)議通過路徑選擇實現(xiàn)信息交換功能，提高計算機(jī)網(wǎng)絡(luò)的數(shù)據(jù)傳輸效率。路由協(xié)議不僅在因特網(wǎng)核心部分的路由器上運行，還在移動自組網(wǎng)(MANET)、面向應(yīng)用層的覆蓋網(wǎng)(例如P2P網(wǎng)絡(luò))這些新型網(wǎng)絡(luò)上擔(dān)任重要角色。特別是在移動自組網(wǎng)中，所有節(jié)點都支持路由發(fā)現(xiàn)和維護(hù)，節(jié)點的動態(tài)變化導(dǎo)致網(wǎng)絡(luò)拓?fù)洳还潭?，移動自組網(wǎng)本身的應(yīng)用領(lǐng)域都要求設(shè)計新的有特色的路由協(xié)議。

因特網(wǎng)上的路由選擇主要分為兩類：距離向量協(xié)議和鏈路狀態(tài)協(xié)議。移動自組網(wǎng)上的路由協(xié)議分為被動式、主動式和混合式三類[1]。被動式通常由表驅(qū)動，可根據(jù)路由表預(yù)先獲取路由；主動式在需要時才進(jìn)行路由發(fā)現(xiàn)；混合式結(jié)合被動式和主動式的特點靈活選擇路由。P2P網(wǎng)絡(luò)因其無中心、動態(tài)性和基于應(yīng)用層的特點，路由算法的優(yōu)劣應(yīng)考慮效率、易用性、可擴(kuò)展性等方面。

一個好的路由協(xié)議應(yīng)是正確、穩(wěn)健、有效的，同時根據(jù)應(yīng)用網(wǎng)絡(luò)的特點具有不同能力。此外，面對外部的攻擊威脅，路由協(xié)議應(yīng)具有抵御和處理能力。為了尋找路由協(xié)議設(shè)計缺陷、發(fā)現(xiàn)攻擊威脅，近年來已有大量研究者使用形式化方法，特別是形式化驗證技術(shù)解決此類問題。

文中總結(jié)了近年來使用自動形式化驗證技術(shù)驗證路由協(xié)議的正確性(correctness)和安全性(security)的方法及其相應(yīng)的優(yōu)缺點。正確性是諸如無環(huán)、收斂、死鎖這類問題，安全性是像文獻(xiàn)[2]這種關(guān)注外部攻擊對協(xié)議穩(wěn)健性的影響。

1 形式化驗證技術(shù)分類

形式化方法是基于數(shù)學(xué)的語言、技術(shù)和工具，用來幫助開發(fā)軟硬件系統(tǒng)[3]。形式化驗證是形式化方法的一個研究內(nèi)容，根據(jù)系統(tǒng)的形式化規(guī)約或?qū)傩詠碜C明系統(tǒng)的正確性，在計算機(jī)硬件、控制系統(tǒng)、通信協(xié)議、安全關(guān)鍵軟件等領(lǐng)域有大量應(yīng)用[4-6]。相對于傳統(tǒng)的模擬、仿真和測試，形式化驗證是一種窮盡式的數(shù)學(xué)技術(shù)，因此不需要花費過多時間關(guān)注輸入條件或測試用例，保證了測試的覆蓋率。

手動驗證常用來提高人員對系統(tǒng)的理解，驗證過程像數(shù)學(xué)證明那樣，常用自然語言進(jìn)行。但因為證明層次高且自然語言存在固有的歧義性，系統(tǒng)中的一些錯誤，特別是底層錯誤，不能有效發(fā)現(xiàn)。此外，由于系統(tǒng)復(fù)雜度越來越高，手動證明也不適合用于這些研究。驗證過程的自動化能提高形式化驗證的易用性。目前，已有大量工具支持自動的形式化驗證，它們主要基于模型檢驗、定理證明和等價性檢驗三類技術(shù)原理。

1.1 模型檢驗

模型檢驗(model checking)建立系統(tǒng)的有限狀態(tài)模型，在驗證時窮舉搜索狀態(tài)空間，檢查模型是否滿足性質(zhì)。性質(zhì)包括安全性(safety)和活性(liveness)。安全性描述“壞的事情永遠(yuǎn)(always)不會發(fā)生”，例如斷言始終為真、空指針不能被引用、緩沖區(qū)禁止溢出?；钚悦枋觥昂玫氖虑榻K(eventually)將發(fā)生”，例如程序最終總會終止運行、請求的服務(wù)總能被響應(yīng)。性質(zhì)的表示方法多種多樣，可由時序邏輯表示，例如線性時序邏輯(LTL)和計算樹邏輯(CTL)[7]，也可通過斷言等方式表達(dá)的不變式表示。如果性質(zhì)不滿足，將提供反例執(zhí)行路徑。

模型中變量數(shù)目多、數(shù)據(jù)類型寬度大、函數(shù)調(diào)用、動態(tài)內(nèi)存分配等都會使?fàn)顟B(tài)空間迅速變大，分布系統(tǒng)模型中進(jìn)程的交錯執(zhí)行也會使?fàn)顟B(tài)數(shù)目呈指數(shù)增長，這種狀態(tài)空間的急速增長稱為狀態(tài)爆炸問題，是模型檢驗的瓶頸問題。為緩解該問題，已提出多種通過壓縮和減少狀態(tài)數(shù)的方法，例如符號表示、偏序歸約、組合推理、抽象、對稱約簡等。

模型檢驗是形式化驗證的研究熱點，原理簡單且較為實用。目前已有大量模型檢驗工具[8]提供高度自動化的驗證，并自動生成反例。但是網(wǎng)絡(luò)的分布特性使?fàn)顟B(tài)爆炸問題更突出，這也是使用模型檢驗驗證路由協(xié)議時應(yīng)關(guān)注的一個主要問題。

1.2 定理證明

定理證明(theorem proving)從待驗證系統(tǒng)抽取出模型，由一階邏輯或高階邏輯表示。這個邏輯系統(tǒng)是一個形式化系統(tǒng)，由公理和推理規(guī)則組成。驗證過程在實驗者指導(dǎo)下，對公理和已證明的定理使用推理規(guī)則，產(chǎn)生新的定理。目前存在多種具有一定自動化程度的定理證明工具，它們內(nèi)嵌一部分決策過程和證明技術(shù)，并由實驗者協(xié)助完成證明。典型的工具有HOL[9]和PVS[10]。HOL用函數(shù)式語言和高階邏輯描述形式化規(guī)約和屬性，PVS的規(guī)約語言也基于高階邏輯。HOL需要更詳細(xì)的人工引導(dǎo)，因此靈活性較大，PVS自動化程度更高，但靈活性差一些。

定理證明具有高度抽象、邏輯表達(dá)能力強(qiáng)的特點，能驗證具有無限狀態(tài)的系統(tǒng)。但是它的抽象較困難、人工參與度高，使用者應(yīng)具有相關(guān)的邏輯知識和經(jīng)驗，因此實用定理證明的研究進(jìn)度會很慢。

1.3 等價性檢驗

等價性檢驗(equivalence checking)是驗證同一個系統(tǒng)的兩種不同抽象層次是否一致的技術(shù)。它大量應(yīng)用在工業(yè)界，特別是硬件電路的驗證上，例如比較門級網(wǎng)表和RTL設(shè)計的一致性。軟件程序的等價性檢驗將軟件轉(zhuǎn)化為具有不同組合的狀態(tài)機(jī)，給定輸入，檢查是否產(chǎn)生相同的輸出。軟件程序的等價性檢驗關(guān)注同一項目的不同設(shè)計層次，能使開發(fā)過程的前后保持一致，但是不擅長檢查程序缺陷。

2 基于模型檢驗的方法

目前大部分研究都是從路由協(xié)議的標(biāo)準(zhǔn)文檔或形式化規(guī)約中抽取出模型，用模型檢驗工具驗證該模型是否滿足性質(zhì)。為減小狀態(tài)空間，模型應(yīng)該越小越好，但也應(yīng)該保持模型的表達(dá)能力。因此建模要在緩解狀態(tài)爆炸問題和保持模型表達(dá)能力間進(jìn)行權(quán)衡。

(3)菲尼爾濾光片因為性能要求的不同而具有不同的焦距，即是我們平時所說的感應(yīng)距離。因此，它會產(chǎn)生不同的監(jiān)控視場。視場越多，控制越嚴(yán)密。

一個建議的建模和驗證方法[11]是，初始時為提高建模速度，可以先構(gòu)造一個簡單、粗糙的模型，對該模型進(jìn)行驗證，然后用逐步求精的方法建立一個適度的模型。這個逐步求精的過程可根據(jù)驗證結(jié)果(例如反例)來實現(xiàn)。以下三點為該方法中應(yīng)該注意的內(nèi)容。

(1)模型抽取。

應(yīng)充分獲取協(xié)議信息，簡化和假設(shè)協(xié)議的行為和參數(shù)，明確節(jié)點可發(fā)送和接收的消息格式，建立協(xié)議的偽代碼或有限狀態(tài)機(jī)的描述。通常包括對節(jié)點、通信鏈路、低層服務(wù)、配置和策略、網(wǎng)絡(luò)拓?fù)涞暮喕图僭O(shè)[12-14]。例如，研究BGP的路由策略時，假設(shè)協(xié)議機(jī)制是可靠的。研究自組網(wǎng)協(xié)議時，將網(wǎng)絡(luò)拓?fù)涑橄蟪删哂腥惞?jié)點的網(wǎng)絡(luò)，即源節(jié)點、目的節(jié)點和中間節(jié)點集合[15-16]。此外，還可根據(jù)驗證的性質(zhì)，假設(shè)其他部分是可靠運行的。例如，在研究AODV時間方面的正確性時，可構(gòu)造一個具有靜態(tài)、線性拓?fù)涞腁ODV時間相關(guān)的UPPAAL模型。

(2)建模。

根據(jù)抽取后的協(xié)議描述建立一個可運行的模型，該模型應(yīng)進(jìn)一步抽象。例如，計時器能生成的Time To Live (TTL)信息，為簡化模型，可用SPIN[17]建模語言Promela中非確定性的分支語句模擬：

bool TTL;

::ture->TTL=1;

::true->TTL=0; //表示TTL結(jié)束

fi

(3)驗證。

搜索狀態(tài)空間的驗證過程是自動化的[18-22]，但反例的分析是人工的。對模型驗證呈現(xiàn)的反例，應(yīng)確認(rèn)它是屬于協(xié)議本身引起的錯誤還是建模不當(dāng)引起的偽反例。前者表明協(xié)議存在錯誤，應(yīng)進(jìn)一步確認(rèn)，提出解決辦法；后者表明該模型與協(xié)議存在不一致，應(yīng)修改模型以再次驗證。

2.1 工具的選擇

具有良好界面和易于學(xué)習(xí)的支撐工具能降低模型檢驗的使用難度，適合描述路由協(xié)議的建模語言和內(nèi)嵌的緩解狀態(tài)爆炸問題的策略，能有效提高驗證效率。SPIN和UPPAAL是常用的工具。SPIN的建模語言Promela支持非確定性選擇，并發(fā)進(jìn)程和信道模擬的同步、異步通信，支持嵌入C代碼，性質(zhì)用斷言和LTL公式描述，能自動生成反例，并提供多種可選的無損壓縮和有損壓縮技術(shù)。UPPAAL用時間自動機(jī)網(wǎng)絡(luò)描述系統(tǒng)行為，同樣支持非確定性過程和信道通信，用CTL公式描述性質(zhì)，能自動生成反例，適合驗證多種系統(tǒng)，特別是實時系統(tǒng)。

文獻(xiàn)[23]對移動自組網(wǎng)路由協(xié)議(WARP)抽象出一個5節(jié)點模型，用SPIN驗證其正確性。驗證時由于狀態(tài)數(shù)巨大，作者使用了SPIN支持的位狀態(tài)哈希技術(shù)壓縮內(nèi)存，使驗證時間控制在30 min之內(nèi)，而狀態(tài)空間的平均覆蓋率卻達(dá)到98%。

2.2 歸 約

歸約方法(reduction-based)通過合并或刪除網(wǎng)絡(luò)節(jié)點來減小模型規(guī)模。文獻(xiàn)[24]對一個BGP組合模型SPP[25]進(jìn)行擴(kuò)展并實行歸約，最后驗證了BGP的路由振蕩特性。該方法可應(yīng)用在含有iBGP或eBGP的網(wǎng)絡(luò)上，實驗使用基于Maude[26]開發(fā)的工具包，使歸約過程實現(xiàn)自動化，最后通過模型檢驗實現(xiàn)驗證。實驗數(shù)據(jù)表明，驗證效率大大提高，相比文獻(xiàn)[27]，驗證節(jié)點數(shù)目從25增加到100以上。在此方法的基礎(chǔ)上，文獻(xiàn)[28]提出一個BGP形式化模型EPD和兩條歸約規(guī)則：重復(fù)歸約和互補歸約，并證明了該方法的可靠性和局部完備性?？煽啃员砻魅绻麣w約后模型G'是安全的，那么相應(yīng)歸約前的模型G也是安全的；如果G'存在路由振蕩，那么G中至少存在一條執(zhí)行路徑能產(chǎn)生路由振蕩。局部完備性表明，只要知道節(jié)點的局部拓?fù)湫畔?，就可進(jìn)行有效歸約。

上述歸約方法能提高驗證效率并增加驗證規(guī)模，但是存在兩個缺點。一方面歸約規(guī)則沒有普遍適用性，其他類型的協(xié)議需要提出不同的規(guī)則，因此歸約方法難度較大。另一方面，雖然上述歸約方法實現(xiàn)了自動化，但過于依賴工具的支持。例如，文獻(xiàn)[29]中也提出了類似的方法，將OSPF協(xié)議的模型歸約成參數(shù)化網(wǎng)絡(luò)(或抽象網(wǎng)絡(luò))，讓一個參數(shù)化網(wǎng)絡(luò)代表一類實際網(wǎng)絡(luò)模型的集合，但該方法只能手動完成，因此實用性較差。

2.3 有界模型檢驗

有界模型檢驗[30]是針對基于BDD/OBDD模型檢驗的不足而提出的新型技術(shù)。它通過設(shè)置驗證邊界上界K產(chǎn)生有界模型，再把該模型編碼成SAT/SMT實例，最后利用SAT/SMT求解器進(jìn)行求解。如果性質(zhì)被違反，找到的反例通常是長度最短、最簡單的反例；如果是無反例的，那么模型在運行到K階段時是安全的，是否需要增加K值以再次驗證由實驗者決定，但如果能找到一個完備性閾值[31]，那么在此閾值內(nèi)的驗證結(jié)果與無限階段的驗證是等價的。已有研究表明，當(dāng)驗證邊界上界K小于60時，有界模型檢驗優(yōu)于傳統(tǒng)的模型檢驗[32]。

目前使用有界模型檢驗驗證路由協(xié)議的研究不多，只有Adi Sosnovich等使用有界模型檢驗工具CBMC[33]驗證了OSPF協(xié)議的安全性，并找到未發(fā)表過的攻擊。實驗結(jié)果表明，有界模型檢驗適合驗證期望找到反例的模型，但是如果用來證明正確性成立(例如希望協(xié)議具有無環(huán)特征)，那么建?；?qū)ふ彝陚湫蚤撝档碾y度較大。

2.4 系統(tǒng)實現(xiàn)級驗證

目前介紹的方法都是從路由協(xié)議的技術(shù)規(guī)范或形式化歸約中抽取模型，驗證的模型是欠近似的(under approximation)，因此更適合在系統(tǒng)早期設(shè)計階段使用。雖然系統(tǒng)中錯誤的發(fā)現(xiàn)越早越好，但總是存在一些在系統(tǒng)多次運行后才會發(fā)現(xiàn)的錯誤，特別是分布式系統(tǒng)中，這些深度的、不可重現(xiàn)的錯誤表現(xiàn)更明顯。由于模型檢驗對狀態(tài)空間的窮舉和錯誤重現(xiàn)能力，所以可用來尋找這些系統(tǒng)實現(xiàn)級錯誤。但如果使用目前介紹的方法，對系統(tǒng)實現(xiàn)級代碼進(jìn)行建模會非常困難，表現(xiàn)在三個方面：首先，建模語言多樣，通常與系統(tǒng)實現(xiàn)代碼不同且抽取模型耗時非常大；其次，抽象描述的模型和實際運行的系統(tǒng)易存在不一致性，錯誤可能被隱藏；最后，高層次的抽象模型不能快速應(yīng)對系統(tǒng)的改變。目前已有一些模型檢驗工具能跳過形式化規(guī)約和模型抽取步驟，直接驗證代碼，例如CMC、MaceMC、Verisoft、Java PathFinder等。

CMC[34]能對C、C++系統(tǒng)代碼進(jìn)行直接驗證，可看作一個具有模型檢驗功能的網(wǎng)絡(luò)模擬器。它能驗證整個網(wǎng)絡(luò)協(xié)議，也能通過抽取系統(tǒng)指定部分進(jìn)行單元測試，性質(zhì)用不變式表示。CMC已經(jīng)驗證了移動自組網(wǎng)路由協(xié)議(AODV)的三個系統(tǒng)實現(xiàn)，驗證的性質(zhì)包括內(nèi)存泄漏、無環(huán)性、路由表項和分組消息的正確性等，最終找到34處不同的錯誤，驗證代碼近六千行。此外，CMC還用來驗證Linux上的TCP/IP實現(xiàn)，使驗證代碼量達(dá)到五萬行[35]。

由于CMC用不變式描述性質(zhì)，故可驗證安全性，但不適合驗證活性。因此文獻(xiàn)[36]提出用模型檢驗驗證系統(tǒng)實現(xiàn)級的活性的方法?；钚詄ventually p成立，表示待驗證系統(tǒng)的任何執(zhí)行序列上，總會存在一個狀態(tài)使斷言p成立；那么該性質(zhì)的違反則表示存在一條執(zhí)行路徑，該路徑上的所有狀態(tài)都使p不成立。由于反例路徑的長度是無限的，因此驗證較麻煩。作者開發(fā)出工具M(jìn)aceMC來驗證安全性和活性，它將狀態(tài)分為live和dead兩類，通過啟發(fā)式地搜索，自動搜索到一個關(guān)鍵轉(zhuǎn)移，并據(jù)此剪掉所有可到達(dá)live狀態(tài)的執(zhí)行路徑，最終那些剩下的dead狀態(tài)路徑就是活性違反的反例。作者使用MaceMC和他們開發(fā)出的一種交互式的調(diào)試程序MDB，驗證了P2P路由協(xié)議PASTRY和Chord，最終找到31處活性錯誤和21處安全性錯誤，且沒有出現(xiàn)誤報的情況。

3 基于定理證明的方法

文獻(xiàn)[37]提出一種基于定理證明的驗證方法，并設(shè)計一種框架工具DNV來驗證路由協(xié)議。它的規(guī)約語言是一種分布式的基于邏輯的遞歸查詢語言NDlog(未來還將加入Type Schema)，不變式性質(zhì)的表示有兩種方法，一是直接用定理表示，二是用NDlog規(guī)則表示。驗證時，NDlog程序和NDlog規(guī)則表示的性質(zhì)由定理生成器(axiom generator)自動轉(zhuǎn)化成定理證明工具(例如PVS)可識別的模型。DNV除了形式化驗證功能，還可直接運行NDlog描述的路由協(xié)議，因此DNV集合了規(guī)約、驗證和實現(xiàn)的功能，不僅能用于協(xié)議設(shè)計階段，還可用于協(xié)議實現(xiàn)級的分析。作者最后用DNV分析了距離向量協(xié)議在動態(tài)網(wǎng)絡(luò)上的計數(shù)到無窮大問題。相比模型檢驗，DNV的驗證不受網(wǎng)絡(luò)大小限制，且不需要復(fù)雜的模型抽取。相比傳統(tǒng)的定理證明，DNV降低了定理證明的使用難度，提高了自動化程度，對網(wǎng)絡(luò)設(shè)計人員來說更實用。

4 其他方法

4.1 模型檢驗和定理證明的結(jié)合

模型檢驗自動化程度高，但存在狀態(tài)爆炸問題，即使使用歸約方法，能驗證的模型規(guī)模也不會太大。此外，協(xié)議的不可判定性使模型檢驗難以證明協(xié)議正確性的成立。

定理證明不受狀態(tài)數(shù)限制，但人工參與度高。如果合理結(jié)合兩者能實現(xiàn)大規(guī)模甚至無界網(wǎng)絡(luò)的正確性成立的驗證。

文獻(xiàn)[38]提出一種驗證距離向量路由協(xié)議標(biāo)準(zhǔn)或草案的方法，用模型檢驗工具SPIN驗證節(jié)點數(shù)少的網(wǎng)絡(luò)或初始模型，并用定理證明工具HOL將網(wǎng)絡(luò)規(guī)模擴(kuò)展到任意大小。作者證明了RIP的正確性和實時收斂的穩(wěn)定性，并分析了當(dāng)時的新移動自組網(wǎng)路由協(xié)議AODV草案，驗證了無環(huán)性，并提出修改意見應(yīng)對草案中的歧義描述。該方法不受網(wǎng)絡(luò)模型的規(guī)模約束，能應(yīng)用在無限大小的網(wǎng)絡(luò)上，但是定理證明的使用需要大量人工指導(dǎo)，提出定理和引理來描述協(xié)議性質(zhì)具有難度，針對距離向量協(xié)議的方法不能很好地應(yīng)用到其他類型的協(xié)議上。

4.2 參數(shù)化系統(tǒng)驗證

參數(shù)化系統(tǒng)[39]是指包含特定有限狀態(tài)進(jìn)程的多個實例的并發(fā)系統(tǒng)。參數(shù)表示進(jìn)程實例的個數(shù)，該參數(shù)確定系統(tǒng)的規(guī)模。移動自組網(wǎng)的節(jié)點動態(tài)變化導(dǎo)致網(wǎng)絡(luò)拓?fù)涞牟还潭ǎ?jié)點功能相同，因此可看作一個參數(shù)化系統(tǒng)驗證[40-42]。

文獻(xiàn)[43]提出一種基于圖轉(zhuǎn)換系統(tǒng)(Graph Transformation System，GTS)的建模和自動驗證網(wǎng)絡(luò)協(xié)議框架，并驗證了自組網(wǎng)路由協(xié)議DYMO的無環(huán)性。該框架用圖模式符號化表示協(xié)議的全局配置集合和安全性(一個不良全局配置集合)，通過對初始配置到不良全局配置的反向可達(dá)性分析，自動驗證協(xié)議的安全性。反向可達(dá)性分析技術(shù)已成功應(yīng)用于參數(shù)化的無限狀態(tài)系統(tǒng)和不可判定問題的驗證，作者結(jié)合GTS和反向可達(dá)性分析，使該方法適合那些節(jié)點數(shù)無限、以結(jié)構(gòu)和拓?fù)錇橹行牡木W(wǎng)絡(luò)協(xié)議驗證，例如自組網(wǎng)路由協(xié)議的驗證。但是該方法在前期計算的優(yōu)化、可達(dá)性分析的終止和因過近似(over approximation)產(chǎn)生的偽反例的處理上仍有不足。此外，它無法驗證活性。

4.3 輕量級建模分析

有學(xué)者認(rèn)為形式化方法過于強(qiáng)調(diào)規(guī)約和設(shè)計的形式化，語言的表達(dá)能力和系統(tǒng)建模的復(fù)雜程度讓形式化過程異常困難[44]。輕量級形式化方法關(guān)注應(yīng)用和部分規(guī)約，且自動化程度高，是使形式化方法變得簡單易用的一種途徑。Alloy分析器[45]是一種支持輕量級模型分析的工具，與模型檢驗工具相比，它們都具有高度自動化的優(yōu)點和狀態(tài)爆炸的缺點。不同的是，在建模語言表達(dá)能力和驗證能力方面各有利弊。Alloy能生成不變式的實例、模擬操作的執(zhí)行(即使是隱式定義的操作)并檢查一個模型的用戶指定屬性，最終生成易于閱讀的圖形化反例。

文獻(xiàn)[46]使用Alloy分析器研究P2P協(xié)議Chord的節(jié)點加入和退出機(jī)制的正確性，為降低模型復(fù)雜度，作者抽象掉了Chord查找定位資源的功能描述，最終找到多處反例，這些反例質(zhì)疑了Chord的正確性。抽取Alloy模型的過程類似模型檢驗，而驗證時的執(zhí)行路徑都很短，因此反例像有界模型檢驗?zāi)菢右子陂喿x，但只能用不變式描述性質(zhì)，和時序邏輯相比表達(dá)能力各有側(cè)重。

5 結(jié)束語

自動形式化驗證路由協(xié)議是有價值的研究領(lǐng)域，不僅能尋找新開發(fā)的路由協(xié)議的設(shè)計缺陷，還能提高協(xié)議實現(xiàn)的質(zhì)量。文中總結(jié)了近年來自動形式化驗證路由協(xié)議的方法和應(yīng)用，它們的主要技術(shù)基礎(chǔ)包括模型檢驗和定理證明。模型檢驗自動化程度高、易用性強(qiáng)，但狀態(tài)爆炸問題限制了驗證規(guī)模；定理證明邏輯表達(dá)能力強(qiáng)、能驗證無限狀態(tài)的系統(tǒng)，但是人工參與度高、使用難度大。筆者認(rèn)為，未來的形式化驗證路由協(xié)議的研究方向包括：

(1)增加可驗證的模型規(guī)模，例如驗證移動自組網(wǎng)路由協(xié)議在多節(jié)點、動態(tài)拓?fù)涞拇笠?guī)模網(wǎng)絡(luò)上的正確性；

(2)不僅使用形式化驗證技術(shù)實現(xiàn)早期設(shè)計階段的驗證，還應(yīng)用在系統(tǒng)實現(xiàn)級驗證。例如第2節(jié)用模型檢驗實現(xiàn)了路由協(xié)議實現(xiàn)代碼的驗證；

(3)綜合不同分析方法的特點，取長補短，提高驗證效率；

(4)追求形式化方法支撐工具的通用和完善是不現(xiàn)實的，因此應(yīng)開發(fā)有特色的路由協(xié)議驗證工具。第3節(jié)中基于自動定理證明技術(shù)的框架工具DNV就是較好的例子。

[1] Abolhasan M,Wysocki T,Dutkiewicz E.A review of routing protocols for mobile ad hoc networks[J].Ad Hoc Networks,2004,2(1):1-22.

[2] Barbir A,Murphy S,Yang Y.Generic threats to routing protocols[J].Annals of Gastroenterology Quarterly Publication of the Hellenic Society of Gastroenterology,2004,27(4):429.

[3] Clarke E M,Wing J M.Formal methods:state of the art and future directions[J].ACM Computing Surveys,1996,28(4):626-643.

[4] Woodcock J,Larsen P G,Bicarregui J,et al.Formal methods:practice and experience[J].ACM Computing Surveys,2009,41(4):19-59.

[5] Chen Z,Gu Y,Huang Z,et al.Model checking aircraft controller software:a case study[J].Software:Practice and Experience,2015,45(7):989-1017.

[6] Holzmann G J.Mars code[J].Communications of the ACM,2014,57(2):64-73.

[7] Huth M, Ryan M. Logic in computer science:modelling and reasoning about systems[M].Cambridge：Cambridge University Press,2004.

[8] D'silva V,Kroening D,Weissenbacher G.A survey of automated techniques for formal software verification[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2008,27(7):1165-1178.

[9] Gordon M J C,Melham T F.Introduction to HOL:a theorem proving environment for higher order logic[M].Cambridge：Cambridge University Press,1993.

[10] Owre S,Rushby J M,Shankar N.PVS:a prototype verification system[M]//Automated Deduction-CADE-11.Berlin:Springer,1992:748-752.

[12] Oleshchuk V A.Modeling,specification and verification of ad-hoc sensor networks using SPIN[J].Computer Standards & Interfaces,2005,28(2):159-165.

[13] Wibling O,Parrow J,Pears A.Ad hoc routing protocol verification through broadcast abstraction[M]//Formal techniques for networked and distributed systems.Berlin:Springer,2005:128-142.

[15] Chiyangwa S, Kwiatkowska M.A timing analysis of AODV[M]//Formal methods for open object-based distributed systems.Berlin:Springer,2005:306-321.

[16] Benetti D,Merro M,Vigano L.Model checking ad hoc network routing protocols:aran vs.endaira[C]//8th IEEE international conference on software engineering and formal methods.[s.l.]:IEEE,2010:191-202.

[17] Holzmann G J.The SPIN model checker:primer and reference manual[M].Reading:Addison-Wesley,2004.

[18] Fehnker A,van Glabbeek R,H?fner P,et al.Automated analysis of AODV using UPPAAL[M]//Tools and algorithms for the construction and analysis of systems.Berlin:Springer,2012:173-187.

[19] Chen Z,Zhang D,Ma Y.Modeling and analyzing the convergence property of the BGP routing protocol in SPIN[J].Telecommunication Systems,2015,58(3):205-217.

[20] Yin P,Ma Y,Chen Z.Model checking the convergence property of BGP networks[J].Journal of Software,2014,9(6):1619-1625.

[21] Griffin T G,Sobrinho J L.Metarouting[J].ACM SIGCOMM Computer Communication Review,2005,35(4):1-12.

[22] Behrmann G, David A, Larsen K G.A tutorial on uppaal[M]//Formal methods for the design of real-time systems.Berlin:Springer,2004:200-236.

[23] de Renesse R, Aghvami A H.Formal verification of ad-hoc routing protocols using SPIN model checker[C]//Electrotechnical conference.[s.l.]:[s.n.],2004:1177-1182.

[24] Wang A,Talcott C,Gurney A J T,et al.Reduction-based formal analysis of BGP instances[M]//Tools and algorithms for the construction and analysis of systems.Berlin:Springer,2012:283-298.

[25] Griffin T G,Shepherd F B,Wilfong G.The stable paths problem and interdomain routing[J].IEEE/ACM Transactions on Networking,2002,10(2):232-243.

[26] Clavel M,Durán F,Eker S,et al.All about maude-a high-performance logical framework:how to specify,program and verify systems in rewriting logic[C]//LNCS.[s.l.]:[s.n.],2007.

[27] Wang A,Talcott C,Jia L,et al.Analyzing bgp instances in maude[M]//Formal techniques for distributed systems.Berlin:Springer,2011:334-348.

[28] Wang A,Gurney A J T,Han X,et al.A reduction-based approach towards scaling up formal analysis of internet configurations[C]//INFOCOM.[s.l.]:IEEE,2014:637-645.

[29] Sosnovich A,Grumberg O,Nakibly G.Finding security vulnerabilities in a network protocol using parameterized systems[C]//Computer aided verification.[s.l.]:[s.n.],2013:724-739.

[30] Biere A,Cimatti A,Clarke E,et al.Symbolic model checking without BDDs[M].Berlin:Springer,1999.

[31] Kroening D,Strichman O.Efficient computation of recurrence diameters[C]//Verification,model checking, and abstract interpretation.[s.l.]:[s.n.],2003:298-309.

[32] Amla N,Kurshan R,McMillan K L,et al.Experimental analysis of different techniques for bounded model checking[M]//Tools and algorithms for the construction and analysis of systems.Berlin:Springer,2003:34-48.

[33] Kroening D,Tautschnig M.CBMC-C bounded model checker[M]//Tools and algorithms for the construction and analysis of systems.Berlin:Springer,2014:389-391.

[34] Musuvathi M,Park D Y W,Chou A,et al.CMC:a pragmatic approach to model checking real code[J].ACM SIGOPS Operating Systems Review,2002,36(SI):75-88.

[35] Musuvathi M.Model checking large network protocol implementations[C]//Conference on symposium on networked systems design and implementation.Berkeley:USENIX Association,2004:12.

[36] Killian C,Anderson J W,Jhala R,et al.Life,death,and the critical transition:finding liveness bugs in systems code[C]//Proceedings of the 4th USENIX conference on networked systems design & implementation.Berkeley:USENIX Association,2007:18.

[37] Wang A,Basu P,Loo B T,et al.Declarative network verification[M]//Practical aspects of declarative languages.Berlin:Springer,2009:61-75.

[38] Bhargavan K,Obradovic D,Gunter C A.Formal verification of standards for distance vector routing protocols[J].Journal of the ACM,2002,49(4):538-576.

[39] Zuck L,Pnueli A.Model checking and abstraction to the aid of parameterized systems (a survey)[J].Computer Languages, Systems & Structures,2004,30(3):139-169.

[40] Delzanno G,Sangnier A,Zavattaro G.Parameterized verification of ad hoc networks[C]//International conference on concurrency theory.[s.l.]:[s.n.],2010:313-327.

[41] Delzanno G,Sangnier A,Zavattaro G.On the power of cliques in the parameterized verification of ad hoc networks[M]//Foundations of software science and computational structures.Berlin:Springer,2011:441-455.

[42] Abdulla P A,Atig M F,Rezine O.Verification of directed acyclic ad hoc networks[M]//Formal techniques for distributed systems.Berlin:Springer,2013:193-208.

[43] Saksena M,Wibling O,Jonsson B.Graph grammar modeling and verification of ad hoc routing protocols[M]//Tools and algorithms for the construction and analysis of systems.Berlin:Springer,2008:18-32.

[44] Jackson D.Lightweight formal methods[M]//Formal methods for increasing software productivity.Berlin:Springer,2001.

[45] Jackson D.Software abstractions:logic,language,and analysis[M].[s.l.]:MIT Press,2012.

[46] Zave P.Using lightweight modeling to understand chord[J].ACM SIGCOMM Computer Communication Review,2012,42(2):49-57.

ResearchonAutomatedFormalVerificationofRoutingProtocols

HUANG Wu-dan，YAN Jun-qi

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Routing protocols are widely deployed in the Internet for exchanging routing information and selecting routes.Having a correct and secure routing protocol is a fundamental problem to computer networks.Recently,formal verification has been successfully applied to ensure quality of routing protocols in design and implementation.And it can effectively find system defects in software testing to enhance the security of systems.The several main techniques in automated formal verification like model checking,theorem proving and equivalence verification are introduced primarily.Then the important methods on automated formal verification for routing protocols and their advantages and disadvantages,as well as their research progress and utilization are summarized,which provides a reference for researchers in related fields to verify routing protocols with formal methods.Finally,the research status of this field is summarized and the future research hotspots are forecasted.Some feasible research directions are also put forward.

routing protocol;formal verification;model checking;theorem proving

TP301

A

1673-629X(2017)12-0001-06

10.3969/j.issn.1673-629X.2017.12.001

2016-11-16

2017-03-22 < class="emphasis_bold">網(wǎng)絡(luò)出版時間

時間：2017-08-01

國家自然科學(xué)基金資助項目(61100034)；國家自然科學(xué)基金委員會-中國民航局民航聯(lián)合研究基金(U1533130)；教育部留學(xué)回國人員科研啟動基金(2013)；中央高?；究蒲袠I(yè)務(wù)費專項資金(NS2016092)

黃吳丹(1991-),男,碩士,研究方向為模型檢驗、軟件驗證。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170801.1551.038.html