| 摘要: |
| 拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1:1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。 |
| 关键词: 拟态防御|形式化验证 |
| DOI：10.19363/J.cnki.cn10-1380/tn.2023.09.01 |
| 投稿时间：2022-02-15修订日期：2022-05-03 |
| 基金项目:本课题得到紫金山实验室自立课题“面向私有云的内生安全多模态基础网络” (No. ZL042301)资助。 |
|
| Design, Implementation and Formal Verification of TCP Proxy in Mimic Defense Router |
| JIN Xiwen,GE Qiang,ZHANG Jin,DING Jian,JIANG Yiming,MA Hailong,YI Peng |
| School of Cyber Science and Engineering, Southeast University, Nanjing 211100, China;Endogenous Security Research Center, Purple Moutain Laboratories, Nanjing 211100, China;Endogenous Security Research Center, Purple Moutain Laboratories, Nanjing 211100, China;Information Engineering University, Zhengzhou 450000, China |
| 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 position 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 establishment 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 containing 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 required 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 |
