技术与标准丨基于输入输出分离标识转换系统的路由协议健壮性分析模型
作者简介
周开波
中国信息通信研究院泰尔系统实验室主任，主要从事通信网和互联网技术、标准和测试研究工作，重点研究领域为网络安全及数据安全，在网络设备安全研究方面具有多年研究经验。张治兵
中国信息通信研究院泰尔系统实验室副总工程师，高级工程师，主要从事信息通信网络安全、工控安全等研究工作，重点研究领域为网络安全检测认证制度和标准、网络关键设备安全、供应链安全、5G安全等。王小雨
中国信息通信研究院泰尔系统实验室网络技术部副主任，高级工程师，主要从事SDN/NFV、5G核心网、数据通信等信息网络领域新技术研究工作，重点研究领域为5G移动通信、云网融合、网络切片、SRv6等。刘欣东
中国信息通信研究院泰尔系统实验室工程师，主要从事信息通信安全领域研究和试验验证工作，重点研究领域为ICT产业新领域技术、安全业务新技术研究等。论文引用格式：
周开波, 张治兵, 王小雨, 等. 基于输入输出分离标识转换系统的路由协议健壮性分析模型[J]. 信息通信技术与政策, 2022,48(4):49-56.
基于输入输出分离标识转换系统的路由协议健壮性分析模型
周开波 张治兵 王小雨 刘欣东
（中国信息通信研究院泰尔系统实验室，北京 100191）
摘要：作为网络关键设备的路由器和交换机，其运行的路由协议的健壮性是设备健壮性的关键因素，如何对路由协议的健壮性进行分析评价是网络关键设备安全性评价的重点。在本文中，基于输入输出分离的标识转换系统（IOLTS），提出了网络设备中路由协议的健壮性的分析方法模型，并以OSPFv2协议为例进行了分析验证。
关键词：网络关键设备；路由协议；OSPF；标识转换；健壮性
中图分类号：TN925；TP393.08 文献标志码：A
引用格式：周开波, 张治兵, 王小雨, 等. 基于输入输出分离标识转换系统的路由协议健壮性分析模型[J]. 信息通信技术与政策, 2022,48(4):49-56.
DOI：10.12267/j.issn.2096-5931.2022.04.009
0 引言
强制性国家标准GB 40050-2021《网络关键设备安全通用要求》于2021年2月20日发布，并于2021年8月1日正式实施。GB 40050-2021的安全功能要求部分第5.8节提出，通信协议应满足协议健壮性要求，防范异常报文攻击。GB 40050-2021的安全保障要求部分第6.1节提出，网络关键设备的提供者在设计和开发阶段应采用健壮性测试等方式对设备进行安全性测试。
对用于跨网段互联的网络设备而言，为方便路由的通告，通常要求支持至少一种以上的路由转发协议。路由转发协议根据工作的机制，分为链路状态协议和距离矢量协议，常见路由转发协议包括RIP[1]、OSPF[2]和BGP[3]。其中，RIP属于域内距离矢量协议、OSPF属于域内链路状态协议、BGP属于域间距离矢量协议。针对路由协议的攻击是现实存在的并且多次出现过。2011年和2013年在美国举办的黑帽大会上，来自以色列的电子战争研究与仿真中心（National EW Research and Simulation Center）研究员GaBI Nakibly曝光了OSPF路由器协议存在的一个漏洞。攻击者利用该漏洞可以欺骗正常的OSPF路由器，使之接受伪造的路由表更新，并最终控制整个网络中所有路由器的路由表，通过伪造网络路由，攻击者可以改变网络流量的流向，实现对数据流的监听，或者造成路由环路,形成拒绝服务攻击。2002年，FX在柏林举办的Chaos Communication Congress 2002大会上展示了针对Cisco路由器OSPF的攻击概念验证代码，攻击成功后可以将配置文件写入到路由器的非易失随机存储器（Non-Volatile RAMs，NVRAM）中。对于BGP路由转发协议，最具代表性的攻击手段就是通过修改自身或者转发的正确路由信息，引发自制系统被错误路由误导的域间路由劫持[4-6]。
本文第2部分对LTS系统、IOLTS系统模型进行了介绍；第3部分结合路由协议的特点，提出了路由协议的通用健壮性分析模型；第4部分以网络设备中部署量最大的OSPF路由协议为例进行了健壮性的分析，给出了生成健壮性测试路径的方法；第5部分给出了总结。
1 标识转换系统
1.1 LTS
标识转换系统（Labeled Transition System，LTS）[7-8]通常用<S,L,T,S0>四元组的方式来表示。其中，S为状态的集合；S0为初始状态，S0∈S；L为可观察到的动作标识的集合，不可观察的动作的记为τ,τ∉L,L∩{τ}=Ø；T为转移关系，在LTS系统中，转移关系是一个重要的概念，用于表示一系列可观察的动作之后转换的集合，T⊆S×(L∪{τ})×S。对于动作μ,μ∈L∪{τ}，动作发生后，系统从状态s转移到状态s′，用(s,μ,s′)表示，通常也记为sμ→s′,(s,μ,s′)∈T。在动作集合L之上，所有转移关系的集合记为L∗。空的转移关系记为ε。如果σ1,σ2∈L∗,σ1·σ2表示在σ1和σ2的联合，即σ1之后继续进行σ2转移。对于转移关系T，还有以下的推论。
LTS模型描述的系统示例如图1所示。其中，S={S1,S2,S3,S4,S5},L={L1,L2,L3,L4}, trace(S2)={S2L3→S4,S2L4→S5}。
1.2 IOLTS输入输出分离的标识转换系统（Input/ Output LTS，IOLTS）相对于LTS的主要改进是将动作标识的集合分为输入和输出两个部分，以便于更好地分析基于状态和输入而进行状态转换的协议。其中，L1表示输入动作标识集合，L0表示输出动作标识集合，L=LI∪L0，LI∩L0=Ø。
IOLTS模型描述的系统示例如图2所示。其中，S={S1,S2,S3,S4,S5},LI={?L1,?L2,?L4},L0={!L3,!L5}, trace（S2)={S2!L3→S4,S2?L4→S5}。
2 路由协议健壮性分析模型
健壮性指的是网络关键设备或部件在无效数据输入或者在高强度输入等环境下，各项功能可保持正确运行的程度。健壮性测试中，特别关注的是无效的输入对整个系统稳定运行的危害。一个健壮性良好的系统即使收到无效的输入或处在不适当的使用环境中也能运行，不出现宕机等情况[9-10]。一个运行路由协议的网络可以简化并抽象为具有多种状态的两个节点通过报文交互所组成的系统（见图 3）。
其中，S1和S2代表两个运行路由协议的节点。为体现在两个节点之间的报文交互过程，引入了一个虚拟的中间层（Medium层），在中间层用双层圈代表对应节点中发送报文的状态，其中用于交互的报文组合分别是{!a, ?a}、{!b, ?b}和{!m, ?m}。“!”表示这是一个输出报文的动作，“?”表示这是一个收到报文的动作。在图3中，仅考虑路由协议正常交互的过程，但为分析协议的健壮性，还需要考虑路由协议在各个状态下收到各种类型报文的情况。对于某一个协议状态，对应的输入可以分为以下3类。
（1）符合协议定义的报文且出现在合适的状态，称为有效的报文，其集合记为PEP。
（2）符合协议定义的报文但出现在不合适的状态，称为不合适的报文，其集合记为POP；所有符合协议定义的报文集合记为PP，PP=PEP∪POP。
（3）与协议中定义不符合的报文，称为无效的报文，其集合记为PP。
综合有效、不合适和无效输入之后的协议模型见图4。在图4中IPP模块用于处理无效报文，其中，A表示收到的无效报文的集合，!e为处理之后的输出，处理完无效报文之后协议返回到原来的状态。此外，针对每一个状态，?Ni表示在该状态下收到的不合适报文的集合。健壮性分析模型建立之后，就需要找出所有可能的转移关系，其集合L∗=PS×(PP∪PP)×PS，并根据列出的转移关系生成测试例。其中，PS=[S1-1,S1-2,S1-3,S1-4,S1-5,S2-1,S2-2,S2-3,S2-4,S2-5,IPP]。
需要注意的是，在分析模型的建立中，需要考虑到协议中没有明确定义的状态，但此类状态对于明确模型又非常重要。此时，可以自主地在模型中增加此类状态。因此，模型中的状态总数应该≥协议中规定的状态数量。PP=[?x,?y,?z,?a,?b,?m,!a,!b,!m,?A,!e,?N1,?N2,?N3,?N4,?N5]。转移关系的生成步骤如下。
（1）明确初始状态。在本协议健壮性分析模型中，初始状态为S1-1，S2-1。（2）确定终结状态的集合。终结状态指的是通过一次转换就到达初始状态的状态。在图4中，对于状态S1-1，其终结状态的集合记为S1-1End,S1-1End={S1-4,S1-5}。（3）从每一个终结状态开始，查找回溯到初始状态的路径。（4）在回溯的路径中，如果出现了交互报文组合中的输入动作，则在回溯的路径中添加对应的输出动作，开始递归回溯。（5）输出所有的转移关系。例如，在图4中，其中一条转移关系就是[S1-5,?m,S1-2,?x,S1-1,S2-2,?a,S2-1]。
之后，根据转移关系编写测试例，指的是在转移关系Si的情况下，生成测试例Ti，其对应的系统响应为Result。对网络路由协议的具体实现而言，如果满足:∀{Si∈L∗}|:Result=Pass，则认为该协议实现满足健壮性的要求。
3 OSPFv2协议健壮性分析
OSPF是互联网上最为常见的链路状态路由协议，使用在自治域内部。OSPF路由协议通过收集路由域内各路由器的链路状态，形成网络的拓扑，再根据网络拓扑，利用最短路径算法得出该路由器至其他网络（主机）的路由表。适用于IPv4的OSPF v2版本于1998年发布，编号为RFC 2328[3]。OSPF将数据直接封装在IP包中，所使用的IP协议号是89。由于IP协议不能保证协议报文的可靠传送，OSPF自身实现了消息检错纠错功能和报文的重传机制。OSPFv2采用鉴权机制来保证安全，只允许可信任的OSPF路由器加入路由域。
3.1 正常协议交互流程路由器RT1和RT2 OSPF协议交互的流程见图5。初始阶段，两个路由器的OSPF协议均处于Down状态。RT1在发出Hello报文后，收到了RT2的Hello报文，并在RT2发来的Hello报文中看到RT1已经列入到邻居列表，表示双方已经建立起双向会话。之后，RT1和RT2通过交互数据库描述（Database Description，DD）报文协商以谁为主进行下一步的数据库信息交互。数据库信息交互完成后，RT1和RT2分别向对方请求链路状态（Link State，LS）信息，实现双方链路状态数据库信息的同步。链路状态数据库同步之后，RT1和RT2进入Full状态，表示双方的OSPF邻接关系建立，并基于各自的链路状态数据库计算路由表。
3.2 健壮性分析根据RFC2328的定义和图5所示的协议交互流程，再考虑到系统在各状态可能收到的报文情况，得到OSPFv2协议的IOLTS模型，如图 6所示。为便于展示OSPF的IOLTS模型，无效报文处理模块IPP分为4个逻辑模块。为便于更好地分析OSPF路由协议的转移状态，在图6中引入了协议中没有的状态，用比正常状态更小的、加粗的、断续圆圈表示。
OSPFv2模型中的各动作说明见表1。Medium层展示RT1和RT2之间有消息交互的状态和交互的消息内容，其中RT1在状态S1、S2、S4、S5、S6与RT2有消息交互，RT2在状态S2、S8、S9、S10、S21与RT2有消息交互。交互的动作组合为：
接下来以S7-Full为例进行回溯，查找回溯到初始状态S1-Down的路径，即S1-Down到S7-Full的转移关系。首先，在RT1中查找其中一条转移关系为：{RT1{S7-Full,!E11,S18-D7,?E9-y+011-R2,S9-ExchangeD,!E9-y010-R1,S5-Exchange,?E2,S1-Down}。
到达初始状态之后，检查现在的转移关系是否存在消息交互的工作组合，发现有E9-y+011-R2>动作组合存在。在RT2中继续查找至初始状态的转移关系，新的转移为：{RT1{S7-Full,!E11,S18-D7,?E9-y+011-R2,S9-ExchangeD,!E9-y010-R1,S5-Exchange,?E2,S1-Down}RT2{S9-ExchangeD,Tau,S22-D9,?E9-y010-R1,S5-Exchange,?E2,S1-Down}}。
再次检查新增的转移关系中是否存在消息交互的工作组合，发现有 动作组合存在。在RT1中继续查找至初始状态的转移关系，新的转移为：{RT1{S7-Full,!E11,S18-D7,?E9-y+011-R2,S9-ExchangeD,!E9-y010-R1,S5-Exchange,?E2,S1-Down}RT2{S9-ExchangeD,Tau,S22-D9,?E9-y010-R1,S5-Exchange,?E2,S1-Down}RT1{S5-Exchange,?E2,S1-Down}}。在新增的转移关系中没有发现动作组合的存在。至此，一条完整的转移关系查找完成。
考虑到最后生成的转移关系跨越了系统中的两个节点，为方便测试例的编写，可以将每一个节点相关的转移关系生成一个测试例。在上述的转移关系中，RT1和RT2相关的转移关系可以生成3个测试例，其中与RT1相关的测试例为2个，与RT2相关的测试例为1个。
4 结束语
路由协议的健壮性可以通过上述方法生成的测试例来进行验证。但在实际的验证过程中，按照上述的分析模型会生成巨量的测试例，执行全部的测试例需要较长的时间。而且根据不同的转移关系生成的测试例可能有重复，如何消除重复的测试例、优化同类无效报文测试例集、提高测试例生成的效率等是下一步需要研究的重点。
参考文献
[1] MALKIN G. RIP version 2[J], 1998.[2] MOY J. OSPF version 2[J]. Request for Comments,1994,28(4):1.[3] HARES S, REKHTER Y, LI T. A border gateway protocol 4(BGP-4)[M]. RFC Editor, 2006.[4] 杨言. 互联网域间路由劫持及其防御研究[D]. 北京:清华大学, 2020.[5] MURPHY S. BGP security vulnerabilities analysis[J].Work in Progress, draft-ietf-idr-bgp-vuln-00. txt, 2006.[6] BAKKALI S, BENABOUD H, MAMOUN M B. Security problems in BGP: an overview[C]//Security Days. IEEE, 2013.[7] KELLER R M . Formal verif icati on of parallel programs[J]. Communications of the ACM, 1976,19(7):371-384.[8] FU Y, KON O. Security and robustness by protocol testing[J]. IEEE Systems Journal, 2014,8(3):699-707. DOI:10.1109/JSYST.2012.2223532.[9] KHORCHEF S. Un cardre formel pour le test de robustesse des protocols de communication[D]. Univ.Bordeaux, France, 2007.[10] 李巍海. 网络协议健壮性测试平台关键技术研究[D]. 北京:北京邮电大学, 2015.
Input/Output labeled transition system based robustness analysis model of routing protocol
ZHOU Kaibo, ZHANG Zhibing, WANG Xiaoyu, LIU Xindong
(CTTL System Laboratory, China Academy of Information Communication Technology, Beijing 100191, China)
Abstract: The robustness of the routing protocol is the key factor of the robustness of the router and switch. How to analyze and evaluate the robustness of the routing protocol is the focus of the security evaluation of the critical network device. In this paper, an analysis method model based on Input/Output Labeled Transition System(IOLTS) of the robustness of routing protocol in network equipment is proposed. Ospfv2 routing protocol is analyzed and verified as an example using the model.Keywords: critical network device; routing protocol; OSPF; IOLTS; robustness
本文刊于《信息通信技术与政策》2022年 第4期
主办：中国信息通信研究院
《信息通信技术与政策》是工业和信息化部主管、中国信息通信研究院主办的专业学术期刊。本刊定位于“信息通信技术前沿的风向标，信息社会政策探究的思想库”，聚焦信息通信领域技术趋势、公共政策、国家/产业/企业战略，发布前沿研究成果、焦点问题分析、热点政策解读等，推动5G、工业互联网、数字经济、人工智能、区块链、大数据、云计算等技术产业的创新与发展，引导国家技术战略选择与产业政策制定，搭建产、学、研、用的高端学术交流平台。
《信息通信技术与政策》官网开通啦！
为进一步提高期刊信息化建设水平，为广大学者提供更优质的服务，我刊于2020年11月18日起正式推出官方网站，现已进入网站试运行阶段。我们将以更专业的态度、更丰富的内容、更权威的报道，继续提供有前瞻性、指导性、实用性的优秀文稿，为建设网络强国和制造强国作出更大贡献！
推荐阅读
你“在看”我吗？