申瑩珠 , 顧純祥,2 , 陳 熹 , 張協(xié)力 , 盧政宇

1(信息工程大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院,河南 鄭州 450001)

2(河南省網(wǎng)絡(luò)密碼技術(shù)重點(diǎn)實(shí)驗(yàn)室,河南 鄭州 450001)

近年來,網(wǎng)絡(luò)安全協(xié)議相關(guān)應(yīng)用的安全性問題越來越受到重視.2014年,開源加密庫(kù)OpenSSL的重大安全漏洞“心臟出血”(CVE-2014-0160)引起了業(yè)界廣泛關(guān)注,攻擊者可以從服務(wù)器內(nèi)存中讀取包括用戶名、密碼和信用卡號(hào)等隱私信息在內(nèi)的數(shù)據(jù),影響波及大量互聯(lián)網(wǎng)公司.2016年,OpenSSL高危漏洞“DROWN”(CVE-2016-0800)以及2017年的OpenSSL拒絕服務(wù)漏洞(CVE-2017-3731)也同樣為網(wǎng)絡(luò)協(xié)議的安全性敲響了警鐘.因此,如何對(duì)網(wǎng)絡(luò)安全協(xié)議的安全性進(jìn)行評(píng)估、盡快盡早發(fā)現(xiàn)其協(xié)議實(shí)現(xiàn)中的脆弱點(diǎn),保護(hù)用戶隱私數(shù)據(jù)安全可靠就顯得格外重要.OpenVPN是一款基于OpenSSL庫(kù)的應(yīng)用層虛擬專用通道(VPN),在TLS之上建立安全的數(shù)據(jù)傳輸隧道,實(shí)現(xiàn)身份認(rèn)證、數(shù)據(jù)加密、完整性保護(hù)和訪問控制.OpenVPN在真實(shí)網(wǎng)絡(luò)中被廣泛部署且常應(yīng)用于大型企業(yè)之中,對(duì)其進(jìn)行脆弱性分析有著重要的現(xiàn)實(shí)意義.

協(xié)議脆弱性分析檢測(cè)技術(shù)也叫協(xié)議漏洞挖掘技術(shù).傳統(tǒng)的漏洞挖掘技術(shù)主要依賴于安全人員的人工分析與測(cè)試,而模糊測(cè)試技術(shù)簡(jiǎn)單、有效、自動(dòng)化程度比較高,是目前進(jìn)行安全測(cè)試最有效的方法,被廣泛應(yīng)用于Web、系統(tǒng)、應(yīng)用程序的漏洞挖掘.由于它一般屬于黑盒測(cè)試,通過構(gòu)造有效的畸形數(shù)據(jù)進(jìn)行測(cè)試,因此該技術(shù)的代碼覆蓋率相對(duì)較低.2015年,Gascon等人[1]提出了可對(duì)私有協(xié)議進(jìn)行態(tài)式黑盒模糊測(cè)試的PULSAR系統(tǒng),通過將模糊測(cè)試與協(xié)議逆向、模擬自動(dòng)化執(zhí)行技術(shù)結(jié)合,提高了協(xié)議狀態(tài)探索空間,能夠挖掘協(xié)議實(shí)現(xiàn)中的深層漏洞;2016年,Ma等人[2]優(yōu)化測(cè)試數(shù)據(jù)生成方法,提出了使用基于規(guī)則的狀態(tài)機(jī)和狀態(tài)規(guī)則樹來生成模糊測(cè)試的數(shù)據(jù),與傳統(tǒng)模糊測(cè)試方法相比,使用更少的測(cè)試數(shù)據(jù)找到脆弱點(diǎn),提高了測(cè)試效率;2017年,Kang等人[3]提出了一種結(jié)合靜態(tài)分析和動(dòng)態(tài)分析的智能模糊測(cè)試系統(tǒng),在提高檢測(cè)有效性的同時(shí),減少了誤報(bào)率和漏報(bào)率.

協(xié)議狀態(tài)機(jī)推斷是脆弱性分析非常關(guān)鍵的內(nèi)容.2015年,de Ruiter提出了通過模型學(xué)習(xí)的方法分析具體TLS實(shí)現(xiàn)的安全性[4],該方法在僅采用黑盒測(cè)試的情況下,應(yīng)用狀態(tài)機(jī)學(xué)習(xí)自動(dòng)推斷出了協(xié)議實(shí)現(xiàn)的狀態(tài)機(jī),并通過觀察推斷出來的狀態(tài)機(jī)來檢測(cè)可能由程序邏輯漏洞引起的異常行為;Beurdouche等人[5]也提出了類似的通過系統(tǒng)測(cè)試非正常TLS消息流以檢測(cè)協(xié)議實(shí)現(xiàn)中是否存在脆弱性的方法,并在測(cè)試中發(fā)現(xiàn)了新漏洞.2016年,Ruiter帶領(lǐng)團(tuán)隊(duì)在其前期工作的基礎(chǔ)上繼續(xù)進(jìn)行了許多相關(guān)研究:Ruiter進(jìn)一步對(duì)過去 14年以來的OpenSSL以及LibreSSL的具體實(shí)現(xiàn)進(jìn)行了并行自動(dòng)化協(xié)議狀態(tài)模糊測(cè)試,通過自動(dòng)化學(xué)習(xí),為145個(gè)不同版本的服務(wù)器端和客戶端構(gòu)建了狀態(tài)機(jī),并分析相關(guān)實(shí)現(xiàn)的安全性[6];Verleg則針對(duì)OpenSSH推斷出了6個(gè)SSH服務(wù)器的狀態(tài)機(jī),驗(yàn)證了協(xié)議狀態(tài)機(jī)推斷方法的通用性和可行性[7].同年,Somorovsky提出了基于已知漏洞專家?guī)斓姆蛛A段模糊測(cè)試框架TLS-attacker[8],能夠提供簡(jiǎn)單接口支持定制TLS消息流,并允許任意修改消息中的內(nèi)容,從而實(shí)現(xiàn)對(duì)TLS庫(kù)安全性的評(píng)估.2017年,Ruiter團(tuán)隊(duì)的Lenaerts[9]對(duì)Verleg的方法[7]進(jìn)行了改進(jìn),將Verleg分別對(duì)SSH協(xié)議的3個(gè)子層協(xié)議進(jìn)行模型學(xué)習(xí)與檢測(cè)的方法整合為統(tǒng)一的模型學(xué)習(xí)與檢測(cè),提出了對(duì)SSH服務(wù)器模型進(jìn)行狀態(tài)安全檢測(cè)的新方法;同年,Veldhuizen針對(duì) IPSEC也進(jìn)行了協(xié)議狀態(tài)機(jī)推斷并分析[10].Novickis[11]在2016年將模型學(xué)習(xí)的方法擴(kuò)展到OpenVPN協(xié)議進(jìn)行研究分析,試圖推斷出OpenVPN系統(tǒng)的狀態(tài)機(jī),但在過程中遇到了許多困難最終并未實(shí)現(xiàn)目標(biāo).

