引用本文
  • 金希文,葛强,张进,丁建,江逸茗,马海龙,伊鹏.拟态路由器TCP代理设计实现与形式化验证研究[J].信息安全学报,已采用    [点击复制]
  • Jin Xiwen,Ge Qiang,Zhang Jin,Ding Jian,Jiang Yiming,Ma Hailong,Yi Peng.Design, implementation and formal verification of TCP proxy in mimic defense router[J].Journal of Cyber Security,Accept   [点击复制]
【打印本页】 【在线阅读全文】【下载PDF全文】 查看/发表评论下载PDF阅读器关闭

过刊浏览    高级检索

本文已被:浏览 309次   下载 0  
拟态路由器TCP代理设计实现与形式化验证研究
金希文1, 葛强1, 张进2, 丁建2, 江逸茗2, 马海龙2, 伊鹏3
0
(1.东南大学;2.网络通信与安全紫金山实验室;3.信息工程大学)
摘要:
拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1:1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。
关键词:  拟态防御  形式化验证
DOI:
投稿时间:2022-02-15修订日期:2022-05-03
基金项目:
Design, implementation and formal verification of TCP proxy in mimic defense router
Jin Xiwen1, Ge Qiang1, Zhang Jin2, Ding Jian2, Jiang Yiming2, Ma Hailong2, Yi Peng3
(1.Southeast University;2.Purple Moutain Laboratories;3.Information Engineering University)
Abstract:
The mimic defense router is designed based on the dynamic heterogeneous redundant architecture of mimic defense, which has good defense capability for unknown vulnerability backdoor. The protocol proxy is in the pivotal posi-tion of internal and external communication in the mimic defense router, and the security and functional correctness of the protocol proxy are of great importance to the mimic defense router. In this paper, we design and implement a TCP protocol proxy for the mimic defense router, and verify its security and functional correctness using a formal approach. The TCP protocol proxy sniffs TCP messages between neighbors and master entities, simulates the estab-lishment of TCP connections between neighbors and slave entities, and provides a programmatic interface to the upper layer application layer protocol proxy. Based on the idea of separation logic and combination, the Verifast theorem provers are used to verify the low-level properties of the TCP protocol proxy, including the safe use of pointers, no memory leakage, and no dead code, etc. Also, some high-level properties of each major functional module of the TCP protocol proxy are formally verified. A mimic defense router experimental environment con-taining three entities was built and the results of the implementation were tested in practice, and the results showed that the implemented TCP proxy achieved the expected functionality. The TCP protocol proxy implementation totals 1611 lines of C code, of which a total of 588 lines of proofs written by a manually guided theorem checker are re-quired for formal verification. In practice, the time required to write the code implementation and the manual proof is about 1:1. The implementation and formal verification work of the TCP protocol proxy in this paper demonstrates that it is indeed feasible to introduce formal verification into the development of key components of mimic defense routers, and that the cost is provably acceptable.
Key words:  mimic defense  formal verification