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

黃吳丹，嚴俊琦

(南京航空航天大學 計算機科學與技術學院,江蘇 南京 210016)

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

黃吳丹，嚴俊琦

(南京航空航天大學 計算機科學與技術學院,江蘇 南京 210016)

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

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

0 引 言

路由協議通過路徑選擇實現信息交換功能，提高計算機網絡的數據傳輸效率。路由協議不僅在因特網核心部分的路由器上運行，還在移動自組網(MANET)、面向應用層的覆蓋網(例如P2P網絡)這些新型網絡上擔任重要角色。特別是在移動自組網中，所有節點都支持路由發現和維護，節點的動態變化導致網絡拓撲不固定，移動自組網本身的應用領域都要求設計新的有特色的路由協議。

因特網上的路由選擇主要分為兩類：距離向量協議和鏈路狀態協議。移動自組網上的路由協議分為被動式、主動式和混合式三類[1]。被動式通常由表驅動，可根據路由表預先獲取路由；主動式在需要時才進行路由發現；混合式結合被動式和主動式的特點靈活選擇路由。P2P網絡因其無中心、動態性和基于應用層的特點，路由算法的優劣應考慮效率、易用性、可擴展性等方面。

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

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

1 形式化驗證技術分類

形式化方法是基于數學的語言、技術和工具，用來幫助開發軟硬件系統[3]。形式化驗證是形式化方法的一個研究內容，根據系統的形式化規約或屬性來證明系統的正確性，在計算機硬件、控制系統、通信協議、安全關鍵軟件等領域有大量應用[4-6]。相對于傳統的模擬、仿真和測試，形式化驗證是一種窮盡式的數學技術，因此不需要花費過多時間關注輸入條件或測試用例，保證了測試的覆蓋率。

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

1.1 模型檢驗

模型檢驗(model checking)建立系統的有限狀態模型，在驗證時窮舉搜索狀態空間，檢查模型是否滿足性質。性質包括安全性(safety)和活性(liveness)。安全性描述“壞的事情永遠(always)不會發生”，例如斷言始終為真、空指針不能被引用、緩沖區禁止溢出。活性描述“好的事情終(eventually)將發生”，例如程序最終總會終止運行、請求的服務總能被響應。性質的表示方法多種多樣，可由時序邏輯表示，例如線性時序邏輯(LTL)和計算樹邏輯(CTL)[7]，也可通過斷言等方式表達的不變式表示。如果性質不滿足，將提供反例執行路徑。

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

模型檢驗是形式化驗證的研究熱點，原理簡單且較為實用。目前已有大量模型檢驗工具[8]提供高度自動化的驗證，并自動生成反例。但是網絡的分布特性使狀態爆炸問題更突出，這也是使用模型檢驗驗證路由協議時應關注的一個主要問題。

1.2 定理證明

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

定理證明具有高度抽象、邏輯表達能力強的特點，能驗證具有無限狀態的系統。但是它的抽象較困難、人工參與度高，使用者應具有相關的邏輯知識和經驗，因此實用定理證明的研究進度會很慢。

1.3 等價性檢驗

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

2 基于模型檢驗的方法

目前大部分研究都是從路由協議的標準文檔或形式化規約中抽取出模型，用模型檢驗工具驗證該模型是否滿足性質。為減小狀態空間，模型應該越小越好，但也應該保持模型的表達能力。因此建模要在緩解狀態爆炸問題和保持模型表達能力間進行權衡。

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

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

(1)模型抽取。

應充分獲取協議信息，簡化和假設協議的行為和參數，明確節點可發送和接收的消息格式，建立協議的偽代碼或有限狀態機的描述。通常包括對節點、通信鏈路、低層服務、配置和策略、網絡拓撲的簡化和假設[12-14]。例如，研究BGP的路由策略時，假設協議機制是可靠的。研究自組網協議時，將網絡拓撲抽象成具有三類節點的網絡，即源節點、目的節點和中間節點集合[15-16]。此外，還可根據驗證的性質，假設其他部分是可靠運行的。例如，在研究AODV時間方面的正確性時，可構造一個具有靜態、線性拓撲的AODV時間相關的UPPAAL模型。

(2)建模。

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

bool TTL;

::ture->TTL=1;

::true->TTL=0; //表示TTL結束

fi

(3)驗證。

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

2.1 工具的選擇

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

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

2.2 歸 約

