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

作     者：张进 葛强 徐伟海 江逸茗 马海龙 于洪涛 ZHANG Jin;GE Qiang;XU Weihai;JIANG Yiming;MA Hailong;YU Hongtao

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

出 版 物：《通信学报》 (Journal on Communications)

年 卷 期：2023年第44卷第3期

页      面：33-44页

核心收录：

学科分类：0810[工学-信息与通信工程] 1205[管理学-图书情报与档案管理] 12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 0839[工学-网络空间安全] 08[工学] 0811[工学-控制科学与工程] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家重点研发计划基金资助项目(No.2022YFB2901400) 

主　　题：拟态防御 边界网关协议 路由器 形式化验证 

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