| 拟态路由器TCP代理设计实现与形式化验证研究 |
| |
| 作者姓名： | 金希文 葛强 张进 丁建 江逸茗 马海龙 伊鹏 |
| |
| 作者单位： | 东南大学 网络空间安全学院 南京 中国 211100;紫金山实验室 内生安全研究中心 南京 中国 211100;紫金山实验室 内生安全研究中心 南京 中国 211100;中国人民解放军信息工程大学 郑州 中国 |
| |
| 基金项目： | 本课题得到紫金山实验室自立课题“面向私有云的内生安全多模态基础网络” (No. ZL042301)资助。 |
| |
| 摘 要： | 拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1:1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。
|
| 关 键 词： | 拟态防御|形式化验证 |
| 收稿时间： | 2022/2/15 0:00:00 |
| 修稿时间： | 2022/5/3 0:00:00 |
Design, Implementation and Formal Verification of TCP Proxy in Mimic Defense Router |
| |
| Authors: | JIN Xiwen GE Qiang ZHANG Jin DING Jian JIANG Yiming MA Hailong YI Peng |
| |
| Affiliation: | 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: | |
| |
| Keywords: | mimic defense|formal verification |
|
| 点击此处可从《》浏览原始摘要信息 |
|
点击此处可从《》下载全文 |
|
