RPKI增量同步Delta協(xié)議的形式化檢測與實(shí)現(xiàn)①

司昊林,馬 迪,毛 偉,,王 偉,邵 晴

1(中國科學(xué)院 計(jì)算機(jī)網(wǎng)絡(luò)信息中心,北京 100190)

2(中國科學(xué)院大學(xué),北京 100049)

3(互聯(lián)網(wǎng)域名系統(tǒng)北京市工程研究中心,北京 100190)

1 RPKI原理簡介

為了解決BGP路由劫持的網(wǎng)絡(luò)安全隱患,互聯(lián)網(wǎng)工程任務(wù)組IETF (Internet Engineering Task Force)提出了RPKI (Resource Public Key Infrastructure)[1].RPKI解決此類隱患的基本思路是: 構(gòu)建一整套公鑰證書體系PKI (Public Key Infrastructure)對互聯(lián)網(wǎng)碼號資源INR (Internet Number Resource),包括IP地址前綴和AS號的所有權(quán)(分配)和使用權(quán)(路由起源通告)進(jìn)行驗(yàn)證,通過驗(yàn)證的結(jié)果指示邊境路由器是否接受收到的路由起源通告以修改自己的路由信息.

如圖1所示的RPKI體系結(jié)構(gòu)中,頂級CA (Certificate Authority)如IANA、RIR、NIR、ISP等在資源分配的過程中,使用CA證書簽發(fā)一系列用于標(biāo)識資源所屬關(guān)系的認(rèn)證證書,其中EE證書主要用于對路由源授權(quán)(Route Origin Authorization,ROA)進(jìn)行驗(yàn)證,從而確認(rèn)某AS是否可以發(fā)起ASN與地址段相匹配的合法路由起源通告.該體系結(jié)構(gòu)中的RP (Relying Party)將從資料庫同步到的證書構(gòu)建成數(shù)據(jù)鏈表,使用OpenSSL對其進(jìn)行驗(yàn)證,驗(yàn)證的結(jié)果緩存于本地?cái)?shù)據(jù)庫中,再通過RTR (Relying party To Router)協(xié)議向路由器提供查詢,邊界路由器通過向RP服務(wù)器發(fā)起查詢以確認(rèn)自身收到的路由源通告是否合法,從而過濾由錯(cuò)誤配置或惡意攻擊等生成的非法路由起源通告,避免路由劫持的發(fā)生[2,3].

圖1 RPKI體系架構(gòu)

2 Delta協(xié)議

2.1 Delta協(xié)議簡介

由于Rsync在一般文件的同步過程中表現(xiàn)優(yōu)異,IETF在RPKI提出初期,建議使用Rsync作為RP和資料庫之間的同步工具[4].但由于RPKI數(shù)據(jù)資料的結(jié)構(gòu)特殊性,使用Rsync進(jìn)行數(shù)據(jù)會(huì)存在明顯缺陷和安全隱患[5].

為了解決RPKI在使用Rsync過程中存在的缺陷和隱患,IETF在2015年2月發(fā)布了RRDP (RPKI Repository Delta Protocol,簡稱 Delta 協(xié)議)草案.經(jīng)過10個(gè)版本的修訂,最終于2017年7月形成標(biāo)準(zhǔn)協(xié)議RFC 8182[6].

相較于Rsync,Delta協(xié)議具有以下顯著特征:

(1) RPKI資料庫需要生成三個(gè)文件: 用以發(fā)布更新信息的Notification更新通告文件、用以發(fā)布大塊證書打包數(shù)據(jù)的Snapshot快照文件和用以實(shí)現(xiàn)增量同步的Delta文件,通過上述文件對同步過程的動(dòng)態(tài)協(xié)調(diào),使RP服務(wù)器和RPKI資料庫之間數(shù)據(jù)同步的可控性大幅提升.

(2) Delta協(xié)議的同步機(jī)制中,RPKI資料庫針對證書文件的數(shù)據(jù)特性,通過Delta文件實(shí)現(xiàn)對文件的精確增量更新,RP服務(wù)器初次運(yùn)行需執(zhí)行Snapshot快照文件外,后續(xù)的增量更新只涉及微量數(shù)據(jù),迅捷高效.

