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

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

路由協(xié)議的自動(dòng)形式化驗(yàn)證方法研究

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

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

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

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

0 引 言

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

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

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

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

1 形式化驗(yàn)證技術(shù)分類(lèi)

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

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

1.1 模型檢驗(yàn)

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

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

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

1.2 定理證明

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

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

1.3 等價(jià)性檢驗(yàn)

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

2 基于模型檢驗(yàn)的方法

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

(3)菲尼爾濾光片因?yàn)樾阅芤蟮牟煌哂胁煌慕咕?，即是我們平時(shí)所說(shuō)的感應(yīng)距離。因此，它會(huì)產(chǎn)生不同的監(jiān)控視場(chǎng)。視場(chǎng)越多，控制越嚴(yán)密。

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

(1)模型抽取。

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

(2)建模。

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

bool TTL;

::ture->TTL=1;

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

fi

(3)驗(yàn)證。

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

2.1 工具的選擇

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

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

2.2 歸 約

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

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

2.3 有界模型檢驗(yàn)

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

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

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

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

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

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

3 基于定理證明的方法

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

4 其他方法

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

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

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

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

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

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

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

4.3 輕量級(jí)建模分析

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

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

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

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

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

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

(3)綜合不同分析方法的特點(diǎn)，取長(zhǎng)補(bǔ)短，提高驗(yàn)證效率；

(4)追求形式化方法支撐工具的通用和完善是不現(xiàn)實(shí)的，因此應(yīng)開(kāi)發(fā)有特色的路由協(xié)議驗(yàn)證工具。第3節(jié)中基于自動(dòng)定理證明技術(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ò)出版時(shí)間

時(shí)間：2017-08-01

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

黃吳丹(1991-),男,碩士,研究方向?yàn)槟Ｐ蜋z驗(yàn)、軟件驗(yàn)證。

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