路由协议的自动形式化验证方法研究

黄吴丹，严俊琦

(南京航空航天大学 计算机科学与技术学院,江苏 南京 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