本文基于模型學(xué)習(xí)的方法,利用協(xié)議狀態(tài)模糊測(cè)試技術(shù),對(duì)OpenVPN 2.0.9服務(wù)器端進(jìn)行了模型學(xué)習(xí)和一致性檢測(cè),自動(dòng)推演出目標(biāo)系統(tǒng)的協(xié)議實(shí)現(xiàn)狀態(tài)機(jī),并對(duì)其狀態(tài)機(jī)模型進(jìn)行化簡(jiǎn),對(duì)其實(shí)現(xiàn)邏輯及過程進(jìn)行詳細(xì)分析;提出了一種狀態(tài)機(jī)時(shí)間壓縮模型,與原始狀態(tài)機(jī)及同版本OpenSSL狀態(tài)機(jī)進(jìn)行對(duì)比分析.結(jié)果表明:利用經(jīng)化簡(jiǎn)后的模型可以更方便迅速地識(shí)別協(xié)議狀態(tài)機(jī)中正常的和特殊的狀態(tài)遷移路徑,從而提高OpenVPN脆弱性檢測(cè)與分析的效率.

1 基礎(chǔ)知識(shí)

1.1 OpenVPN協(xié)議

VPN(虛擬專用通道)是企業(yè)與企業(yè)或者個(gè)人與企業(yè)之間安全數(shù)據(jù)傳輸?shù)乃淼?提供了身份認(rèn)證、數(shù)據(jù)加密、完整性保護(hù)和訪問控制安全服務(wù).OpenVPN是一款基于OpenSSL庫(kù)的應(yīng)用層VPN實(shí)現(xiàn),由于其簡(jiǎn)單易用的特性而被廣泛部署.OpenVPN依賴OpenSSL的安全性,在客戶端和服務(wù)器端通過指定端口建立TCP/UDP(一般默認(rèn)使用UDP)安全隧道,然后在該TLS隧道中加密通信數(shù)據(jù),隧道示意如圖1所示.

· OpenVPN協(xié)議TLS模式下的實(shí)現(xiàn)

OpenVPN提供了兩種完全不同的認(rèn)證模式:TLS模式和預(yù)共享靜態(tài)密鑰(PSK)模式.預(yù)共享靜態(tài)密鑰模式使用預(yù)共享靜態(tài)密鑰認(rèn)證身份并加密.TLS模式采用使用證書的SSL/TLS協(xié)議進(jìn)行身份驗(yàn)證、建立安全隧道、交換對(duì)稱會(huì)話密鑰,并使用會(huì)話密鑰加密數(shù)據(jù)隧道.TLS模式由于能夠保證安全地分發(fā)和更新對(duì)稱密鑰,進(jìn)而在現(xiàn)實(shí)應(yīng)用中具有更強(qiáng)的安全性.因此,本文主要研究基于TLS認(rèn)證模式的OpenVPN協(xié)議.

Fig.1 OpenVPN communication tunnel圖1 OpenVPN通信隧道

OpenVPN安全通信過程如圖2所示,依賴于以下子協(xié)議.

(1) OpenVPN握手協(xié)議,類似于TCP的3次握手過程,握手?jǐn)?shù)據(jù)包包括:由客戶端發(fā)起的握手請(qǐng)求數(shù)據(jù)包P_CONTROL_HARD_RESET_CLIENT_V1/V2(V1/V2代表后續(xù)兩種不同的密鑰協(xié)商方式,分別對(duì)應(yīng)PSK認(rèn)證模式和TLS認(rèn)證模式,OpenVPN 2.0以上版本默認(rèn)使用P_CONTROL_HARD_RESET_CLIENT_V2),服務(wù)器端的請(qǐng)求響應(yīng)數(shù)據(jù)包P_CONTROL_HARD_RESET_SERVER_V1/V2(密鑰協(xié)商方式與請(qǐng)求一致),客戶端對(duì)服務(wù)器端響應(yīng)的確認(rèn)P_ACK_V1;

(2) OpenVPN控制協(xié)議,控制協(xié)議包括TLS握手和密鑰協(xié)商兩個(gè)階段,封裝在P_CONTROL_V1數(shù)據(jù)包中.當(dāng)TLS握手完成后,TLS加密隧道已建立,會(huì)話密鑰協(xié)商信息將被封裝在TLS記錄層中安全傳輸.需要時(shí),可使用P_CONTROL_SOFT_RESET_V1請(qǐng)求會(huì)話密鑰沖協(xié)商;

(3) OpenVPN記錄協(xié)議,建立安全隧道和密鑰交換完成后,雙方進(jìn)行加密數(shù)據(jù)通信P_DATA_V1.

Fig.2 OpenVPN communication process in TLS mode圖2 TLS模式下OpenVPN通信過程

OpenVPN沒有詳細(xì)的官方規(guī)范,2016年,Tomas Novickis方法[11]中給出的在TLS模式下期望的OpenVPN狀態(tài)機(jī)如圖3所示.Novickis試圖基于LearnLib得出真實(shí)的OpenVPN實(shí)現(xiàn)的狀態(tài)機(jī),但其在研究過程中主要遇到了以下困難:(1) 使用python庫(kù)Scapy可以快速構(gòu)造數(shù)據(jù)包,但僅嘗試?yán)弥癢irshark捕獲的數(shù)據(jù)包載荷進(jìn)行復(fù)用,未根據(jù)協(xié)議原理精心設(shè)計(jì)每個(gè)數(shù)據(jù)包字段,導(dǎo)致無法通過證書驗(yàn)證或HMAC校驗(yàn);(2) P_CONTROL_V1數(shù)據(jù)包載荷較多需要分塊傳輸時(shí)還存在一些問題.因此,作者得到OpenVPN實(shí)現(xiàn)狀態(tài)機(jī)的目標(biāo)并未實(shí)現(xiàn).