(3) Delta協(xié)議將資料庫的證書同步過程與其他功能模塊徹底剝離,這使得RP服務(wù)器的驗(yàn)證模塊可以從本地直接檢索構(gòu)建驗(yàn)證鏈所需的證書數(shù)據(jù),驗(yàn)證效率被大幅提升.此外,同步至RP服務(wù)器的各類證書數(shù)據(jù)亦可以結(jié)合其他運(yùn)行數(shù)據(jù)進(jìn)行信息分析和挖掘,對邊界路由器提供與指導(dǎo)路由相關(guān)的增值服務(wù).

(4) Delta協(xié)議中,嚴(yán)格的控制文件校驗(yàn)和全方位的安全考量,使得RPKI與RP服務(wù)器之間數(shù)據(jù)同步的安全性得到大幅提升,同時(shí)RPKI資料庫和RP服務(wù)器之間的控制文件分發(fā)采用HTTPS (Hyper Text Transfer Protocol over Secure socket layer)協(xié)議,由于對傳輸數(shù)據(jù)進(jìn)行了加密,可以有效防止中間人(Monkey-In-the-Middle)攻擊,提升協(xié)議安全性[7].

2.2 Delta協(xié)議工作機(jī)制

圖2用以說明Delta協(xié)議的工作機(jī)制.

Delta協(xié)議工作機(jī)制1) RPKI資料庫需以時(shí)間t為周期,循環(huán)生成Notification文件、Snapshot文件和Delta文件并對其進(jìn)行維護(hù),這三種文件都由當(dāng)前的Session_ID屬性和文件Serial號碼唯一標(biāo)識,并以URL方式發(fā)布以供遠(yuǎn)程獲取,Session_ID本身為一個(gè)隨機(jī)版本4的通用統(tǒng)一標(biāo)識符UUID (Universally Unique Identifier),用以對各個(gè)文件進(jìn)行唯一性標(biāo)識.Notification文件用于對RP服務(wù)器發(fā)布更新會(huì)話發(fā)起通告,文件內(nèi)容包括當(dāng)前Delta版本屬性、本次會(huì)話組合標(biāo)識屬性和,同時(shí)也包括本次會(huì)話相關(guān)的Snapshot和Delta文件信息.資料庫生成的三個(gè)文件均為.xml文件.2) RP服務(wù)器周期性獲取Notification文件,并對其內(nèi)容進(jìn)行解析.各RP服務(wù)器可根據(jù)自身工具差異,選取合適的方式對文件進(jìn)行解析以獲取文件信息,本文中采用Python2.7的xml.etree.ElementTree模塊對.xml文件進(jìn)行解析,并對文件數(shù)據(jù)構(gòu)樹以備后續(xù)使用.

3) RP服務(wù)器需對Notification文件格式進(jìn)行驗(yàn)證.Delta協(xié)議對資料庫生成的三種文件均進(jìn)行了嚴(yán)格的格式規(guī)范,若有任何格式細(xì)節(jié)不匹配的文件,都必須在Delta協(xié)議執(zhí)行的流程中被拒絕.4) Notification文件中攜帶的屬性值必須為“1”,標(biāo)識當(dāng)前Delta協(xié)議版本號.5) Notification文件中攜帶的屬性值需要和本地已存的“Serial”變量進(jìn)行比較,通常若RP服務(wù)器初次發(fā)起更新會(huì)話,“Serial”變量的值為初始值,此時(shí)需要直接執(zhí)行Snapshot文件,至步驟6),若屬性值大于本地“Serial”變量值,則進(jìn)行Delta增量更新,至步驟8),若“Serial”變量值為非初始值且大于等于屬性值,則該Notification文件被拒絕,至步驟11).6) RP服務(wù)器通過Notification文件中Snapshot文件的URL獲取Snapshot文件并驗(yàn)證其文件格式和HASH值,Snapshot文件的HASH值負(fù)載于Notification文件中,Delta協(xié)議中的文件HASH值均為SHA-256散列的十六進(jìn)制編碼.還需驗(yàn)證Snapshot文件的和屬性值是否與Notification匹配,若上述三步驗(yàn)證中的任何一個(gè)驗(yàn)證失敗,將導(dǎo)致此Snapshot文件被拒絕,至步驟11).7) 執(zhí)行Snapshot文件,獲取證書數(shù)據(jù),至步驟11).8) 通常一個(gè)Notification文件會(huì)包含多個(gè)Delta文件信息,需要對多個(gè)Delta文件依照屬性值增序構(gòu)建文件鏈表DeltaFL,并對DeltaFL依次驗(yàn)證和執(zhí)行.9) 驗(yàn)證Delta文件的文件格式、文件HASH值和、屬性值,任何一步驗(yàn)證失敗都將導(dǎo)致此Delta文件被拒絕,并執(zhí)行Snapshot文件,至步驟6).10) 執(zhí)行Delta文件,獲取證書數(shù)據(jù),若DeltaFL為空,至步驟11),若不為空,則至步驟8).11) 周期循環(huán),至步驟2).

