拟态路由器BGP代理的设计实现与形式化验证

doi:10.11959/j.issn.1000-436x.2023065

通信学报 ›› 2023, Vol. 44 ›› Issue (3): 33-44.doi: 10.11959/j.issn.1000-436x.2023065

拟态路由器BGP代理的设计实现与形式化验证

张进¹, 葛强¹^,², 徐伟海¹^,², 江逸茗³, 马海龙³, 于洪涛³

¹ 紫金山实验室内生安全研究中心，江苏南京 211100
² 东南大学网络空间安全学院，江苏南京 211100
³ 信息工程大学信息技术研究所，河南郑州 450000

修回日期:2023-02-27 出版日期:2023-03-25 发布日期:2023-03-01
作者简介:张进（1979− ），男，江苏镇江人，博士，紫金山实验室高级工程师，主要研究方向为宽带信息网络、网络安全、软硬件协同设计
葛强（1997− ），男，浙江台州人，东南大学硕士生，主要研究方向为网络安全
徐伟海（1999− ），男，安徽黄山人，东南大学硕士生，主要研究方向为网络安全
江逸茗（1984– ），男，河南郑州人，博士，信息工程大学副研究员，主要研究方向为新型网络体系结构、网络空间安全防御、云计算、虚拟化技术
马海龙（1980– ），男，山东聊城人，博士，信息工程大学研究员，主要研究方向为创新网络体系、网络安全管控、路由工程等
于洪涛（1970− ），男，辽宁丹东人，博士，信息工程大学研究员，主要研究方向为网络空间安全
基金资助:
国家重点研发计划基金资助项目(2022YFB2901400)

Design, implementation and formal verification of BGP proxy for mimic router

Jin ZHANG¹, Qiang GE¹^,², Weihai XU¹^,², Yiming JIANG³, Hailong MA³, Hongtao YU³

¹ The Endogenous Security Research Centre, Purple Mountain Laboratories, Nanjing 211100, China
² School of Cyber Science and Engineering, Southeast University, Nanjing 211100, China
³ Institute of Information Technology, Information Engineering University, Zhengzhou 450000, China

Revised:2023-02-27 Online:2023-03-25 Published:2023-03-01
Supported by:
The National Key Research and Development Program of China(2022YFB2901400)

摘要/Abstract

摘要：

为确保拟态路由器中协议代理等“拟态括号”关键组件的安全性和功能正确性，设计实现了边界网关协议（BGP）代理，并采用形式化方法对BGP代理的安全性和功能正确性进行了验证。BGP代理通过监听邻居路由器与主执行体之间的BGP会话报文，模拟邻居路由器与从执行体展开BGP会话，实现各执行体的BGP状态一致。采用VeriFast定理证明器，编写基于分离逻辑的形式化规约，证明程序不会出现空指针引用等内存安全问题，并验证了BGP代理各功能模块实现的高级属性符合功能规约。BGP代理实现与验证代码量之比约为1.8:1，程序设计实现和程序验证所耗费的时间之比约为1:3。经过形式化验证的BGP代理处理100 000条BGP路由所花费的时间为0.16 s，约为未经过验证的BGP代理的7倍。研究工作为应用形式化方法证明拟态防御设备与系统中关键组件的安全性和功能正确性提供了参考。

关键词: 拟态防御, 边界网关协议, 路由器, 形式化验证

Abstract:

To ensure the safety and correctness of the critical ‘mimic bracket’ components such as protocol proxies of mimic routers, a BGP (border gateway protocol) proxy was designed and implemented, and formal methods were applied to verify the safety and correctness of the BGP proxy.The BGP packets communicated between the peer routers and the master actor were monitored by the BGP proxy.The BGP sessions with the slave actors on behalf of peer routers were established, ensuring the consistency of the BGP protocol states for all actors.The formal specification of the BGP proxy was written based on separation logic.The VeriFast theorem prover was used to prove that the program had no memory safety problems such as null pointer reference.Furthermore, the formal verification of high-level attributes of each module in BGP proxy was also conducted to strictly ensure that the implementation met the specification.The implementation to proof code ratio of BGP proxy is about 1.8:1, and the implementation to proof labor hour ratio is about 1:3.The formally verified BGP proxy consume 0.16 seconds to process 100 000 BGP routes, which is about 7 times as long as the unverified one.Works done provide a reference for applying formal methods to verify the safety and correctness of critical components in mimic defense equipment and systems.