Fig.3 The expected OpenVPN state machine圖3 期望的OpenVPN狀態(tài)機(jī)

1.2 模型學(xué)習(xí)與一致性檢測(cè)

為了解決使用常規(guī)技術(shù)難以分析檢測(cè)安全協(xié)議的具體實(shí)現(xiàn)與協(xié)議標(biāo)準(zhǔn)之間差異性的問題,采用Angluin的MAT(minimally adequate teachers)框架[12],使用成員查詢和等價(jià)查詢進(jìn)行模型學(xué)習(xí);通過測(cè)試查詢進(jìn)行一致性測(cè)試,確保模型的推斷結(jié)果符合要求;最后,進(jìn)一步分析檢測(cè)協(xié)議實(shí)現(xiàn)是否存在脆弱點(diǎn).在MAT框架中,學(xué)習(xí)器必須通過詢問預(yù)言機(jī)來推斷目標(biāo)安全協(xié)議的狀態(tài)機(jī).圖4為MAT框架示意圖.

Fig.4 MAT framework圖4 MAT框架

基于MAT框架,模型推斷與一致性檢測(cè)系統(tǒng)可抽象為圖5所示,學(xué)習(xí)器提供了一個(gè)可以發(fā)送給測(cè)試目標(biāo)(SUT)的消息列表(輸入表)以及一條重置測(cè)試目標(biāo)到初始狀態(tài)的命令.測(cè)試程序(test harness)可以將輸入表中的抽象消息轉(zhuǎn)換為可以發(fā)送給SUT的具體消息,也可以將SUT反饋的響應(yīng)轉(zhuǎn)換為學(xué)習(xí)器可識(shí)別的抽象消息.因此,測(cè)試程序相當(dāng)于MAT框架中在學(xué)習(xí)器和預(yù)言機(jī)之間進(jìn)行翻譯轉(zhuǎn)換的映射器(mapper).而實(shí)現(xiàn)測(cè)試程序就需要我們知道目標(biāo)協(xié)議使用的具體消息集.

具體過程如下.

a.成員查詢:通過發(fā)送一系列消息和重置命令,學(xué)習(xí)器使用如最早由Angluin提出的L*算法[12]、改進(jìn)L*后去除大量冗余成員查詢的TTT算法[13]等經(jīng)典有限狀態(tài)機(jī)學(xué)習(xí)算法,通過從SUT返回的響應(yīng)推斷出狀態(tài)機(jī)模型;

b.等價(jià)查詢:采用近似等價(jià)查詢算法進(jìn)行一致性檢測(cè),如Chow提出的W-method算法[14]、Ruiter改進(jìn)的wmethod[4]等.通過有限數(shù)量的測(cè)試查詢,檢測(cè)該推斷是否與實(shí)際的狀態(tài)機(jī)等價(jià).如果不等價(jià),將會(huì)返回一個(gè)反例,學(xué)習(xí)器使用該反例重新進(jìn)行推斷,即進(jìn)行模型修正.如果沒有找到反例,則認(rèn)為當(dāng)前狀態(tài)機(jī)推斷近似等價(jià)于真實(shí)實(shí)現(xiàn),得到協(xié)議實(shí)現(xiàn)的狀態(tài)機(jī).

Fig.5 System architecture圖5 系統(tǒng)架構(gòu)

2 基于模型學(xué)習(xí)的OpenVPN狀態(tài)機(jī)推斷

本文在模型學(xué)習(xí)與一致性檢測(cè)技術(shù)的基礎(chǔ)上,基于LearnLib平臺(tái)[15,16]開發(fā)了針對(duì)OpenVPN的狀態(tài)機(jī)推斷框架,本文只考慮TLS模式下的OpenVPN狀態(tài)機(jī)推斷問題.

· 實(shí)驗(yàn)環(huán)境:Intel core i7-4790處理器、8G內(nèi)存、Ubuntu 16.04-64位系統(tǒng)、Wireshark軟件;

· 協(xié)議版本:OpenSSL 1.0.2h,OpenVPN 2.0.9;

· 編程語言:Java,Python;

· 環(huán)境配置:采用橋接模式,在兩臺(tái)虛擬機(jī)中分別配置本文系統(tǒng)與OpenVPN 2.0.9服務(wù)器端環(huán)境進(jìn)行測(cè)試.其中,OpenVPN通信采用默認(rèn)的UDP連接方式(在OpenVPN協(xié)議的可靠傳輸要求下,即使采用TCP連接,也同樣需要實(shí)現(xiàn)確認(rèn)機(jī)制).

2.1 輸入/輸出表構(gòu)造

本文主要測(cè)試OpenVPN服務(wù)器端狀態(tài)機(jī),因此根據(jù)OpenVPN協(xié)議中客戶端消息集構(gòu)造輸入表以及服務(wù)器端響應(yīng)消息集構(gòu)造輸出表,輸入/輸出表的符號(hào)表示及消息含義見表1.

Table 1 Symbol representation and message meaning in input/output table表1 輸入/輸出表符號(hào)表示及消息含義

轉(zhuǎn)換程序Test harness基于OpenVPN底層協(xié)議,對(duì)學(xué)習(xí)器的消息輸入表中的消息進(jìn)行精心構(gòu)造,按照學(xué)習(xí)器中的狀態(tài)機(jī)推斷與近似等價(jià)算法與測(cè)試目標(biāo)進(jìn)行交互,并將服務(wù)器端返回的響應(yīng)消息識(shí)別、抽象,送入學(xué)習(xí)器繼續(xù)分析推斷,直到完成真實(shí)的OpenVPN服務(wù)器端狀態(tài)機(jī)的學(xué)習(xí)與檢測(cè);通過比對(duì)協(xié)議實(shí)現(xiàn)狀態(tài)機(jī)與協(xié)議標(biāo)準(zhǔn)狀態(tài)機(jī)(或期望的狀態(tài)機(jī))之間的差異性,找到可能存在的攻擊路徑.

