基于模型學習的OpenVPN系統脆弱性分析?

2019-10-26 18:05:22申瑩珠顧純祥張協力盧政宇

軟件學報 2019年12期

關鍵詞：模型

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

1(信息工程大學網絡空間安全學院,河南鄭州 450001)

2(河南省網絡密碼技術重點實驗室,河南鄭州 450001)

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

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

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

本文基于模型學習的方法,利用協議狀態模糊測試技術,對OpenVPN 2.0.9服務器端進行了模型學習和一致性檢測,自動推演出目標系統的協議實現狀態機,并對其狀態機模型進行化簡,對其實現邏輯及過程進行詳細分析;提出了一種狀態機時間壓縮模型,與原始狀態機及同版本OpenSSL狀態機進行對比分析.結果表明:利用經化簡后的模型可以更方便迅速地識別協議狀態機中正常的和特殊的狀態遷移路徑,從而提高OpenVPN脆弱性檢測與分析的效率.

1 基礎知識

1.1 OpenVPN協議

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

· OpenVPN協議TLS模式下的實現

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

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

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

(1) OpenVPN握手協議,類似于TCP的3次握手過程,握手數據包包括:由客戶端發起的握手請求數據包P_CONTROL_HARD_RESET_CLIENT_V1/V2(V1/V2代表后續兩種不同的密鑰協商方式,分別對應PSK認證模式和TLS認證模式,OpenVPN 2.0以上版本默認使用P_CONTROL_HARD_RESET_CLIENT_V2),服務器端的請求響應數據包P_CONTROL_HARD_RESET_SERVER_V1/V2(密鑰協商方式與請求一致),客戶端對服務器端響應的確認P_ACK_V1;

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

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

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

OpenVPN沒有詳細的官方規范,2016年,Tomas Novickis方法[11]中給出的在TLS模式下期望的OpenVPN狀態機如圖3所示.Novickis試圖基于LearnLib得出真實的OpenVPN實現的狀態機,但其在研究過程中主要遇到了以下困難:(1) 使用python庫Scapy可以快速構造數據包,但僅嘗試利用之前Wirshark捕獲的數據包載荷進行復用,未根據協議原理精心設計每個數據包字段,導致無法通過證書驗證或HMAC校驗;(2) P_CONTROL_V1數據包載荷較多需要分塊傳輸時還存在一些問題.因此,作者得到OpenVPN實現狀態機的目標并未實現.

Fig.3 The expected OpenVPN state machine圖3 期望的OpenVPN狀態機

1.2 模型學習與一致性檢測

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

Fig.4 MAT framework圖4 MAT框架

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

具體過程如下.

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

b.等價查詢:采用近似等價查詢算法進行一致性檢測,如Chow提出的W-method算法[14]、Ruiter改進的wmethod[4]等.通過有限數量的測試查詢,檢測該推斷是否與實際的狀態機等價.如果不等價,將會返回一個反例,學習器使用該反例重新進行推斷,即進行模型修正.如果沒有找到反例,則認為當前狀態機推斷近似等價于真實實現,得到協議實現的狀態機.

Fig.5 System architecture圖5 系統架構

2 基于模型學習的OpenVPN狀態機推斷

本文在模型學習與一致性檢測技術的基礎上,基于LearnLib平臺[15,16]開發了針對OpenVPN的狀態機推斷框架,本文只考慮TLS模式下的OpenVPN狀態機推斷問題.

· 實驗環境:Intel core i7-4790處理器、8G內存、Ubuntu 16.04-64位系統、Wireshark軟件;

· 協議版本:OpenSSL 1.0.2h,OpenVPN 2.0.9;

· 編程語言:Java,Python;

· 環境配置:采用橋接模式,在兩臺虛擬機中分別配置本文系統與OpenVPN 2.0.9服務器端環境進行測試.其中,OpenVPN通信采用默認的UDP連接方式(在OpenVPN協議的可靠傳輸要求下,即使采用TCP連接,也同樣需要實現確認機制).

2.1 輸入/輸出表構造

本文主要測試OpenVPN服務器端狀態機,因此根據OpenVPN協議中客戶端消息集構造輸入表以及服務器端響應消息集構造輸出表,輸入/輸出表的符號表示及消息含義見表1.

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

轉換程序Test harness基于OpenVPN底層協議,對學習器的消息輸入表中的消息進行精心構造,按照學習器中的狀態機推斷與近似等價算法與測試目標進行交互,并將服務器端返回的響應消息識別、抽象,送入學習器繼續分析推斷,直到完成真實的OpenVPN服務器端狀態機的學習與檢測;通過比對協議實現狀態機與協議標準狀態機(或期望的狀態機)之間的差異性,找到可能存在的攻擊路徑.