2.3 Delta協(xié)議的形式化檢測

Delta協(xié)議的各文件驗(yàn)證過程層疊環(huán)扣,邏輯較為復(fù)雜,為了準(zhǔn)確且全面地說明Delta協(xié)議及其實(shí)現(xiàn)程序的協(xié)議正確性(協(xié)議正確性通常指: 不存在違背斷言(assertion)的情況、不存在不可達(dá)(unreachable)狀態(tài)、不存在死鎖(deadlock)、可以完全覆蓋定義的LTL (Linear Temporal Logic)公式等安全特性)[8],下文將借助用來驗(yàn)證協(xié)議或系統(tǒng)邏輯一致性的工具SPIN對Delta協(xié)議進(jìn)行形式化檢測,以說明Delta具備較高的安全特性.

圖2 Delta協(xié)議工作機(jī)制示意圖

算法1.形式化檢測算法1) 構(gòu)造自動(dòng)機(jī),其對應(yīng)公式;2) 計(jì)算使得;3) 判定是否為空,也就是不接受任何輸入.

SPIN (Simple Promela Interpreter)是一款適合進(jìn)行協(xié)議一致性檢查的分析檢測工具,由貝爾實(shí)驗(yàn)室的形式化方法與驗(yàn)證小組開發(fā),SPIN優(yōu)秀的算法設(shè)計(jì)和有效的檢測能力使其榮獲由ACM (Association for Computing Machinery)授予的軟件系統(tǒng)獎(jiǎng)(software systems award),其他獲得此殊榮的還有Unix、TCP/IP、Tcl/Tk、Java、WWW等[10].如圖3所示的SPIN驗(yàn)證流程,SPIN可以接受由Promela建模語言構(gòu)筑的協(xié)議或系統(tǒng)模型,模型通常由消息通道、變量和進(jìn)程進(jìn)行描述.SPIN會(huì)將模型中構(gòu)筑的進(jìn)程翻譯為有限自動(dòng)機(jī),并對這些自動(dòng)機(jī)進(jìn)行異步積運(yùn)算得到優(yōu)先自動(dòng)機(jī)A,同時(shí)LTL公式會(huì)被取反轉(zhuǎn)換為自動(dòng)機(jī)B,再將自動(dòng)機(jī)A和B進(jìn)行同步積運(yùn)算得到自動(dòng)機(jī)C,SPIN將使用內(nèi)嵌的搜索算法對C進(jìn)行窮盡搜索[11],搜索過程可以通過SPIN獨(dú)有的On-the-fly技術(shù)以及偏序簡化技術(shù)對狀態(tài)空間進(jìn)行簡化,搜索完畢的自動(dòng)機(jī)C若其接受的語言為空,則表示系統(tǒng)滿足LTL描述的屬性,反之則不滿足[12].

圖3 SPIN模擬與驗(yàn)證結(jié)構(gòu)流程圖

(1) Delta協(xié)議的語言和有限狀態(tài)機(jī)描述

