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

司昊林,马 迪,毛 伟,,王 伟,邵 晴

1(中国科学院 计算机网络信息中心,北京 100190)

2(中国科学院大学,北京 100049)

3(互联网域名系统北京市工程研究中心,北京 100190)

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 (Certificate 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版本属性、本次会话组合标识属性和,同时也包括本次会话相关的Snapshot和Delta文件信息.资料库生成的三个文件均为.xml文件.2) RP服务器周期性获取Notification文件,并对其内容进行解析.各RP服务器可根据自身工具差异,选取合适的方式对文件进行解析以获取文件信息,本文中采用Python2.7的xml.etree.ElementTree模块对.xml文件进行解析,并对文件数据构树以备后续使用.

3) RP服务器需对Notification文件格式进行验证.Delta协议对资料库生成的三种文件均进行了严格的格式规范,若有任何格式细节不匹配的文件,都必须在Delta协议执行的流程中被拒绝.4) Notification文件中携带的属性值必须为“1”,标识当前Delta协议版本号.5) Notification文件中携带的属性值需要和本地已存的“Serial”变量进行比较,通常若RP服务器初次发起更新会话,“Serial”变量的值为初始值,此时需要直接执行Snapshot文件,至步骤6),若属性值大于本地“Serial”变量值,则进行Delta增量更新,至步骤8),若“Serial”变量值为非初始值且大于等于属性值,则该Notification文件被拒绝,至步骤11).6) RP服务器通过Notification文件中Snapshot文件的URL获取Snapshot文件并验证其文件格式和HASH值,Snapshot文件的HASH值负载于Notification文件中,Delta协议中的文件HASH值均为SHA-256散列的十六进制编码.还需验证Snapshot文件的和属性值是否与Notification匹配,若上述三步验证中的任何一个验证失败,将导致此Snapshot文件被拒绝,至步骤11).7) 执行Snapshot文件,获取证书数据,至步骤11).8) 通常一个Notification文件会包含多个Delta文件信息,需要对多个Delta文件依照属性值增序构建文件链表DeltaFL,并对DeltaFL依次验证和执行.9) 验证Delta文件的文件格式、文件HASH值和、属性值,任何一步验证失败都将导致此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具备较高的安全特性.

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

算法1.形式化检测算法1) 构造自动机,其对应公式;2) 计算使得;3) 判定是否为空,也就是不接受任何输入.

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是变量集合叫做一个语法变量;T是终极符的集合,T中的字符是语言的句子中出现的字符,P是产生式的集合,P中的元素具有形式文法G的开始符号.

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

S ⇒aAS→aA使用产生式⇒aaA 使用产生式⇒aaaB A→aA使用产生式⇒aaaaA A→aB使用产生式⇒aaaaB B→aA使用产生式⇒aaaab A→aB使用产生式S ⇒aA B→b S→aA使用产生式⇒aaaC使用产生式⇒aaCA→aC使用产生式⇒aaaB C→aC使用产生式⇒aaab C→aB使用产生式⇒aaac B→b使用产生式C→c

文法GD可产生的语言为可接受或识别上述语言的有限状态机DeltaState如图4.

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

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

(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(){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(){/*Library进程,模拟文件生成*/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进程变量定义和状态转移*/…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进程中的Snapshot处理状态*/…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进程中的Delta处理状态*/38.refuse:…39.continue:/*RP进程中出错或循环转移状态*/…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协议不存在“死锁”、“无效循环”等不安全协议特性,同时其协议逻辑完全可达.

图7 Promela模型验证结果

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

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

图8 Promela模型模拟运行

3 Delta协议实现

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

4 总结

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

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