Key words: mimic defense, BGP, router, formal verification

中图分类号:

TP393

张进, 葛强, 徐伟海, 江逸茗, 马海龙, 于洪涛. 拟态路由器BGP代理的设计实现与形式化验证[J]. 通信学报, 2023, 44(3): 33-44.

Jin ZHANG, Qiang GE, Weihai XU, Yiming JIANG, Hailong MA, Hongtao YU. Design, implementation and formal verification of BGP proxy for mimic router[J]. Journal on Communications, 2023, 44(3): 33-44.

图/表 23

图1

图2

图3

图4

图5

图6

图7

图8

图9

图10

表1

图11

表2

表3

表4

图12

图13

图14

图15

图16

表5

表6

图17

参考文献 22

[1]	ISLAM S , PAPASTERGIOU S , KALOGERAKI E M ,et al. Cyberattack path generation and prioritisation for securing healthcare systems[J]. Applied Sciences, 2022,12(9): 4443.
[2]	Cisco. Cisco small business RV series routers vulnerabilities[R]. 2022.
[3]	马海龙, 伊鹏, 江逸茗 ,等. 基于动态异构冗余机制的路由器拟态防御体系结构[J]. 信息安全学报, 2017,2(1): 29-42.
	MA H L , YI P , JIANG Y M ,et al. Dynamic heterogeneous redundancy based router architecture with mimic defenses[J]. Journal of Cyber Security, 2017,2(1): 29-42.
[4]	邬江兴 . 网络空间拟态防御研究[J]. 信息安全学报, 2016,1(4): 1-10.
	WU J X . Research on cyber mimic defense[J]. Journal of Cyber Security, 2016,1(4): 1-10.
[5]	DOBRESCU M , ARGYRAKI K . Software dataplane verification[C]// Proceedings of 11th Symposium on Networked Systems Design and Implementation. New York:ACM Press, 2014: 101-114.
[6]	ZHANG K , ZHUO D , AKELLA A ,et al. Automated verification of customizable middlebox properties with gravel[C]// Proceedings of 17th USENIX Symposium on Networked Systems Design and Implementation. New York:ACM Press, 2020: 221-239.
[7]	MOURA D L , BJORNER N . Satisfiability modulo theories:introduction and applications[J]. Communications of the ACM, 2011,54(9): 69-77.
[8]	ZAOSTROVNYKH A , PIRELLI S , PEDROSA L ,et al. A formally verified NAT[C]// Proceedings of the Conference of the ACM Special Interest Group on Data Communication. New York:ACM Press, 2017: 141-154.
[9]	ZAOSTROVNYKH A , PIRELLI S , IYER R ,et al. Verifying software network functions with no verification expertise[C]// Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York:ACM Press, 2019: 275-290.
[10]	LIU J , HALLAHAN W , SCHLESINGER C ,et al. P4V:practical verification for programmable data planes[C]// Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. New York:ACM Press, 2018: 490-503.
[11]	DUMITRESCU D , STOENESCU R , NEGREANU L ,et al. BF4:towards bug-free P4 programs[C]// Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the Applications,Technologies,Architectures,and Protocols for Computer Communication. New York:ACM Press, 2020: 571-585.
[12]	TIAN B C , GAO J Q , LIU M Q ,et al. Aquila:a practically usable verification system for production-scale programmable data planes[C]// Proceedings of the 2021 ACM SIGCOMM 2021 Conference. New York:ACM Press, 2021: 17-32.
[13]	JACOBS B , PIESSENS F . The VeriFast program verifier[R]. 2008.
[14]	MOURA D L , BJ?RNER N . Z3:an efficient SMT solver[C]// Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2008: 337-340.
[15]	邬江兴 . 网络空间内生安全发展范式[J]. 中国科学:信息科学, 2022,52(2): 189-204.
	WU J X . Development paradigms of cyberspace endogenous safety and security[J]. Scientia Sinica (Informationis), 2022,52(2): 189-204.
[16]	宋克, 刘勤让, 魏帅 ,等. 基于拟态防御的以太网交换机内生安全体系结构[J]. 通信学报, 2020,41(5): 18-26.
	SONG K , LIU Q R , WEI S ,et al. Endogenous security architecture of Ethernet switch based on mimic defense[J]. Journal on Communications, 2020,41(5): 18-26.
