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

引用本文

司昊林, 马迪, 毛伟, 王伟, 邵晴. RPKI增量同步Delta协议的形式化检测与实现. 计算机系统应用, 2018, 27(11): 1-8.http://www.c-s-a.org.cn/1003-3254/6562.html

Si HL, Ma D, Mao W, Wang W, Shao Q. Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol. Computer Systems and Applications, 2018, 27(11): 1-8(in Chinese).http://www.c-s-a.org.cn/1003-3254/6562.html

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

司昊林^1,2,3, 马迪², 毛伟^2,3, 王伟², 邵晴³

1. 中国科学院计算机网络信息中心, 北京 100190;
2. 中国科学院大学, 北京 100049;
3. 互联网域名系统北京市工程研究中心, 北京 100190

收稿日期：2018-02-09; 修改日期：2018-03-07; 采用时间：2018-03-14; csa 在线出版时间：2018-09-30

通讯作者：司昊林, E-mail: 1335800763@qq.com.

摘要：现有RPKI体系中, RPKI资料库与RP服务器之间的数据同步使用开源工具Rsync, 但由于RPKI体系中证书数据结构的特殊性, 使用Rsync进行数据的同步不仅效率低下, 而且Rsync会消耗过多的系统资源, 从而使整个RPKI体系遭遇潜在的安全风险. 因此, IETF针对RPKI资料库数据特征, 提出增量同步Delta协议以替代Rsync在RPKI中的作用. 本文详细介绍了Delta协议的工作逻辑和机制, 从安全性和高效性两方面将之与Rsync进行全面对比, 并使用Promela语言构建Delta协议模型, 借助形式化验证工具SPIN对该模型进行验证, 从而证明该协议具备较高的协议安全性和稳定性. 最后, 本文给出Delta协议的实现结构.

关键词: RPKI Delta SPIN 增量同步形式化检测模型检查协议安全性

Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol

SI Hao-Lin^1,2,3, MA Di², MAO Wei^2,3, WANG Wei², SHAO Qing³

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

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.

Key words: RPKI Delta SPIN incremental synchronization formal verification model checking protocol security

1 RPKI原理简介

为了解决BGP路由劫持的网络安全隐患, 互联网工程任务组IETF (Internet Engineering Task Force)提出了RPKI (Resource Public Key Infrastructure)^[1]. RPKI解决此类隐患的基本思路是: 构建一整套公钥证书体系PKI (Public Key Infrastructure)对互联网码号资源INR (Internet Number Resource), 包括IP地址前缀和AS号的所有权(分配)和使用权(路由起源通告)进行验证, 通过验证的结果指示边境路由器是否接受收到的路由起源通告以修改自己的路由信息.

如图1所示的RPKI体系结构中, 顶级CA (Certi- ficate Authority)如IANA、RIR、NIR、ISP等在资源分配的过程中, 使用CA证书签发一系列用于标识资源所属关系的认证证书, 其中EE证书主要用于对路由源授权(Route Origin Authorization, ROA)进行验证, 从而确认某AS是否可以发起ASN与地址段相匹配的合法路由起源通告. 该体系结构中的RP (Relying Party)将从资料库同步到的证书构建成数据链表, 使用OpenSSL对其进行验证, 验证的结果缓存于本地数据库中, 再通过RTR (Relying party To Router)协议向路由器提供查询, 边界路由器通过向RP服务器发起查询以确认自身收到的路由源通告是否合法, 从而过滤由错误配置或恶意攻击等生成的非法路由起源通告, 避免路由劫持的发生^[2,3].

图 1 RPKI体系架构

2 Delta协议 2.1 Delta协议简介

由于Rsync在一般文件的同步过程中表现优异, IETF在RPKI提出初期, 建议使用Rsync作为RP和资料库之间的同步工具^[4]. 但由于RPKI数据资料的结构特殊性, 使用Rsync进行数据会存在明显缺陷和安全隐患^[5].

