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

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

Abstract

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

CLC Number:

TP393

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.

Figures/Tables 23

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

特性名称	验证方法
内存泄露	每个函数堆上的内存块只有 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

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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 23

References 22

Related Articles 15

Metrics

Recommended 0

[1]	Dacheng ZHOU, Hongchang CHEN, Guozhen CHENG, Weizhen HE, Ke SHANG, Hongchao HU. Design and implementation of adaptive mimic voting device oriented to persistent connection [J]. Journal on Communications, 2022, 43(6): 71-84.
[2]	Hongyong JIA, Yunfei PAN, Wenhe LIU, Junjie ZENG, Jianhui ZHANG. Executive dynamic scheduling algorithm based on high-order heterogeneity [J]. Journal on Communications, 2022, 43(3): 233-245.
[3]	Zhengbin ZHU, Qinrang LIU, Dongpei LIU, Chong WANG. Research progress of mimic multi-execution scheduling algorithm [J]. Journal on Communications, 2021, 42(5): 179-190.
[4]	Ting WU, Chengnan HU, Qingnan CHEN, Anbang CHEN, Qiuhua ZHENG. Defense-enhanced dynamic heterogeneous redundancy architecture based on executor partition [J]. Journal on Communications, 2021, 42(3): 122-134.
[5]	Chuanxing PAN, Zheng ZHANG, Bolin MA, Yuan YAO, Xinsheng JI. Method against process control-flow hijacking based on mimic defense [J]. Journal on Communications, 2021, 42(1): 37-47.
[6]	Shaohu DING,Ning QI,Yiwei GUO. Evaluation of mimic defense strategy based on M-FlipIt game model [J]. Journal on Communications, 2020, 41(7): 186-194.
[7]	Qinglei ZHOU,Shaohuan BAN,Yingjie HAN,Feng FENG. Mimic defense authentication method for physical access control [J]. Journal on Communications, 2020, 41(6): 80-87.
[8]	Ke SONE,Qinrang LIU,Shuai WEI,Wenjian ZHANG,Libo TAN. Endogenous security architecture of Ethernet switch based on mimic defense [J]. Journal on Communications, 2020, 41(5): 18-26.
[9]	Yuan YAO,Chuanxing PAN,Zheng ZHANG,Gaofei ZHANG. Method of quantitative assessment for diversified software system [J]. Journal on Communications, 2020, 41(3): 120-125.
[10]	Zhongyi GUO,Zhenzhen PAN,Chaofan GONG,Zikun WANG,Kai GUO,Hongping ZHOU. Research on router device of OAM optical communication [J]. Journal on Communications, 2020, 41(11): 185-197.
[11]	Xingming ZHANG,Zeyu GU,Shuai WEI,Jianliang SHEN. Markov game modeling of mimic defense and defense strategy determination [J]. Journal on Communications, 2018, 39(10): 143-154.
[12]	Liang LIANG,Yuan CAO,Lian-chuan MA,Yu-zhuo ZHANG,Heng-kui LI. Formal verification and implementation of safety computer communication management mechanism [J]. Journal on Communications, 2016, 37(11): 196-204.
[13]	Long-hai LI,Cheng-qiang HUANG,Wan-xing WANG,Jian-jun MU. Attacks on Telex Internet anticensorship system [J]. Journal on Communications, 2014, 35(9): 40-56.
[14]	Lai-quan HAN,Jin-kuan WANG,Xing-wei WANG. Flow-splitting algorithm of MPLS single label based on programmable router [J]. Journal on Communications, 2014, 35(5): 155-159.
[15]	. Flow-splitting algorithm of MPLS single label based on programmable router [J]. Journal on Communications, 2014, 35(5): 20-159.