[17]	欧阳玲, 贺磊, 宋克 ,等. 基于编码信道理论的拟态括号设计方法[J]. 信息工程大学学报, 2021,22(4): 456-461.
	OUYANG L , HE L , SONG K ,et al. Design method of mimicry brackets based on coding channel theory[J]. Journal of Information Engineering University, 2021,22(4): 456-461.
[18]	金希文, 葛强, 张进 ,等. 拟态路由器TCP代理设计实现与形式化验证研究[D]. 南京:东南大学, 2022.
	JIN X W , GE Q , ZHANG J ,et al. Design,implementation and formal verification of TCP proxy in mimic defense router[D]. Nanjing:Southeast University, 2022.
[19]	BALDONI R , COPPA E , D’ELIA D C ,et al. A survey of symbolic execution techniques[J]. ACM Computing Surveys, 2019,51(3): 1-39.
[20]	REYNOLDS J C , . Separation logic:a logic for shared mutable data structures[C]// Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. Piscataway:IEEE Press, 2002: 55-74.
[21]	JACOBS B , VOGELS F , PIESSENS F . Featherweight VeriFast[J]. Logical Methods in Computer Science, 2015,11(3): 1-57.
[22]	GE Q . BGP proxy source code[R]. 2023.

特性名称	验证方法
内存泄露	每个函数堆上的内存块只有 2 个结果，一个在函数中被释放，另一个被添加到后置条件中返回上层函数。如果一块内存既没有在函数中被释放，也没有作为后置条件的一部分返回上层函数，那么该函数的验证就会报错，错误显示有内存块泄露
空指针引用	对于未在函数内赋值或判断非空以及前置条件中未明确描述非空的指针，符号执行会生成空指针的路径继续运行，从而导致验证不通过
指针多次释放	程序每次申请动态内存时，会将该内存的符号值放入函数堆中，释放时删除。如果一块内存已经被释放后再次被释放，验证会因为在函数堆中找不到该块内存的符号值而报错
指针访问的内存安全	程序申请动态内存时，会保存内存的符号值，用以详细描述该内存。通过检查当前函数是否拥有对这块内存的访问权限检查指针的解引用操作是否正确

模块名称	已验证的功能特性
初始化模块	1) 堆上应有Peers、Slaves和连接池对应的内存块；
	2) 连接池中连接数为空；
	3) Peers和Slaves中每个元素的IP值与配置文件中的信息一致；
	4) Slaves中每个元素的状态都为在线，Peers中每个元素的状态都为离线
报文顶层处理模块	1) 对于不同类型的报文，程序调用的行为函数正确；
	2) 每个行为函数对于指定的输入，输出符合预期，即函数的功能正确
BGP状态管理模块	1) 运行发送OPEN报文的函数后，判断连接状态为OpenSend；
	2) 发送 KEEPALIVE 报文的函数中，如果前置条件中连接状态为 OpenSend，则后置条件应该判断连接状态为OpenConfirm，如果前置条件中连接状态为OpenConfirm，则后置条件判断连接状态为Established
执行体状态同步模块	1) 运行上线函数之后，从执行体状态为在线；
	2) 运行下线函数之后，从执行体状态为离线；
	3) 从执行体s上线后，能将所有邻居路由器的UPDATE报文发给s

模块	C程序代码行数	验证代码行数	验证代码行数/C程序代码行数×100%（保留两位小数）	总行数
初始化模块	74	43	58%	117
报文顶层处理模块（除BGP状态管理模块）	377	217	57%	594
BGP状态管理模块	489	301	61%	790
执行体状态同步模块	40	27	68%	67
其他部分	298	120	40%	418
总计	1 278	708	55%	1 986

设备名	IP地址	本地AS号	配置的邻居AS号
Peer	192.168.180.129/24	129	130
Master	192.168.180.130/24	130	129
Slave₁	192.168.180.131/24	131	129
Slave₂	192.168.180.132/24	132	129
BGP-Proxy	192.168.180.133/24	—	—

场景	步骤	T₁	T₂	T₃	T₄	T₅	T₆	T₇	T₈	T₉	T₁₀	A
	R	0.010 6	0.012 9	0.016 7	0.017 0	0.014 5	0.018 2	0.017 2	0.015 2	0.016 4	0.014 1	0.015 3