为了解决RPKI在使用Rsync过程中存在的缺陷和隐患, IETF在2015年2月发布了RRDP (RPKI Repository Delta Protocol, 简称Delta协议)草案. 经过10个版本的修订, 最终于2017年7月形成标准协议RFC 8182^[6].

相较于Rsync, Delta协议具有以下显著特征:

(1) RPKI资料库需要生成三个文件: 用以发布更新信息的Notification更新通告文件、用以发布大块证书打包数据的Snapshot快照文件和用以实现增量同步的Delta文件, 通过上述文件对同步过程的动态协调, 使RP服务器和RPKI资料库之间数据同步的可控性大幅提升.

(2) Delta协议的同步机制中, RPKI资料库针对证书文件的数据特性, 通过Delta文件实现对文件的精确增量更新, RP服务器初次运行需执行Snapshot快照文件外, 后续的增量更新只涉及微量数据, 迅捷高效.

(3) Delta协议将资料库的证书同步过程与其他功能模块彻底剥离, 这使得RP服务器的验证模块可以从本地直接检索构建验证链所需的证书数据, 验证效率被大幅提升. 此外, 同步至RP服务器的各类证书数据亦可以结合其他运行数据进行信息分析和挖掘, 对边界路由器提供与指导路由相关的增值服务.

(4) Delta协议中, 严格的控制文件校验和全方位的安全考量, 使得RPKI与RP服务器之间数据同步的安全性得到大幅提升, 同时RPKI资料库和RP服务器之间的控制文件分发采用HTTPS (Hyper Text Transfer Protocol over Secure socket layer)协议, 由于对传输数据进行了加密, 可以有效防止中间人(Monkey-In-the-Middle)攻击, 提升协议安全性^[7].

2.2 Delta协议工作机制

图2用以说明Delta协议的工作机制.

Delta协议工作机制

1) RPKI资料库需以时间t为周期, 循环生成Notification文件、Snapshot文件和Delta文件并对其进行维护, 这三种文件都由当前的Session_ID属性和文件Serial号码唯一标识, 并以URL方式发布以供远程获取, Session_ID本身为一个随机版本4的通用统一标识符UUID (Universally Unique Identifier), 用以对各个文件进行唯一性标识. Notification文件用于对RP服务器发布更新会话发起通告, 文件内容包括当前Delta版本属性<Version>、本次会话组合标识属性<Session_ID>和<Serial>, 同时也包括本次会话相关的Snapshot和Delta文件信息. 资料库生成的三个文件均为.xml文件.

2) RP服务器周期性获取Notification文件, 并对其内容进行解析. 各RP服务器可根据自身工具差异, 选取合适的方式对文件进行解析以获取文件信息, 本文中采用Python2.7的xml.etree.ElementTree模块对.xml文件进行解析, 并对文件数据构树以备后续使用.

3) RP服务器需对Notification文件格式进行验证. Delta协议对资料库生成的三种文件均进行了严格的格式规范, 若有任何格式细节不匹配的文件, 都必须在Delta协议执行的流程中被拒绝.

4) Notification文件中携带的<Version>属性值必须为“1”, 标识当前Delta协议版本号.

5) Notification文件中携带的<Serial>属性值需要和本地已存的“Serial”变量进行比较, 通常若RP服务器初次发起更新会话, “Serial”变量的值为初始值, 此时需要直接执行Snapshot文件, 至步骤6), 若<Serial>属性值大于本地“Serial”变量值, 则进行Delta增量更新, 至步骤8), 若“Serial”变量值为非初始值且大于等于<Serial>属性值, 则该Notification文件被拒绝, 至步骤11).

6) RP服务器通过Notification文件中Snapshot文件的URL获取Snapshot文件并验证其文件格式和HASH值, Snapshot文件的HASH值负载于Notification文件中, Delta协议中的文件HASH值均为SHA-256散列的十六进制编码. 还需验证Snapshot文件的<Session_ID>和<Serial>属性值是否与Notification匹配, 若上述三步验证中的任何一个验证失败, 将导致此Snapshot文件被拒绝, 至步骤11).

