期刊文献+

RPKI增量同步Delta协议的形式化检测与实现 被引量:3

Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol
下载PDF
导出
摘要 现有RPKI体系中, RPKI资料库与RP服务器之间的数据同步使用开源工具Rsync,但由于RPKI体系中证书数据结构的特殊性,使用Rsync进行数据的同步不仅效率低下,而且Rsync会消耗过多的系统资源,从而使整个RPKI体系遭遇潜在的安全风险.因此, IETF针对RPKI资料库数据特征,提出增量同步Delta协议以替代Rsync在RPKI中的作用.本文详细介绍了Delta协议的工作逻辑和机制,从安全性和高效性两方面将之与Rsync进行全面对比,并使用Promela语言构建Delta协议模型,借助形式化验证工具SPIN对该模型进行验证,从而证明该协议具备较高的协议安全性和稳定性.最后,本文给出Delta协议的实现结构. 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.
作者 司昊林 马迪 毛伟 王伟 邵晴 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)
出处 《计算机系统应用》 2018年第11期1-8,共8页 Computer Systems & Applications
关键词 RPKI DELTA SPIN 增量同步 形式化检测 模型检查 协议安全性 RPKI Delta SPIN incremental synchronization formal verification model checking protocol security
  • 相关文献

参考文献8

二级参考文献66

  • 1王千祥,申峻嵘,梅宏.自适应软件初探[J].计算机科学,2004,31(10):168-171. 被引量:21
  • 2卢锡城,赵金晶,朱培栋,董攀.域间路由系统自组织特性[J].软件学报,2006,17(9):1922-1932. 被引量:10
  • 3Object Management Group.version 2.1.1 Unified Modeling Language : Superstructure[S].2007.
  • 4Clarke E M Jr,Grumberg O,Peled D A.Model checking[M|.4th ed. Cambridge, Massachusetts : MIT Press, 2002.
  • 5Holzmann G J.The spin model checker:primer and reference manual[M].[S.1.] : Addison Wesley, 2003.
  • 6MOCES :Model ChEcking Statecharts [CP/OL].http://www.informatik. uni-kiel.de/inf/deRoever/research.html.
  • 7Mikk E,Lakhnech Y,Siegel M,et al.Implementing statecharts in PROMELA/SPIN[C]//Proceedings of the 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques,IEEE Computer Society,October 21-23,1998.90-101.
  • 8Latella D,Majzik I,Massink M.Automatic verification of a behavioural subset of UML stateehart diagrams using the SPIN modelcheeker[J].Formal Aspects of Computing, 1999,11 (6) : 637-664.
  • 9Latella D,Majzik I,Massink M.Towardsa formal operational semantics of UML statechart diagrams[C]//Proc FMOODS'99,IFIPTC6/ WG6.1.Third International Conference on Formal Methods for Open Object-Based Distributed Systems,Florence,Italy,February 15-18,1999.
  • 10Paltor I,Lilius J.Vuml:a tool for verifying UML models[C]//Proc of the 14th IEEE International Conference on Automated Software Engineering, ASE'99, IEEE, 1999.

共引文献80

同被引文献12

引证文献3

二级引证文献6

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部