定義一個(gè)四元組文法G:G=(V，T，P，S),其中,V是變量集合叫做一個(gè)語法變量;T是終極符的集合,T中的字符是語言的句子中出現(xiàn)的字符,P是產(chǎn)生式的集合,P中的元素具有形式文法G的開始符號.

因此,Delta協(xié)議的驗(yàn)證邏輯可以使用此語法G進(jìn)行表述:

S ?aAS→aA使用產(chǎn)生式?aaA 使用產(chǎn)生式?aaaB A→aA使用產(chǎn)生式?aaaaA A→aB使用產(chǎn)生式?aaaaB B→aA使用產(chǎn)生式?aaaab A→aB使用產(chǎn)生式S ?aA B→b S→aA使用產(chǎn)生式?aaaC使用產(chǎn)生式?aaCA→aC使用產(chǎn)生式?aaaB C→aC使用產(chǎn)生式?aaab C→aB使用產(chǎn)生式?aaac B→b使用產(chǎn)生式C→c

文法GD可產(chǎn)生的語言為可接受或識別上述語言的有限狀態(tài)機(jī)DeltaState如圖4.

圖4 Delta協(xié)議有限自動(dòng)狀態(tài)機(jī)

表1 Delta對應(yīng)的自動(dòng)機(jī)轉(zhuǎn)移狀態(tài)DeltaState

(2) Delta協(xié)議模型的Promela描述

SPIN需要接受由Promela語言進(jìn)行描述的協(xié)議或系統(tǒng)模型,并對其進(jìn)行轉(zhuǎn)化和驗(yàn)證.Promela語言是一種用來描述并發(fā)系統(tǒng)(concurrent systems)的模型語言(modelling language),可以使用Promela語言模擬和創(chuàng)建進(jìn)程,表述變量,通過進(jìn)程間信息傳輸?shù)葘δＰ瓦M(jìn)行描述[13].使用Promela語言對Delta協(xié)議進(jìn)行如下描述.

Delta協(xié)議的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進(jìn)程,模擬文件生成*/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進(jìn)程變量定義和狀態(tài)轉(zhuǎn)移*/…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進(jìn)程中的Snapshot處理狀態(tài)*/…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進(jìn)程中的Delta處理狀態(tài)*/38.refuse:…39.continue:/*RP進(jìn)程中出錯(cuò)或循環(huán)轉(zhuǎn)移狀態(tài)*/…40.od}

圖5為Promela模型中各進(jìn)程間信息傳遞過程及狀態(tài)轉(zhuǎn)移圖.在Promela模型中,構(gòu)建了兩個(gè)進(jìn)程proctype_Library和proctype_RP分別用以模擬Delta協(xié)議中RPKI資料庫端和RP依賴方的運(yùn)行狀態(tài).proctype_Library進(jìn)程對控制文件的生成和數(shù)據(jù)打包進(jìn)行了模擬,此進(jìn)程為循環(huán)進(jìn)程,若產(chǎn)生文件生成或數(shù)據(jù)打包失敗則循環(huán),生成的文件和數(shù)據(jù)都將被公用全局通道變量notifFile、snapshFile、snapshData、deltaFile、deltaData負(fù)載以供proctype_RP進(jìn)程獲取.proctype_RP為Delta主要的協(xié)議邏輯模擬進(jìn)程,表2中為進(jìn)程中變量與之對應(yīng)的模擬狀態(tài)和模型中取值.

表2 Delta協(xié)議模型進(jìn)程內(nèi)變量

proctype_RP進(jìn)程中主要的循環(huán)邏輯在do…od循環(huán)體中,表 2中的狀態(tài)變量則由if…fi結(jié)構(gòu)內(nèi)的語句進(jìn)行隨機(jī)的數(shù)值變換,以表述文件驗(yàn)證或數(shù)據(jù)獲取的成功與否,根據(jù)狀態(tài)數(shù)據(jù)表述的結(jié)果在邏輯處理之間使用goto語句進(jìn)行跳轉(zhuǎn),主要的三個(gè)處理邏輯部分分別為主循環(huán)體中的Notification文件處理邏輯、Snapshot文件處理邏輯proSnapsh和Delta文件處理邏輯proDelta.同時(shí)在Promela模型中標(biāo)注了下述語句:::(1)->progress1: snapshData?getSnapshData和::(1)->progress2:deltaData?getDeltaData分別使用模型標(biāo)記關(guān)鍵字progress用于指示SPIN在驗(yàn)證過程不允許出現(xiàn)從不執(zhí)行語句snapshData?getSnapshData和deltaData?getDeltaData的循環(huán)發(fā)生,因?yàn)榇藘蓷l語句所表示的模型意義分別是從proctype_Library進(jìn)程獲取Snapshot數(shù)據(jù)和Delta數(shù)據(jù),為該驗(yàn)證模型必須可達(dá)的“可接受”狀態(tài).