7) 执行Snapshot文件, 获取证书数据, 至步骤11).

8) 通常一个Notification文件会包含多个Delta文件信息, 需要对多个Delta文件依照<Serial>属性值增序构建文件链表DeltaFL, 并对DeltaFL依次验证和执行.

9) 验证Delta文件的文件格式、文件HASH值和<Session_ID>、<Serial>属性值, 任何一步验证失败都将导致此Delta文件被拒绝, 并执行Snapshot文件, 至步骤6).

10) 执行Delta文件, 获取证书数据, 若DeltaFL为空, 至步骤11), 若不为空, 则至步骤8).

11) 周期循环, 至步骤2).

2.3 Delta协议的形式化检测

Delta协议的各文件验证过程层叠环扣, 逻辑较为复杂, 为了准确且全面地说明Delta协议及其实现程序的协议正确性(协议正确性通常指: 不存在违背断言(assertion)的情况、不存在不可达(unreachable)状态、不存在死锁(deadlock)、可以完全覆盖定义的LTL (Linear Temporal Logic)公式等安全特性)^[8], 下文将借助用来验证协议或系统逻辑一致性的工具SPIN对Delta协议进行形式化检测, 以说明Delta具备较高的安全特性.

形式化方法是验证协议一致性和提高软件质量而经常使用的重要方法, 在所有形式化方法中, 模型检查是一种用于验证有穷状态系统模态/命题性质的自动验证技术, 最早由Clarke和Emerson等^[9]提出, 已经被成功地应用于计算机硬件、通信协议、控制系统和安全认证协议等方面的分析和验证中, 它的思想是检验系统中所有可能的状态, 验证这些状态是否满足某些性质. 如果不满足, 将产生一个反例以说明这种情况. 给定系统或协议模型M及LTL公式ϕ, 检测是否有 $L\left( {{A_\varphi }} \right) \subseteq {\rm{model}}\left( \varphi \right)$ 的步骤如算法1.

图 2 Delta协议工作机制示意图

算法1. 形式化检测算法

1) 构造自动机 $\scriptstyle{A_{\neg \varphi }}$ , 其对应公式 $\scriptstyle\neg \varphi $ ;

2) 计算 $\scriptstyle{A_{M,\varphi }} = M \times {A_{\neg \varphi }}$ 使得 $\scriptstyle L({A_{M,\varphi }}) = L(M) \cap L({A_{\neg \varphi }})$ ;

3) 判定 $\scriptstyle L({A_{M,\varphi }})$ 是否为空, 也就是 $\scriptstyle{A_{M,\varphi }}$ 不接受任何输入.

SPIN (Simple Promela Interpreter)是一款适合进行协议一致性检查的分析检测工具, 由贝尔实验室的形式化方法与验证小组开发, SPIN优秀的算法设计和有效的检测能力使其荣获由ACM (Association for Computing Machinery)授予的软件系统奖(software systems award), 其他获得此殊荣的还有Unix、TCP/IP、Tcl/Tk、Java、WWW等^[10]. 如图3所示的SPIN验证流程, SPIN可以接受由Promela建模语言构筑的协议或系统模型, 模型通常由消息通道、变量和进程进行描述. SPIN会将模型中构筑的进程翻译为有限自动机, 并对这些自动机进行异步积运算得到优先自动机A, 同时LTL公式会被取反转换为自动机B, 再将自动机A和B进行同步积运算得到自动机C, SPIN将使用内嵌的搜索算法对C进行穷尽搜索^[11], 搜索过程可以通过SPIN独有的On-the-fly技术以及偏序简化技术对状态空间进行简化, 搜索完毕的自动机C若其接受的语言为空, 则表示系统满足LTL描述的属性, 反之则不满足^[12].

图 3 SPIN模拟与验证结构流程图

(1) Delta协议的语言和有限状态机描述

定义一个四元组文法G: $G = (V,T,P,S)$ , 其中, V是变量集合, $\forall { A} \in V$ , A叫做一个语法变量; T是终极符的集合, T中的字符是语言的句子中出现的字符, $V \cap T = \emptyset $ ; P是产生式的集合, P中的元素具有形式 $\alpha \to \beta $ ; $S \in V$ , 文法G的开始符号.

