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

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

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

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