1 000条路由	B	0.027 6	0.021 6	0.023 9	0.023 8	0.023 7	0.029 4	0.030 1	0.025 5	0.026 1	0.023 1	0.025 5
	O	0.017 0	0.008 7	0.007 2	0.006 8	0.009 2	0.011 2	0.012 9	0.010 3	0.009 7	0.009 0	0.010 2
	R	0.079 7	0.105 5	0.035 1	0.054 0	0.053 8	0.062 6	0.058 7	0.066 1	0.055 7	0.063 2	0.063 4
10 000条路由	B	0.097 5	0.126 7	0.059 8	0.076 4	0.077 7	0.090 1	0.082 6	0.089 2	0.073 4	0.087 8	0.086 1
	O	0.017 8	0.021 2	0.024 7	0.022 4	0.023 9	0.027 5	0.023 9	0.023 1	0.017 7	0.024 6	0.022 7
	R	0.193 9	0.091 4	0.203 1	0.196 8	0.071 0	0.195 0	0.151 5	0.083 4	0.087 9	0.105 7	0.138 0
100 000条路由	B	0.216 0	0.100 3	0.219 3	0.207 3	0.075 4	0.206 7	0.216 5	0.091 9	0.102 7	0.139 6	0.157 6
	O	0.022 1	0.008 9	0.016 2	0.010 5	0.004 4	0.011 7	0.065 0	0.008 5	0.014 8	0.033 9	0.019 6

拟态路由器BGP代理的设计实现与形式化验证

Design, implementation and formal verification of BGP proxy for mimic router

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 23

参考文献 22

相关文章 15

Metrics

推荐阅读 0

[1]	赵仕祺, 黄小红, 钟志港. 基于信誉的域间路由选择机制的研究与实现[J]. 通信学报, 2023, 44(6): 47-56.
[2]	周大成, 陈鸿昶, 程国振, 何威振, 商珂, 扈红超. 面向持久性连接的自适应拟态表决器设计与实现[J]. 通信学报, 2022, 43(6): 71-84.
[3]	贾洪勇, 潘云飞, 刘文贺, 曾俊杰, 张建辉. 基于高阶异构度的执行体动态调度算法[J]. 通信学报, 2022, 43(3): 233-245.
[4]	朱正彬, 刘勤让, 刘冬培, 王崇. 拟态多执行体调度算法研究进展[J]. 通信学报, 2021, 42(5): 179-190.
[5]	吴铤, 胡程楠, 陈庆南, 陈安邦, 郑秋华. 基于执行体划分的防御增强型动态异构冗余架构[J]. 通信学报, 2021, 42(3): 122-134.
[6]	潘传幸, 张铮, 马博林, 姚远, 季新生. 面向进程控制流劫持攻击的拟态防御方法[J]. 通信学报, 2021, 42(1): 37-47.
[7]	丁绍虎,齐宁,郭义伟. 基于M-FlipIt博弈模型的拟态防御策略评估[J]. 通信学报, 2020, 41(7): 186-194.
[8]	周清雷,班绍桓,韩英杰,冯峰. 针对物理访问控制的拟态防御认证方法[J]. 通信学报, 2020, 41(6): 80-87.
[9]	宋克,刘勤让,魏帅,张文建,谭力波. 基于拟态防御的以太网交换机内生安全体系结构[J]. 通信学报, 2020, 41(5): 18-26.
[10]	姚远,潘传幸,张铮,张高斐. 多样化软件系统量化评估方法[J]. 通信学报, 2020, 41(3): 120-125.
[11]	郭忠义,潘珍珍,龚超凡,王子坤,郭凯,周红平. OAM光通信路由器件研究[J]. 通信学报, 2020, 41(11): 185-197.
[12]	张兴明,顾泽宇,魏帅,沈剑良. 拟态防御马尔可夫博弈模型及防御策略选择[J]. 通信学报, 2018, 39(10): 143-154.
[13]	梁靓,曹源,马连川,张玉琢,李恒奎. 安全计算机通信管理机制的形式化验证与实现[J]. 通信学报, 2016, 37(11): 196-204.
[14]	李龙海,黄城强,王万兴,慕建君. 对Telex互联网反监管系统的攻击[J]. 通信学报, 2014, 35(9): 40-56.
[15]	卢泽新,张晓哲,马世聪,王宝生. 面向多网络体制并存的开放式可重构路由器体系结构设计与实践[J]. 通信学报, 2013, 34(3): 126-133.