2.2 數(shù)據(jù)包構(gòu)造及狀態(tài)機(jī)推斷策略

網(wǎng)絡(luò)安全協(xié)議的執(zhí)行路徑中往往存在許多條件控制,這也正是限制傳統(tǒng)模糊測(cè)試進(jìn)行脆弱性分析檢測(cè)能力與效率的一個(gè)重要方面.因此在狀態(tài)模糊測(cè)試中,數(shù)據(jù)包構(gòu)造是整個(gè)測(cè)試的基礎(chǔ)[17].OpenVPN協(xié)議中只有正確的證書驗(yàn)證、HMAC校驗(yàn)等才能順利完成整個(gè)連接過程.

本文參考RFC 2246及Wireshark捕獲的OpenVPN真實(shí)通信數(shù)據(jù),精心構(gòu)造轉(zhuǎn)換程序中使用的數(shù)據(jù)包,并按照期望的路徑進(jìn)行測(cè)試,保證構(gòu)造的消息集合產(chǎn)生的消息流能夠生成正確的執(zhí)行路徑.

在TLS模式下,OpenVPN使用TLS協(xié)議認(rèn)證、建立安全隧道,并交換安全隧道的會(huì)話密鑰.基于TCP/UDP的OpenVPN報(bào)文格式如圖6所示.

Fig.6 Message format圖6 報(bào)文格式

OpenVPN報(bào)文主要包括IP頭、TCP/UDP頭、OpenVPN頭和OpenVPN載荷字段.其中,基于TCP和UDP協(xié)議的OpenVPN頭部有細(xì)微差異,UDP包含5位操作碼字段以及3位KeyID(密鑰標(biāo)號(hào)),基于TCP連接的報(bào)文的OpenVPN頭部信息還包括16位的包長(zhǎng)度字段.本文實(shí)驗(yàn)采取OpenVPN默認(rèn)的基于UDP連接的方式.數(shù)據(jù)包構(gòu)造示例如下.

OpenVPN初始化時(shí)的第 1個(gè)消息是客戶端向服務(wù)器端請(qǐng)求連接的 PHRCV2(P_CONTROL_HARD_RESET_CLIENT_V2)消息,其操作碼為0X07,keyID為0,因此,其VPNType(由5位操作碼與3位KeyID串聯(lián)而成)為MSG_TYPE_P_CONTROL_HARD_RESET_CLIENT_V2=0X38,代碼如下:

按照上述方法依次構(gòu)造數(shù)據(jù)包,有效性測(cè)試結(jié)果如圖7所示.可以看出,本文構(gòu)造的數(shù)據(jù)包在測(cè)試中能夠突破條件控制的限制.

OpenVPN協(xié)議沒有標(biāo)準(zhǔn)的協(xié)議規(guī)范,現(xiàn)有的可參考研究資料很少,系統(tǒng)中映射程序只能根據(jù)Wireshark工具捕獲真實(shí)數(shù)據(jù)包結(jié)合讀OpenVPN源碼來實(shí)現(xiàn).結(jié)合Open VPN系統(tǒng)特點(diǎn),在狀態(tài)機(jī)推斷過程中本文制定以下策略.

(1) OpenVPN按消息生成順序?yàn)閿?shù)據(jù)包編號(hào),因此在進(jìn)行狀態(tài)模糊測(cè)試的過程中需要正確處理消息序號(hào),否則會(huì)造成正確路徑難以正常執(zhí)行;

(2) 為了防止確認(rèn)機(jī)制導(dǎo)致的ACK數(shù)據(jù)包過多而出現(xiàn)無限狀態(tài)機(jī),因此在測(cè)試程序test harness中每每收到服務(wù)器端發(fā)回的響應(yīng)都對(duì)其進(jìn)行確認(rèn),且認(rèn)為狀態(tài)不改變;

(3) 測(cè)試程序每次執(zhí)行重置reset指令后,為了防止由于異常數(shù)據(jù)流導(dǎo)致拋出空指針異常,要對(duì)所有內(nèi)部變量進(jìn)行初始化;

(4) 出于應(yīng)用場(chǎng)景及安全性考慮,OpenVPN建議默認(rèn)配置下服務(wù)器要對(duì)客戶端身份進(jìn)行驗(yàn)證,因此測(cè)試程序?qū)LS中為可選項(xiàng)的客戶端證書驗(yàn)證過程進(jìn)行了實(shí)現(xiàn),同時(shí)也對(duì)客戶端證書為空時(shí)服務(wù)器端具體實(shí)現(xiàn)的邏輯行為進(jìn)行了測(cè)試;

(5) 網(wǎng)絡(luò)傳輸消息的拆分與組包,以及對(duì)每個(gè)拆分后數(shù)據(jù)包響應(yīng)的識(shí)別;

(6) OpenVPN密鑰協(xié)商子協(xié)議是在TLS加密隧道中完成的,整個(gè)過程都為密文封裝,因此不再進(jìn)行后續(xù)分析.

Fig.7 Packet construction test圖7 數(shù)據(jù)包構(gòu)造測(cè)試

2.3 狀態(tài)機(jī)推斷與化簡(jiǎn)

實(shí)驗(yàn)中,狀態(tài)機(jī)推斷采用經(jīng)典的L*[12]算法,一致性測(cè)試采用改進(jìn)的W[4]方法,用時(shí)19小時(shí)53分鐘,經(jīng)過76輪次的推斷與修正,推演出OpenVPN系統(tǒng)的狀態(tài)機(jī)見附錄1.在本文所示的狀態(tài)機(jī)圖中,節(jié)點(diǎn)代表狀態(tài),S0為起始狀態(tài),S2為連接關(guān)閉狀態(tài).邊上I/O形式的輸入/輸出符號(hào)對(duì)代表輸入消息以及目標(biāo)系統(tǒng)返回的響應(yīng)消息.如S0→S1,表示向目標(biāo)OpenVPN系統(tǒng)發(fā)送PHRCV2消息后得到響應(yīng)PHRSV2,由狀態(tài)S0遷移至狀態(tài)S1.