因此, Delta协议的验证逻辑可以使用此语法G进行表述:

$\begin{array}{l}{G_D} = (\{ S,A,B,C\} ,\{ a,b,c\} ,\\\{ S \to aA,A \to aA|aB|aC,B \to aA|b,C \to aC|aB|c\} ,S)\end{array}$

则使用文法 ${G_D}$ 可生成如下的语言:

S	$\scriptstyle \Rightarrow aA$	使用产生式 $\scriptstyle S \to aA$
	$\scriptstyle \Rightarrow aaA$	使用产生式 $\scriptstyle A \to aA$
	$\scriptstyle \Rightarrow aaaB$	使用产生式 $\scriptstyle A \to aB$
	$\scriptstyle \Rightarrow aaaaA$	使用产生式 $\scriptstyle B \to aA$
	$\scriptstyle \Rightarrow aaaaB$	使用产生式 $\scriptstyle A \to aB$
	$\scriptstyle \Rightarrow aaaab$	使用产生式 $\scriptstyle B \to b$
S	$ \scriptstyle\Rightarrow aA$	使用产生式 $\scriptstyle S \to aA$
	$ \scriptstyle\Rightarrow aaC$	使用产生式 $\scriptstyle A \to aC$
	$ \scriptstyle\Rightarrow aaaC$	使用产生式 $\scriptstyle C \to aC$
	$ \scriptstyle\Rightarrow aaaB$	使用产生式 $\scriptstyle C \to aB$
	$ \scriptstyle\Rightarrow aaab$	使用产生式 $\scriptstyle B \to b$
	$\scriptstyle \Rightarrow aaac$	使用产生式 $\scriptstyle C \to c$

文法G_D可产生的语言为: $\{ {a^n}b|n \ge 1\} \cup \{ {a^n}c|n \ge 1\} $ ; 可接受或识别上述语言的有限状态机DeltaState如图4.

图 4 Delta协议有限自动状态机

表 1 Delta对应的自动机转移状态DeltaState

有限自动状态机DeltaState初始进入状态 ${P_0}$ , ${P_0}$ 状态获取Notification文件并对其进行验证, 根据验证结果进行状态转移: 若验证结果为0, 则重复自身状态, 重新获取Notification文件并验证; 若验证结果为1, 则转移至协议状态 ${P_1}$ ; 若验证结果为2, 则转移至协议状态 ${P_2}$ . ${P_1}$ 状态, 获取Snapshot文件并验证, 根据验证结果进行状态转移: 若验证结果为0, 该Snapshot文件被拒绝, 转移至协议状态 ${P_0}$ ; 若验证结果为1, 则转移至协议状态 ${P_{{b}}}$ . ${P_2}$ 状态, 获取Delta文件并构建DeltaFL文件链表, 进行验证, 根据验证结果进行状态转移: 若验证结果为0, 则转移至协议状态 ${P_1}$ ; 若验证结果为2, 则转移至自身继续完成DeltaFL文件链表的构建; 若验证结果为1, 则转移至协议状态 ${P_{{c}}}$ ; 协议状态 ${P_{{b}}}$ 和协议状态 ${P_{{c}}}$ 均为可接受状态, ${P_{{b}}}$ 协议状态表示Snapshot文件通过验证且被执行, ${P_{{c}}}$ 协议状态则表示DeltaFL文件链表构建完成且被执行.

(2) Delta协议模型的Promela描述

SPIN需要接受由Promela语言进行描述的协议或系统模型, 并对其进行转化和验证. Promela语言是一种用来描述并发系统(concurrent systems)的模型语言(modelling language), 可以使用Promela语言模拟和创建进程, 表述变量, 通过进程间信息传输等对模型进行描述^[13]. 使用Promela语言对Delta协议进行如下描述.

