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實現的主要功能函數