###
计算机系统应用:2018,27(11):1-8
本文二维码信息
码上扫一扫!
RPKI增量同步Delta协议的形式化检测与实现
司昊林1,2,3, 马迪2, 毛伟2,3, 王伟2, 邵晴3
(1.中国科学院 计算机网络信息中心, 北京 100190;2.中国科学院大学, 北京 100049;3.互联网域名系统北京市工程研究中心, 北京 100190)
Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol
SI Hao-Lin1,2,3, MA Di2, MAO Wei2,3, WANG Wei2, SHAO Qing3
(1.Computer Network Information Center, Chinese Academy of Sciences, Beijing 100190, China;2.University of Chinese Academy of Sciences, Beijing 100049, China;3.ZDNS Co. Ltd., Beijing 100190, China)
摘要
图/表
参考文献
相似文献
本文已被:浏览 215次   下载 104
投稿时间:2018-02-09    修订日期:2018-03-07
中文摘要: 现有RPKI体系中,RPKI资料库与RP服务器之间的数据同步使用开源工具Rsync,但由于RPKI体系中证书数据结构的特殊性,使用Rsync进行数据的同步不仅效率低下,而且Rsync会消耗过多的系统资源,从而使整个RPKI体系遭遇潜在的安全风险.因此,IETF针对RPKI资料库数据特征,提出增量同步Delta协议以替代Rsync在RPKI中的作用.本文详细介绍了Delta协议的工作逻辑和机制,从安全性和高效性两方面将之与Rsync进行全面对比,并使用Promela语言构建Delta协议模型,借助形式化验证工具SPIN对该模型进行验证,从而证明该协议具备较高的协议安全性和稳定性.最后,本文给出Delta协议的实现结构.
Abstract:In the existing RPKI system, the open source tool Rsync is used to synchronize data between the RPKI databases and the RP servers. However, due to the particularity of the certificate data structure in the RPKI system, data synchronization using Rsync not only is inefficient, but also consumes too much system resources, so that the entire RPKI system suffers potential security risks. Therefore, the IETF proposes an incremental synchronization Delta protocol to replace Rsync's role in RPKI. This paper introduces the working logic and mechanism of Delta protocol in detail, compares it with Rsync in terms of security and efficiency, constructs the Delta protocol model by using Promela language, and verifies the model with formal verification tool SPIN. It proves that the protocol has high protocol security and stability. Finally, this paper presents the Delta protocol implementation structure, in order to offer reference and communication.
文章编号:     中图分类号:    文献标志码:
基金项目:
引用文本:
司昊林,马迪,毛伟,王伟,邵晴.RPKI增量同步Delta协议的形式化检测与实现.计算机系统应用,2018,27(11):1-8
SI Hao-Lin,MA Di,MAO Wei,WANG Wei,SHAO Qing.Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol.COMPUTER SYSTEMS APPLICATIONS,2018,27(11):1-8

用微信扫一扫

用微信扫一扫