2.2 數據包構造及狀態機推斷策略

網絡安全協議的執行路徑中往往存在許多條件控制,這也正是限制傳統模糊測試進行脆弱性分析檢測能力與效率的一個重要方面.因此在狀態模糊測試中,數據包構造是整個測試的基礎[17].OpenVPN協議中只有正確的證書驗證、HMAC校驗等才能順利完成整個連接過程.

本文參考RFC 2246及Wireshark捕獲的OpenVPN真實通信數據,精心構造轉換程序中使用的數據包,并按照期望的路徑進行測試,保證構造的消息集合產生的消息流能夠生成正確的執行路徑.

在TLS模式下,OpenVPN使用TLS協議認證、建立安全隧道,并交換安全隧道的會話密鑰.基于TCP/UDP的OpenVPN報文格式如圖6所示.

Fig.6 Message format圖6 報文格式

OpenVPN報文主要包括IP頭、TCP/UDP頭、OpenVPN頭和OpenVPN載荷字段.其中,基于TCP和UDP協議的OpenVPN頭部有細微差異,UDP包含5位操作碼字段以及3位KeyID(密鑰標號),基于TCP連接的報文的OpenVPN頭部信息還包括16位的包長度字段.本文實驗采取OpenVPN默認的基于UDP連接的方式.數據包構造示例如下.

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

按照上述方法依次構造數據包,有效性測試結果如圖7所示.可以看出,本文構造的數據包在測試中能夠突破條件控制的限制.

OpenVPN協議沒有標準的協議規范,現有的可參考研究資料很少,系統中映射程序只能根據Wireshark工具捕獲真實數據包結合讀OpenVPN源碼來實現.結合Open VPN系統特點,在狀態機推斷過程中本文制定以下策略.

(1) OpenVPN按消息生成順序為數據包編號,因此在進行狀態模糊測試的過程中需要正確處理消息序號,否則會造成正確路徑難以正常執行;

(2) 為了防止確認機制導致的ACK數據包過多而出現無限狀態機,因此在測試程序test harness中每每收到服務器端發回的響應都對其進行確認,且認為狀態不改變;

(3) 測試程序每次執行重置reset指令后,為了防止由于異常數據流導致拋出空指針異常,要對所有內部變量進行初始化;

(4) 出于應用場景及安全性考慮,OpenVPN建議默認配置下服務器要對客戶端身份進行驗證,因此測試程序對TLS中為可選項的客戶端證書驗證過程進行了實現,同時也對客戶端證書為空時服務器端具體實現的邏輯行為進行了測試;

(5) 網絡傳輸消息的拆分與組包,以及對每個拆分后數據包響應的識別;

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

Fig.7 Packet construction test圖7 數據包構造測試

2.3 狀態機推斷與化簡

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

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

Fig.8 The simplified state machine圖8 化簡狀態機

2.4 時間壓縮模型

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

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

由于協議實現都是根據輸入消息進行響應的網絡交互系統,而協議狀態機描述了協議實體間的消息序列及狀態遷移,因此特別適合使用確定型的Mealy機來形式化描述協議狀態機模型[21].

定義1.協議狀態機模型定義為一個六元組M=(Q,I,O,δ,λ,q0),其中,Q為非空有限狀態集,I為有限輸入符號集,O為有限輸出符號集,q0∈Q為初始狀態,δ:Q×I→Q為狀態遷移函數,λ:Q×I→O為輸出函數.

針對協議系統是對一系列通信報文序列進行交互處理的特點,將定義1中的狀態轉移函數δ和輸出函數λ的輸入從單個符號i∈I擴展至符號序列w∈I*,對應的輸出也為遷移狀態序列Q∈O*和輸出符號序列μ∈O*.例如:對于狀態q1∈Q,輸入字符序列w=i1…ik∈I*,輸出符號序列μ=λ(q1,w)=o1o2…ok,中間經歷的遷移狀態Q=q2…qk+1∈O*.

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

狀態后綴是從該狀態出發的所有遷移路徑上的I/O序列的集合,其代表著該狀態對不同的輸入序列所響應的輸出序列,是該狀態可能具有的不同行為的集合.

定義3.兩個狀態之間的相似度為其最長共同后綴的長度.

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

Fig.9 Example of similarity calculation圖9 相似度計算示例

根據定義3可知:相似度可以作為一種衡量標準,表明兩個不同狀態后續行為的近似程度.相似度越高,兩個狀態后續的行為集合中就具有越相似的行為.因此,本文考慮壓縮協議狀態機在時間軸上的近似等價行為,提出時間壓縮算法.設定相似度閾值變量depth反映對近似等價狀態合并的嚴苛程度,depth值越大,滿足合并條件的狀態數越少,說明要求能夠合并的狀態近似等價程度越高;反之,近似程度越低.