歸約方法(reduction-based)通過合并或刪除網絡節點來減小模型規模。文獻[24]對一個BGP組合模型SPP[25]進行擴展并實行歸約，最后驗證了BGP的路由振蕩特性。該方法可應用在含有iBGP或eBGP的網絡上，實驗使用基于Maude[26]開發的工具包，使歸約過程實現自動化，最后通過模型檢驗實現驗證。實驗數據表明，驗證效率大大提高，相比文獻[27]，驗證節點數目從25增加到100以上。在此方法的基礎上，文獻[28]提出一個BGP形式化模型EPD和兩條歸約規則：重復歸約和互補歸約，并證明了該方法的可靠性和局部完備性。可靠性表明如果歸約后模型G'是安全的，那么相應歸約前的模型G也是安全的；如果G'存在路由振蕩，那么G中至少存在一條執行路徑能產生路由振蕩。局部完備性表明，只要知道節點的局部拓撲信息，就可進行有效歸約。

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

2.3 有界模型檢驗

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

目前使用有界模型檢驗驗證路由協議的研究不多，只有Adi Sosnovich等使用有界模型檢驗工具CBMC[33]驗證了OSPF協議的安全性，并找到未發表過的攻擊。實驗結果表明，有界模型檢驗適合驗證期望找到反例的模型，但是如果用來證明正確性成立(例如希望協議具有無環特征)，那么建模或尋找完備性閾值的難度較大。

2.4 系統實現級驗證

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

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

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

3 基于定理證明的方法

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

4 其他方法

4.1 模型檢驗和定理證明的結合

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

定理證明不受狀態數限制，但人工參與度高。如果合理結合兩者能實現大規模甚至無界網絡的正確性成立的驗證。

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

4.2 參數化系統驗證

參數化系統[39]是指包含特定有限狀態進程的多個實例的并發系統。參數表示進程實例的個數，該參數確定系統的規模。移動自組網的節點動態變化導致網絡拓撲的不固定，但節點功能相同，因此可看作一個參數化系統驗證[40-42]。

文獻[43]提出一種基于圖轉換系統(Graph Transformation System，GTS)的建模和自動驗證網絡協議框架，并驗證了自組網路由協議DYMO的無環性。該框架用圖模式符號化表示協議的全局配置集合和安全性(一個不良全局配置集合)，通過對初始配置到不良全局配置的反向可達性分析，自動驗證協議的安全性。反向可達性分析技術已成功應用于參數化的無限狀態系統和不可判定問題的驗證，作者結合GTS和反向可達性分析，使該方法適合那些節點數無限、以結構和拓撲為中心的網絡協議驗證，例如自組網路由協議的驗證。但是該方法在前期計算的優化、可達性分析的終止和因過近似(over approximation)產生的偽反例的處理上仍有不足。此外，它無法驗證活性。

4.3 輕量級建模分析

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

文獻[46]使用Alloy分析器研究P2P協議Chord的節點加入和退出機制的正確性，為降低模型復雜度，作者抽象掉了Chord查找定位資源的功能描述，最終找到多處反例，這些反例質疑了Chord的正確性。抽取Alloy模型的過程類似模型檢驗，而驗證時的執行路徑都很短，因此反例像有界模型檢驗那樣易于閱讀，但只能用不變式描述性質，和時序邏輯相比表達能力各有側重。

5 結束語

自動形式化驗證路由協議是有價值的研究領域，不僅能尋找新開發的路由協議的設計缺陷，還能提高協議實現的質量。文中總結了近年來自動形式化驗證路由協議的方法和應用，它們的主要技術基礎包括模型檢驗和定理證明。模型檢驗自動化程度高、易用性強，但狀態爆炸問題限制了驗證規模；定理證明邏輯表達能力強、能驗證無限狀態的系統，但是人工參與度高、使用難度大。筆者認為，未來的形式化驗證路由協議的研究方向包括：

(1)增加可驗證的模型規模，例如驗證移動自組網路由協議在多節點、動態拓撲的大規模網絡上的正確性；

(2)不僅使用形式化驗證技術實現早期設計階段的驗證，還應用在系統實現級驗證。例如第2節用模型檢驗實現了路由協議實現代碼的驗證；

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

(4)追求形式化方法支撐工具的通用和完善是不現實的，因此應開發有特色的路由協議驗證工具。第3節中基于自動定理證明技術的框架工具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">網絡出版時間

時間：2017-08-01

國家自然科學基金資助項目(61100034)；國家自然科學基金委員會-中國民航局民航聯合研究基金(U1533130)；教育部留學回國人員科研啟動基金(2013)；中央高校基本科研業務費專項資金(NS2016092)

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

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