(3) Delta協(xié)議模型的SPIN驗(yàn)證

圖6所示是由Promela模型生成的Delta協(xié)議邏輯自動(dòng)機(jī),其本質(zhì)與圖4自動(dòng)機(jī)相同,只不過在Promela描述中加入了循環(huán)用轉(zhuǎn)移狀態(tài),所以略有差異.

圖5 Delta協(xié)議Promela模型

圖6 Promela模型生成的自動(dòng)機(jī)

圖7為使用SPIN對Delta協(xié)議的Promela模型進(jìn)行驗(yàn)證的結(jié)果,驗(yàn)證結(jié)果表示Delta協(xié)議不存在“死鎖”、“無效循環(huán)”等不安全協(xié)議特性,同時(shí)其協(xié)議邏輯完全可達(dá).

圖7 Promela模型驗(yàn)證結(jié)果

圖8為Promela模型的模擬運(yùn)行,共進(jìn)行10 000步模擬運(yùn)行,無任何報(bào)錯(cuò),協(xié)議穩(wěn)定性較高.

通過上述驗(yàn)證過程,可以從邏輯層面非常嚴(yán)密地證明: Delta協(xié)議不存在“死鎖”、“無效循環(huán)”等不安全協(xié)議特性,同時(shí)其協(xié)議邏輯完全可達(dá),具有非常高的協(xié)議安全性.通過模擬運(yùn)行則可以體現(xiàn)出其具備極高的穩(wěn)定性.

圖8 Promela模型模擬運(yùn)行

3 Delta協(xié)議實(shí)現(xiàn)

Promela構(gòu)建的協(xié)議模型不僅可以對協(xié)議驗(yàn)證進(jìn)行模擬,同時(shí)由于具備完整的協(xié)議結(jié)構(gòu),也可以在協(xié)議的實(shí)現(xiàn)中進(jìn)行指導(dǎo).本文基于Delta的Promela模型,使用Python對Delta協(xié)議進(jìn)行了實(shí)現(xiàn)開發(fā).截止本文撰寫,該Delta功能為國內(nèi)首次實(shí)現(xiàn),源碼已呈現(xiàn)于GitHub供開源使用https://github.com/sihaolin/RPKIDelta-Protocol.表3為該協(xié)議實(shí)現(xiàn)的各主要功能函數(shù),可以從邏輯上完整搭建Delta協(xié)議的工程架構(gòu),望能對其他有需求的開發(fā)者提供參考和幫助.

4 總結(jié)

通過上文闡述,可以看出Delta協(xié)議具有較高協(xié)議安全特性,且其協(xié)議邏輯穩(wěn)定.相較于RPKI體系中早期使用的Rsync同步工具,Delta協(xié)議的同步可控性得到大幅提升,增量更新的方式也使得其更新效率大幅提高,嚴(yán)密的控制文件格式驗(yàn)證和HTTPS協(xié)議對傳輸數(shù)據(jù)的加密也使得數(shù)據(jù)同步的安全性得到保障,Delta協(xié)議對資料庫服務(wù)器更少的資源占用則使得服務(wù)器在遭受DDOS攻擊時(shí)具有更高的抵御力.Delta協(xié)議已經(jīng)較為成熟,且具備RPKI體系所需的優(yōu)秀特性,在未來一段時(shí)間內(nèi)將會(huì)完全替代Rsync,成為組成RPKI體系的重要組件.

表3 Delta實(shí)現(xiàn)的主要功能函數(shù)