推斷得到的原始狀態(tài)機(jī)共存在18個(gè)不同狀態(tài)、133條狀態(tài)遷移,狀態(tài)遷移數(shù)量較多.過于復(fù)雜的狀態(tài)遷移使安全性分析非常困難.對(duì)推斷出的狀態(tài)機(jī)進(jìn)一步分析發(fā)現(xiàn):一方面,在TLS隧道建立過程中,任意握手?jǐn)?shù)據(jù)包或TLS數(shù)據(jù)流的錯(cuò)誤都會(huì)導(dǎo)致連接關(guān)閉,產(chǎn)生大量關(guān)閉連接的狀態(tài)遷移;另一方面,由于OpenVPN的確認(rèn)機(jī)制,大量ACK數(shù)據(jù)包會(huì)導(dǎo)致狀態(tài)機(jī)遷移冗余.然而這些狀態(tài)遷移對(duì)協(xié)議實(shí)現(xiàn)的安全性分析并無影響,因此對(duì)原始狀態(tài)機(jī)進(jìn)行化簡(jiǎn):將PCH/CLOSED,PCC/CLOSED,PCKE/CLOSED,PCV/CLOSED,PCCS/CLOSED,PF/CLOSED合并為Other/CLOSED,同時(shí)將服務(wù)器端接收不同消息并確認(rèn)合并為狀態(tài)遷移PF/PACK||PCCS/PACK||PCV/PACK||PCKE/PACK||PCH/PACK(“||”表示或的關(guān)系),化簡(jiǎn)后得到較為清晰簡(jiǎn)潔的狀態(tài)機(jī),如圖8所示.

Fig.8 The simplified state machine圖8 化簡(jiǎn)狀態(tài)機(jī)

2.4 時(shí)間壓縮模型

由本文第2.3節(jié)中推斷并化簡(jiǎn)后的狀態(tài)機(jī)可以看出:通過模型學(xué)習(xí)得到的OpenVPN系統(tǒng)狀態(tài)機(jī),除了正確路徑外還存在相似行為路徑,這說明狀態(tài)機(jī)在一定程度上可能存在狀態(tài)及路徑的近似等價(jià).由于狀態(tài)機(jī)主要是描述對(duì)象在它的生命周期內(nèi)所經(jīng)歷的狀態(tài)序列,因此協(xié)議狀態(tài)機(jī)也具有時(shí)間特性.我們考慮將狀態(tài)機(jī)在時(shí)間軸上進(jìn)行壓縮,對(duì)比其狀態(tài)及路徑的近似等價(jià)部分的差異性.

狀態(tài)融合技術(shù)是狀態(tài)機(jī)推斷相關(guān)研究中的一部分重要內(nèi)容.正則語言推斷中的RPNI算法[18]可根據(jù)樣本集構(gòu)建初始狀態(tài)機(jī),并不斷融合冗余狀態(tài),最終推斷出與給定樣本相一致的有限狀態(tài)自動(dòng)機(jī).但該算法在檢測(cè)候選狀態(tài)融合正確性時(shí)會(huì)產(chǎn)生大量的無效主動(dòng)推斷測(cè)試請(qǐng)求.因此,Lang等人[19]提出了依據(jù)狀態(tài)之間相似度對(duì)候選狀態(tài)排序的解決方案Blue-Fringe算法.本文借鑒王辰等人[20]對(duì)原始的Blue-Fringe算法相似度規(guī)則進(jìn)行擴(kuò)展的方法,提出狀態(tài)機(jī)時(shí)間壓縮模型.

由于協(xié)議實(shí)現(xiàn)都是根據(jù)輸入消息進(jìn)行響應(yīng)的網(wǎng)絡(luò)交互系統(tǒng),而協(xié)議狀態(tài)機(jī)描述了協(xié)議實(shí)體間的消息序列及狀態(tài)遷移,因此特別適合使用確定型的Mealy機(jī)來形式化描述協(xié)議狀態(tài)機(jī)模型[21].

定義1.協(xié)議狀態(tài)機(jī)模型定義為一個(gè)六元組M=(Q,I,O,δ,λ,q0),其中,Q為非空有限狀態(tài)集,I為有限輸入符號(hào)集,O為有限輸出符號(hào)集,q0∈Q為初始狀態(tài),δ:Q×I→Q為狀態(tài)遷移函數(shù),λ:Q×I→O為輸出函數(shù).

針對(duì)協(xié)議系統(tǒng)是對(duì)一系列通信報(bào)文序列進(jìn)行交互處理的特點(diǎn),將定義1中的狀態(tài)轉(zhuǎn)移函數(shù)δ和輸出函數(shù)λ的輸入從單個(gè)符號(hào)i∈I擴(kuò)展至符號(hào)序列w∈I*,對(duì)應(yīng)的輸出也為遷移狀態(tài)序列Q∈O*和輸出符號(hào)序列μ∈O*.例如:對(duì)于狀態(tài)q1∈Q,輸入字符序列w=i1…ik∈I*,輸出符號(hào)序列μ=λ(q1,w)=o1o2…ok,中間經(jīng)歷的遷移狀態(tài)Q=q2…qk+1∈O*.

定義2.狀態(tài)后綴定義為一個(gè)輸入/輸出符號(hào)序列集L={l1,l2,…,ln},輸入/輸出符號(hào)序列定義為l=i1/o1i2/o2...ik/ok,其中,in/on∈I/O.

狀態(tài)后綴是從該狀態(tài)出發(fā)的所有遷移路徑上的I/O序列的集合,其代表著該狀態(tài)對(duì)不同的輸入序列所響應(yīng)的輸出序列,是該狀態(tài)可能具有的不同行為的集合.

定義3.兩個(gè)狀態(tài)之間的相似度為其最長(zhǎng)共同后綴的長(zhǎng)度.

