本文已被：浏览 2212次 下载 2509次
Received:February 09, 2018 Revised:March 07, 2018
Received:February 09, 2018 Revised:March 07, 2018
中文摘要: 现有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.
keywords: RPKI Delta SPIN incremental synchronization formal verification model checking protocol security
文章编号： 中图分类号： 文献标志码：
基金项目:
引用文本：
司昊林,马迪,毛伟,王伟,邵晴.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
司昊林,马迪,毛伟,王伟,邵晴.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
