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

摘要：

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

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

所属期刊栏目：44

分类号：TP393(计算技术、计算机技术)

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

在线出版日期：2023-04-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：33-44