根據(jù)定義2和定義3,狀態(tài)后綴描述了一個(gè)狀態(tài)在協(xié)議系統(tǒng)中后續(xù)可能出現(xiàn)的所有行為特征.相似度就是兩個(gè)不同狀態(tài)最長(zhǎng)的相同后續(xù)I/O序列的長(zhǎng)度值,描述了兩個(gè)狀態(tài)后續(xù)行為特征集合中最為相似的行為路徑的相似程度.例如圖9所示,S1與S2的最長(zhǎng)共同后綴為I4/O4|I5/O5(“|”表示序列符號(hào)之間的連接關(guān)系),相似度為2.

Fig.9 Example of similarity calculation圖9 相似度計(jì)算示例

根據(jù)定義3可知:相似度可以作為一種衡量標(biāo)準(zhǔn),表明兩個(gè)不同狀態(tài)后續(xù)行為的近似程度.相似度越高,兩個(gè)狀態(tài)后續(xù)的行為集合中就具有越相似的行為.因此,本文考慮壓縮協(xié)議狀態(tài)機(jī)在時(shí)間軸上的近似等價(jià)行為,提出時(shí)間壓縮算法.設(shè)定相似度閾值變量depth反映對(duì)近似等價(jià)狀態(tài)合并的嚴(yán)苛程度,depth值越大,滿足合并條件的狀態(tài)數(shù)越少,說明要求能夠合并的狀態(tài)近似等價(jià)程度越高;反之,近似程度越低.

算法1.時(shí)間壓縮算法.

輸入:推斷得到的狀態(tài)機(jī)模型SM,相似度閾值depth;

輸出:經(jīng)過狀態(tài)融合后得到的SM*.

在該算法中需要注意:

·S0為起始狀態(tài),不考慮與其他狀態(tài)的壓縮;

· 因狀態(tài)機(jī)存在循環(huán),因此在計(jì)算共同后綴時(shí),若遇到已經(jīng)計(jì)算過的狀態(tài)節(jié)點(diǎn),則其后綴長(zhǎng)度不再增加;

· 當(dāng)兩個(gè)不同狀態(tài)經(jīng)過相同的路徑長(zhǎng)度后轉(zhuǎn)移到同一狀態(tài)時(shí),計(jì)算的共同后綴長(zhǎng)度不再增加;

· 該算法旨在針對(duì)狀態(tài)機(jī)時(shí)間特性進(jìn)行壓縮,在每輪融合當(dāng)前狀態(tài)后,處理后綴遷移路徑及狀態(tài)節(jié)點(diǎn)時(shí),只根據(jù)輸入符號(hào)判斷是否可合并,從而可能存在一條狀態(tài)遷移上輸入相同輸出不同的情況,因此最后得到的是類狀態(tài)機(jī)模型而非嚴(yán)格的Mealy機(jī);

· 雖然depth值越高,合并后不改變其他狀態(tài)機(jī)特性的可能性越大,但由于協(xié)議實(shí)現(xiàn)過程中的行為路徑往往與期望行為路徑存在一定差異,depth值過高會(huì)導(dǎo)致對(duì)特別行為的容忍度降低,可能會(huì)出現(xiàn)合并不完全的情況.基于以上考慮,本文取depth值為3.

以本文第2.3節(jié)中推演化簡(jiǎn)得到的狀態(tài)機(jī)作為初始狀態(tài)機(jī)SM,按照算法1對(duì)化簡(jiǎn)狀態(tài)機(jī)進(jìn)行時(shí)間壓縮后的模型如圖10所示.

Fig.10 Model of the simplified state machine after time compression圖10 對(duì)化簡(jiǎn)狀態(tài)機(jī)時(shí)間壓縮后的模型

3 OpenVPN狀態(tài)機(jī)脆弱性分析

基于模型學(xué)習(xí)的狀態(tài)機(jī)推斷方法通過主動(dòng)詢問的方式,確保了推斷結(jié)果的正確性,并且基于主動(dòng)學(xué)習(xí)型算法L*[15]可以保證推斷的狀態(tài)機(jī)是最小且完備的[1].在此基礎(chǔ)上,我們對(duì)化簡(jiǎn)狀態(tài)機(jī)與經(jīng)過時(shí)間壓縮后的模型進(jìn)行進(jìn)一步分析.

3.1 對(duì)化簡(jiǎn)后狀態(tài)機(jī)分析

我們將狀態(tài)機(jī)中的狀態(tài)變遷稱為OpenVPN系統(tǒng)的行為.由圖8可以看出,推演并化簡(jiǎn)后的OpenVPN系統(tǒng)狀態(tài)機(jī)中除了期望的正常行為外,還存在一些比較特別的狀態(tài)與行為.

· 期望的行為

狀態(tài)遷移路徑:S0→S1→S4→S6→S9→S12→S14→S16,如圖8中的虛線所示.

由初始狀態(tài)S0開始,經(jīng)過OpenVPN連接請(qǐng)求與響應(yīng)消息交互PHRCV2/PHRSV2到達(dá)S1后,開始協(xié)商TLS加密隧道:通過PCH/PSH|PC|PCR|PSHD到達(dá)S4(“|”代表連續(xù)的數(shù)據(jù)包),PCC/PACK|PACK到達(dá)S6(由于PCC消息包含了客戶端證書,消息內(nèi)容較長(zhǎng)將分割為多個(gè)數(shù)據(jù)包在網(wǎng)絡(luò)中傳輸,因此對(duì)其確認(rèn)的數(shù)據(jù)包也為多個(gè)),PCKE/PACK到達(dá)S9,PCV/PACK到達(dá)S12,PCCS/PACK到達(dá)S14,PF/PCCS|PF到達(dá)S16,此時(shí)加密隧道建立完成,之后開始以密文進(jìn)行子密鑰協(xié)商.

可以發(fā)現(xiàn),S16→S18→S5→S8→S11→S13→S15→S17也是一條成功的加密隧道建立路徑.

· 特別的行為

(1) 服務(wù)器在收到兩次PHRCV2連接請(qǐng)求后,從第3次開始不再回應(yīng)PHRSV2消息,而是基于OpenVPN協(xié)議的確認(rèn)機(jī)制返回PACK消息,因此會(huì)形成自循環(huán),如S3,S7,S18,圖8中雙圓節(jié)點(diǎn).這是由于SSL握手協(xié)議需要一個(gè)可靠的下層,從而采用確認(rèn)機(jī)制;