Delta协议的Promela描述
1.	chan notifFile=[1]of{byte};	/定义全局消息通道/
…
2.	chan deltaData=[1]of{byte};
3.	active proctype Library(){	/Library进程, 模拟文件生成/
4.	byte nF=1, sF=1, sD=1, dF=1, dD=1;
5.	byte rubbish;
6.	do
7.	::notifFile!nF
…
8.	::deltaData!dD
9.	od}
10.	active proctype RP(){	/RP进程变量定义和状态转移/
11.	byte getNoti;
…
12.	byte deltaState;
13.	do
14.	::notifFile?getNoti;
15.	::(getNoti==0)->goto continue
16.	if
17.	fi
18.	::(notiState==0)->goto refuse
…
19.	::(notiState==2)->goto proDelta
20.	proSnapsh:	/RP进程中的Snapshot处理状态/
…
21.	::snapshFile?getSnapsh;
22.	::(getSnapsh==0)->goto continue
23.	if
…
24.	fi
25.	::(snapshState==0)->goto refuse
26.	progress1: snapshData?getSnapshData
27.	::(getSnapshData==0)->goto continue
28.	goto continue
29.	proDelta:	/RP进程中的Delta处理状态/
…
30.	::deltaFile?getDelta;
31.	::(getDelta==0)->goto continue
32.	if
…
33.	fi
34.	::(deltaState==0)->goto refuse
35.	progress2:deltaData?getDeltaData
36.	::(getDeltaData==0)->goto continue
37.	goto continue
…		/RP进程中出错或循环转移状态/
38.	refuse:
…
39.	continue:
…
40.	od}

图5为Promela模型中各进程间信息传递过程及状态转移图. 在Promela模型中, 构建了两个进程proctype_Library和proctype_RP分别用以模拟Delta协议中RPKI资料库端和RP依赖方的运行状态. proctype_Library进程对控制文件的生成和数据打包进行了模拟, 此进程为循环进程, 若产生文件生成或数据打包失败则循环, 生成的文件和数据都将被公用全局通道变量notifFile、snapshFile、snapshData、deltaFile、deltaData负载以供proctype_RP进程获取. proctype_RP为Delta主要的协议逻辑模拟进程, 表2中为进程中变量与之对应的模拟状态和模型中取值.

表 2 Delta协议模型进程内变量

proctype_RP进程中主要的循环逻辑在do…od循环体中, 表 2中的状态变量则由if…fi结构内的语句进行随机的数值变换, 以表述文件验证或数据获取的成功与否, 根据状态数据表述的结果在逻辑处理之间使用goto语句进行跳转, 主要的三个处理逻辑部分分别为主循环体中的Notification文件处理逻辑、Snapshot文件处理逻辑proSnapsh和Delta文件处理逻辑proDelta. 同时在Promela模型中标注了下述语句: ::(1)->progress1: snapshData?getSnapshData和::(1)->progress2:deltaData?getDeltaData分别使用模型标记关键字progress用于指示SPIN在验证过程不允许出现从不执行语句snapshData?getSnapshData和deltaData?getDeltaData的循环发生, 因为此两条语句所表示的模型意义分别是从proctype_Library进程获取Snapshot数据和Delta数据, 为该验证模型必须可达的“可接受”状态.

(3) Delta协议模型的SPIN验证

图6所示是由Promela模型生成的Delta协议逻辑自动机, 其本质与图4自动机相同, 只不过在Promela描述中加入了循环用转移状态, 所以略有差异.

图 5 Delta协议Promela模型

图 6 Promela模型生成的自动机

图7为使用SPIN对Delta协议的Promela模型进行验证的结果, 验证结果表示Delta协议不存在“死锁”、“无效循环”等不安全协议特性, 同时其协议逻辑完全可达.

图8为Promela模型的模拟运行, 共进行10 000步模拟运行, 无任何报错, 协议稳定性较高.

图 7 Promela模型验证结果

通过上述验证过程, 可以从逻辑层面非常严密地证明: Delta协议不存在“死锁”、“无效循环”等不安全协议特性, 同时其协议逻辑完全可达, 具有非常高的协议安全性. 通过模拟运行则可以体现出其具备极高的稳定性.