算法1.時間壓縮算法.

輸入:推斷得到的狀態機模型SM,相似度閾值depth;

輸出:經過狀態融合后得到的SM*.

在該算法中需要注意:

·S0為起始狀態,不考慮與其他狀態的壓縮;

· 因狀態機存在循環,因此在計算共同后綴時,若遇到已經計算過的狀態節點,則其后綴長度不再增加;

· 當兩個不同狀態經過相同的路徑長度后轉移到同一狀態時,計算的共同后綴長度不再增加;

· 該算法旨在針對狀態機時間特性進行壓縮,在每輪融合當前狀態后,處理后綴遷移路徑及狀態節點時,只根據輸入符號判斷是否可合并,從而可能存在一條狀態遷移上輸入相同輸出不同的情況,因此最后得到的是類狀態機模型而非嚴格的Mealy機;

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

以本文第2.3節中推演化簡得到的狀態機作為初始狀態機SM,按照算法1對化簡狀態機進行時間壓縮后的模型如圖10所示.

Fig.10 Model of the simplified state machine after time compression圖10 對化簡狀態機時間壓縮后的模型

3 OpenVPN狀態機脆弱性分析

基于模型學習的狀態機推斷方法通過主動詢問的方式,確保了推斷結果的正確性,并且基于主動學習型算法L*[15]可以保證推斷的狀態機是最小且完備的[1].在此基礎上,我們對化簡狀態機與經過時間壓縮后的模型進行進一步分析.

3.1 對化簡后狀態機分析

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

· 期望的行為

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

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

· 特別的行為

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

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

(3)S1(或S4,S6,S9,S12,S14)→S3→S5→S8→S11→S13→S15→S17也是成功的隧道連接路徑,這正是由于特別行為1允許服務器端在收到重復的客戶端連接請求PHRCV2后,對服務器端響應兩次PHRSV2以確保可靠傳輸;

(4) 在非正常數據流中,服務器端會對客戶端的亂序數據包給予一定程度的確認響應,如經過PCH/PACK,PF/PACK,PCCS/PACK,PCV/PACK,PCKE/PACK等消息對的交互,但當前狀態并未發生改變,如S10;

(5) 由于網絡傳輸數據包大小有一定的限制,因此存在消息拆分與組裝問題,這就造成了出現類似PCC/PACK|PACK這樣的消息對,即,客戶端發送的證書被拆分為兩個數據包,相應地也就得到了兩個服務器端的響應消息;

(6)S18→S5的狀態遷移上出現了PCH/DecryptError,這是因為在S18的前一個狀態S16已經完成了隧道建立,此時再次發送PHRCV2時會重新請求協商加密隧道,但test harness認為仍在加密隧道中而進行解密,從而出現解密失敗.

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

3.2 與期望的狀態機對比

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

綜上所述,雖然真實測得的狀態機較為復雜,但其完整顯示了協議實現的重要過程,且根據狀態機路徑能夠得到一些協議實現的具體細節,如服務器端對OpenVPN連接請求響應兩次后轉為ACK確認.這對于類似缺少協議規范但應用廣泛的安全協議的分析具有重要的參考意義.

3.3 與TLS狀態機比對

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

Fig.11 Server side state machine of OpenSSL 1.0.2g圖11 OpenSSL 1.0.2g服務器端狀態機

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

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

3.4 對時間壓縮模型分析

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

· 時間壓縮模型對期望的系統行為的刻畫

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

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

· 時間壓縮模型對系統特別行為的刻畫

(1) 對于不同輪次的連接請求PHRCV2,時間壓縮模型通過狀態合并以及采用集合{PHRSV2,PACK}表示可能收到的響應消息,可以清楚地展示出OpenVPN系統服務器端對PHRCV2消息在不同時間點響應是具有差異性的;

(2) 雙圓節點的自循環行為以及S10/S18節點反映了OpenVPN系統的確認機制;

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

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

4 結語

本文主要研究了對網絡安全協議的實現邏輯脆弱性進行自動化分析的問題.基于模型學習的方法,對OpenVPN系統實現邏輯進行黑盒測試分析,自動推演出系統的實現狀態機,發現了多條期望路徑外的特別路徑及可能的安全隱患,為目標系統的脆弱性分析和攻擊路徑發現提供依據,提出了針對協議實現狀態機的時間壓縮模型及算法,提高了脆弱性分析和攻擊路徑發現的效率.本文研究成果為大型應用的安全協議的脆弱性分析提供了理論和技術支持.

附錄1.