(2) 由S7→S5這個(gè)狀態(tài)遷移的過程可以看出:在完成兩次加密隧道建立的情況下,發(fā)送TLS握手消息都轉(zhuǎn)移到狀態(tài)S5,此狀態(tài)可繼續(xù)順利完成握手,但雙方不再需要進(jìn)行TLS握手的ClientHello,ServerHello等消息交換;

(3)S1(或S4,S6,S9,S12,S14)→S3→S5→S8→S11→S13→S15→S17也是成功的隧道連接路徑,這正是由于特別行為1允許服務(wù)器端在收到重復(fù)的客戶端連接請(qǐng)求PHRCV2后,對(duì)服務(wù)器端響應(yīng)兩次PHRSV2以確?？煽總鬏?

(4) 在非正常數(shù)據(jù)流中,服務(wù)器端會(huì)對(duì)客戶端的亂序數(shù)據(jù)包給予一定程度的確認(rèn)響應(yīng),如經(jīng)過PCH/PACK,PF/PACK,PCCS/PACK,PCV/PACK,PCKE/PACK等消息對(duì)的交互,但當(dāng)前狀態(tài)并未發(fā)生改變,如S10;

(5) 由于網(wǎng)絡(luò)傳輸數(shù)據(jù)包大小有一定的限制,因此存在消息拆分與組裝問題,這就造成了出現(xiàn)類似PCC/PACK|PACK這樣的消息對(duì),即,客戶端發(fā)送的證書被拆分為兩個(gè)數(shù)據(jù)包,相應(yīng)地也就得到了兩個(gè)服務(wù)器端的響應(yīng)消息;

(6)S18→S5的狀態(tài)遷移上出現(xiàn)了PCH/DecryptError,這是因?yàn)樵赟18的前一個(gè)狀態(tài)S16已經(jīng)完成了隧道建立,此時(shí)再次發(fā)送PHRCV2時(shí)會(huì)重新請(qǐng)求協(xié)商加密隧道,但test harness認(rèn)為仍在加密隧道中而進(jìn)行解密,從而出現(xiàn)解密失敗.

綜合以上分析可以看出,OpenVPN系統(tǒng)實(shí)現(xiàn)狀態(tài)機(jī)的特別行為可能導(dǎo)致攻擊路徑的存在.例如,依據(jù)RFC 2246可知:傳統(tǒng)的ClientHello,ServerHello消息格式中分別包含了客戶端和服務(wù)器端產(chǎn)生的隨機(jī)數(shù)random,而在特別行為2中,完成兩次加密隧道建立后,再次握手重連時(shí)不再進(jìn)行ClientHello,ServerHello消息交互,這與規(guī)范的TLS握手過程不同,導(dǎo)致至少通信雙方的隨機(jī)數(shù)沒有更新.另一方面,由于OpenVPN缺乏詳細(xì)的官方規(guī)范,前期Novickis[11]在2016年做過相關(guān)研究,但其最終也并未實(shí)現(xiàn)推斷出OpenVPN實(shí)現(xiàn)狀態(tài)機(jī)的目標(biāo),因此本文推斷狀態(tài)機(jī)發(fā)現(xiàn)的期望行為和特殊行為,為OpenVPN安全研究提供了參考依據(jù).

3.2 與期望的狀態(tài)機(jī)對(duì)比

與第1節(jié)基礎(chǔ)知識(shí)中借鑒的Novickis給出的期望的狀態(tài)機(jī)[14]作比較可以發(fā)現(xiàn):本文測(cè)試得到的OpenVPN實(shí)現(xiàn)的狀態(tài)機(jī)具有18個(gè)不同狀態(tài),與期望的狀態(tài)機(jī)相比更為復(fù)雜;真實(shí)實(shí)現(xiàn)的狀態(tài)機(jī)完成隧道建立的路徑不止一條,而期望的狀態(tài)機(jī)未考慮OpenVPN確認(rèn)機(jī)制帶來的影響;真實(shí)實(shí)現(xiàn)的狀態(tài)機(jī)在任何時(shí)候都接受PHRCV2消息重新建立連接,但期望的狀態(tài)機(jī)只在起始狀態(tài)接受該連接請(qǐng)求并相應(yīng);由于本文測(cè)試目標(biāo)為OpenVPN協(xié)議的客戶端實(shí)現(xiàn),無法測(cè)得服務(wù)器端發(fā)送P_CONTROL_SOFT_ RESET_V1消息請(qǐng)求與客戶端進(jìn)行重協(xié)商的過程,因此不存在期望的狀態(tài)機(jī)中S7→S8的狀態(tài)遷移.

綜上所述,雖然真實(shí)測(cè)得的狀態(tài)機(jī)較為復(fù)雜,但其完整顯示了協(xié)議實(shí)現(xiàn)的重要過程,且根據(jù)狀態(tài)機(jī)路徑能夠得到一些協(xié)議實(shí)現(xiàn)的具體細(xì)節(jié),如服務(wù)器端對(duì)OpenVPN連接請(qǐng)求響應(yīng)兩次后轉(zhuǎn)為ACK確認(rèn).這對(duì)于類似缺少協(xié)議規(guī)范但應(yīng)用廣泛的安全協(xié)議的分析具有重要的參考意義.

3.3 與TLS狀態(tài)機(jī)比對(duì)

由于OpenVPN安全性是以SSL/TLS加密隧道為基礎(chǔ)的,因此將推斷得到的OpenVPN 2.0.9系統(tǒng)狀態(tài)機(jī)與其對(duì)應(yīng)的OpenSSL 1.0.2g系統(tǒng)狀態(tài)機(jī)進(jìn)行對(duì)比分析.基于Statelearner開源框架推斷出OpenSSL 1.0.2g的狀態(tài)機(jī)如圖11所示.由于SSL/TLS協(xié)議是基于TCP的可靠連接,握手過程不需要確認(rèn)機(jī)制,因此會(huì)出現(xiàn)在發(fā)送ClientKeyExchange,ChangeCipherSpec消息時(shí)沒有收到服務(wù)器端的響應(yīng)(記為Empty),但狀態(tài)已發(fā)生遷移的情況.另一方面,由于TLS協(xié)議中用于檢測(cè)連接是否保持的心跳請(qǐng)求數(shù)據(jù)包只有在握手階段完成后才會(huì)得到響應(yīng),且其會(huì)導(dǎo)致出現(xiàn)無限狀態(tài)機(jī)模型[4],會(huì)對(duì)本文的協(xié)議脆弱性分析工作造成困難,且對(duì)安全連接階段的檢測(cè)分析沒有影響,因此在輸入表中將其刪除.