图 8 Promela模型模拟运行

3 Delta协议实现

Promela构建的协议模型不仅可以对协议验证进行模拟, 同时由于具备完整的协议结构, 也可以在协议的实现中进行指导. 本文基于Delta的Promela模型, 使用Python对Delta协议进行了实现开发. 截止本文撰写, 该Delta功能为国内首次实现, 源码已呈现于GitHub供开源使用https://github.com/sihaolin/RPKI-Delta-Protocol. 表3为该协议实现的各主要功能函数, 可以从逻辑上完整搭建Delta协议的工程架构, 望能对其他有需求的开发者提供参考和帮助.

4 总结

通过上文阐述, 可以看出Delta协议具有较高协议安全特性, 且其协议逻辑稳定. 相较于RPKI体系中早期使用的Rsync同步工具, Delta协议的同步可控性得到大幅提升, 增量更新的方式也使得其更新效率大幅提高, 严密的控制文件格式验证和HTTPS协议对传输数据的加密也使得数据同步的安全性得到保障, Delta协议对资料库服务器更少的资源占用则使得服务器在遭受DDOS攻击时具有更高的抵御力. Delta协议已经较为成熟, 且具备RPKI体系所需的优秀特性, 在未来一段时间内将会完全替代Rsync, 成为组成RPKI体系的重要组件.

表 3 Delta实现的主要功能函数

参考文献

[1]	马迪, 沈烁. 基于本地信任锚点管理的RPKI安全运行机制研究. 电信科学, 2013, 29(9): 55-59. DOI:10.3969/j.issn.1000-0801.2013.09.010
[2]	贾佳, 延志伟, 耿光刚, 等. BGP路由泄露研究. 网络与信息安全学报, 2016, 2(8): 54-61.
[3]	Ballani H, Francis P, Zhang XY. A study of prefix hijacking and interception in the internet. Proceedings of the 2007 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications. Kyoto, Japan. 2007. 265–276.
[4]	许圣明, 马迪, 毛伟, 等. 基于有序哈希树的RPKI资料库数据同步方法. 计算机系统应用, 2016, 25(6): 141-146. DOI:10.15888/j.cnki.csa.005203
[5]	刘晓伟, 延志伟, 耿光刚, 等. RPKI中CA资源分配风险及防护技术. 计算机系统应用, 2016, 25(8): 16-22. DOI:10.15888/j.cnki.csa.005313
[6]	王娜, 杜学绘, 王文娟, 等. 边界网关协议安全研究综述. 计算机学报, 2017, 40(7): 1626-1648.
[7]	肖美华, 薛锦云. 基于SPIN/Promela的并发系统验证. 计算机科学, 2004, 31(8): 201-203, 208. DOI:10.3969/j.issn.1002-137X.2004.08.059
[8]	韩德帅, 杨启亮, 邢建春. 一种软件自适应UML建模及其形式化验证方法. 软件学报, 2015, 26(4): 730-746. DOI:10.13328/j.cnki.jos.004758
[9]	郭伟, 缪力, 张大方, 等. 基于Spin的UML状态图模型检查的设计与实现. 计算机工程与应用, 2008, 44(10): 43-47. DOI:10.3778/j.issn.1002-8331.2008.10.013
[10]	Yang QL, Lv J, Tao XP, et al. Fuzzy self-adaptation of mission-critical software under uncertainty. Journal of Computer Science and Technology, 2013, 28(1): 165-187. DOI:10.1007/s11390-013-1321-9
[11]	Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295. DOI:10.1109/32.588521
[12]	Yang WH, Xu C, Liu YP, et al. Verifying self-adaptive applications suffering uncertainty. Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. Vasteras, Sweden. 2014. 199–210.
[13]	Huston G, Michaelson G. RFC 6483 - Validation of route origination using the resource certificate Public Key Infrastructure (PKI) and Route Origin Authorizations (ROAs). BMC Public Health, 2012, 11(1): 1-6.