Fig.11 Server side state machine of OpenSSL 1.0.2g圖11 OpenSSL 1.0.2g服務(wù)器端狀態(tài)機(jī)

由圖8與圖11對(duì)比可知:雖然OpenVPN基于OpenSSL建立加密隧道進(jìn)行安全傳輸,但其由于特有的確認(rèn)機(jī)制以及開發(fā)者對(duì)于重鏈接的具體實(shí)現(xiàn),導(dǎo)致其具體實(shí)現(xiàn)的狀態(tài)機(jī)較為復(fù)雜,且擁有不止一條成功路徑,這使得OpenVPN通信雙方在后續(xù)的數(shù)據(jù)加密密鑰協(xié)商及數(shù)據(jù)加密過程中都存在一定的安全隱患.

由圖10與圖11對(duì)比可知:通過對(duì)OpenVPN實(shí)現(xiàn)狀態(tài)機(jī)進(jìn)行時(shí)間壓縮,期望中應(yīng)該是相對(duì)應(yīng)版本OpenSSL實(shí)現(xiàn)狀態(tài)機(jī)的擴(kuò)充(如增加OpenVPN連接請(qǐng)求與響應(yīng)等),且能很清晰地看出不同輪次連接建立中的差異.如S1/S3自循環(huán)與S16/S17→S10/S18,這兩條狀態(tài)遷移就是由于加密隧道建立過程中因?yàn)檫B接請(qǐng)求次數(shù)不同而響應(yīng)不同,符合第3.1節(jié)中描述的特別行為1.除此之外,還存在S7這樣特殊的狀態(tài),其產(chǎn)生的原因正是OpenVPN協(xié)議對(duì)消息拆分產(chǎn)生多次響應(yīng),與分析的特別行為5一致.

3.4 對(duì)時(shí)間壓縮模型分析

圖10顯示了對(duì)化簡(jiǎn)狀態(tài)機(jī)進(jìn)行時(shí)間壓縮后的模型中共有11個(gè)狀態(tài)節(jié)點(diǎn)、36條不同的狀態(tài)遷移.與圖8化簡(jiǎn)狀態(tài)機(jī)18個(gè)狀態(tài)節(jié)點(diǎn)、50條遷移相比更加精簡(jiǎn).但需要注意的是,采用時(shí)間壓縮算法得到的模型并不是Mealy機(jī).這是由于在時(shí)間軸上進(jìn)行了壓縮,可能出現(xiàn)某一狀態(tài)的狀態(tài)遷移上輸入相同、輸出不同,卻遷移至同一狀態(tài)的情況.如圖10中的由原狀態(tài)S1和S3合并得到的節(jié)點(diǎn),其輸入PHRCV2消息后,在不同時(shí)間點(diǎn)可能得到的響應(yīng)為PHRSV2或PACK.

· 時(shí)間壓縮模型對(duì)期望的系統(tǒng)行為的刻畫

圖10中虛線所示路徑即為期望中的加密隧道建立路徑:

S0→S1/S3→S4/S5→S6/S8→S9/S11→S12/S13→S14/S15→S16/S17,說明該時(shí)間壓縮模型能夠表示推斷并化簡(jiǎn)得到的狀態(tài)機(jī)圖中的期望路徑.

· 時(shí)間壓縮模型對(duì)系統(tǒng)特別行為的刻畫

(1) 對(duì)于不同輪次的連接請(qǐng)求PHRCV2,時(shí)間壓縮模型通過狀態(tài)合并以及采用集合{PHRSV2,PACK}表示可能收到的響應(yīng)消息,可以清楚地展示出OpenVPN系統(tǒng)服務(wù)器端對(duì)PHRCV2消息在不同時(shí)間點(diǎn)響應(yīng)是具有差異性的;

(2) 雙圓節(jié)點(diǎn)的自循環(huán)行為以及S10/S18節(jié)點(diǎn)反映了OpenVPN系統(tǒng)的確認(rèn)機(jī)制;

(3)S7,S10,S18等具有特別行為的狀態(tài)經(jīng)過時(shí)間壓縮算法后仍能夠很好地保持其特征.

由上面的分析可以看出來:經(jīng)過時(shí)間壓縮后的狀態(tài)機(jī)模型合并了對(duì)協(xié)議進(jìn)行安全性分析沒有影響的近似等價(jià)的遷移路徑與狀態(tài),與原狀態(tài)機(jī)相比更加清晰且能夠充分反映出原模型的各種特征——期望的路徑與特殊的路徑.因此,通過對(duì)狀態(tài)機(jī)時(shí)間壓縮模型所進(jìn)行的分析,是尋找協(xié)議實(shí)現(xiàn)中可能存在的攻擊路徑的一種簡(jiǎn)單可行的方法.

4 結(jié) 語

本文主要研究了對(duì)網(wǎng)絡(luò)安全協(xié)議的實(shí)現(xiàn)邏輯脆弱性進(jìn)行自動(dòng)化分析的問題.基于模型學(xué)習(xí)的方法,對(duì)OpenVPN系統(tǒng)實(shí)現(xiàn)邏輯進(jìn)行黑盒測(cè)試分析,自動(dòng)推演出系統(tǒng)的實(shí)現(xiàn)狀態(tài)機(jī),發(fā)現(xiàn)了多條期望路徑外的特別路徑及可能的安全隱患,為目標(biāo)系統(tǒng)的脆弱性分析和攻擊路徑發(fā)現(xiàn)提供依據(jù),提出了針對(duì)協(xié)議實(shí)現(xiàn)狀態(tài)機(jī)的時(shí)間壓縮模型及算法,提高了脆弱性分析和攻擊路徑發(fā)現(xiàn)的效率.本文研究成果為大型應(yīng)用的安全協(xié)議的脆弱性分析提供了理論和技術(shù)支持.

附錄1.