基于模型檢測的TLS協(xié)議實(shí)現(xiàn)庫安全性分析

畢 興,唐朝京

(1.國防科技大學(xué)前沿交叉學(xué)科學(xué)院,湖南 長沙 410073;2.國防科技大學(xué)電子科學(xué)學(xué)院,湖南 長沙 410073)

0 引 言

傳輸層安全性(transport layer security,TLS)[1]協(xié)議作為廣泛應(yīng)用的網(wǎng)絡(luò)安全協(xié)議,用于確保網(wǎng)絡(luò)安全通信,能夠保障網(wǎng)絡(luò)數(shù)據(jù)機(jī)密性及完整性，從面世開始就受到了各類研究者及攻擊者的高度重視，也始終面臨著密碼學(xué)攻擊、邏輯漏洞的威脅。其中TLS協(xié)議實(shí)現(xiàn)庫作為TLS協(xié)議的應(yīng)用載體,有許多對于協(xié)議的攻擊是針對TLS協(xié)議實(shí)現(xiàn)庫進(jìn)行的,如幸運(yùn)13漏洞(Lucky13)[2]、密文填塞攻擊(Padding-Oracle)[3]和貴賓犬攻擊(Poodle)[4]。但是,這些攻擊是對協(xié)議實(shí)現(xiàn)而非協(xié)規(guī)范的攻擊,并沒有方法能夠有效發(fā)現(xiàn)協(xié)議實(shí)現(xiàn)庫存在的邏輯漏洞。

在安全協(xié)議中,每個多余的狀態(tài)或遷移都不是必要的,并且其中可能有潛在的安全威脅,需要進(jìn)行仔細(xì)的檢查。這種多余或過渡的狀態(tài)通常不易發(fā)現(xiàn)。模型檢測技術(shù)作為形式化分析中的一種重要方法,能夠?qū)顟B(tài)機(jī)進(jìn)行可靠且系統(tǒng)的分析,已經(jīng)能夠驗(yàn)證TLS 1.2協(xié)議規(guī)范滿足其安全目標(biāo),但在實(shí)現(xiàn)TLS時,這些規(guī)范為開發(fā)人員在處理錯誤或異常方面和實(shí)現(xiàn)協(xié)議方面留出了很大的自由度。這些異常消息在規(guī)范中并沒有嚴(yán)格固定,可以在實(shí)現(xiàn)協(xié)議時自由選擇。這也意味著即使協(xié)議規(guī)范已經(jīng)證明安全的協(xié)議,其實(shí)現(xiàn)仍可能存在缺陷。為了檢測這些實(shí)現(xiàn)上的缺陷,需要靜態(tài)分析或模糊測試技術(shù)。但是這些技術(shù)通常對內(nèi)存溢出等漏洞有效,而無法挖掘協(xié)議實(shí)現(xiàn)庫的邏輯漏洞。通過提取安全協(xié)議實(shí)現(xiàn)的狀態(tài)機(jī),能夠?qū)崿F(xiàn)對協(xié)議實(shí)現(xiàn)的形式化建模。但是目前能夠用于精確分析協(xié)議實(shí)現(xiàn)狀態(tài)機(jī)的技術(shù)較少且效果不佳。

本文針對此問題,對協(xié)議實(shí)現(xiàn)庫采用狀態(tài)機(jī)學(xué)習(xí)技術(shù),提取了協(xié)議實(shí)現(xiàn)庫的狀態(tài)機(jī)模型,同時對照協(xié)議規(guī)范請求意見稿(request for comments,RFC)中的安全條件,建立協(xié)議安全屬性模型,并通過模型檢測方法,利用新型符號模型檢查器(new symbolic model verifier,NuSMV)[5],完成了對TLS協(xié)議實(shí)現(xiàn)庫的形式化分析,用于尋找TLS協(xié)議實(shí)現(xiàn)庫的邏輯漏洞。與Beurdouche等人通過從手動構(gòu)建的參考協(xié)議狀態(tài)機(jī)開始對TLS實(shí)現(xiàn)庫分析不同[6-7],本文方法在沒有先驗(yàn)知識的情況下,通過協(xié)議實(shí)現(xiàn)黑盒測試推斷出狀態(tài)機(jī),具有更完備的路徑覆蓋。此外,Beurdouche等人的測試并非真正的隨機(jī)性,使用的是一組啟發(fā)式測試自動生成的測試跡,而本文方法利用了完全隨機(jī)的測試協(xié)議。與Brostean、申瑩珠等人通過對推斷得到的狀態(tài)機(jī)進(jìn)行人工分析[8-9]不同,本文通過模型檢測技術(shù),能夠?qū)崿F(xiàn)對協(xié)議實(shí)現(xiàn)的形式化建模,并精確分析協(xié)議實(shí)現(xiàn)狀態(tài)機(jī)的邏輯漏洞。

1 安全協(xié)議實(shí)現(xiàn)層的形式化驗(yàn)證

從安全協(xié)議的設(shè)計到實(shí)現(xiàn)的過程上看,安全協(xié)議包括規(guī)范和實(shí)現(xiàn)兩個層次,如圖1所示。上層為規(guī)范層,重點(diǎn)考慮協(xié)議實(shí)體間的消息時序關(guān)系和實(shí)體內(nèi)部運(yùn)算細(xì)節(jié),例如具體的消息長度、采用的加密算法、加密模式、分組填充方式、協(xié)議版本兼容、子協(xié)議交互等等，表現(xiàn)為使用函數(shù)符號抽象實(shí)體的內(nèi)部計算。規(guī)范層的協(xié)議通常表示為消息交互圖(message switch chart,MSC),其漏洞主要為邏輯漏洞和部分密碼算法漏洞,目前的形式化方法中的符號方法和計算方法主要針對規(guī)范層進(jìn)行驗(yàn)證。而協(xié)議實(shí)現(xiàn)層考慮協(xié)議采用具體編程語言的軟件實(shí)現(xiàn),其漏洞除了包含規(guī)范層漏洞外,還包括實(shí)現(xiàn)協(xié)議功能的漏洞,如緩沖區(qū)溢出、內(nèi)存泄露等。例如“心臟出血”漏洞(heartbleed)與TLS安全套接層(secure sockets layer,SSL)協(xié)議規(guī)范無關(guān),只存在某些版本的開放式SSL(openSSL)協(xié)議中。通常對協(xié)議實(shí)現(xiàn)的分析只能聚焦于傳統(tǒng)軟件安全性分析層面,目前很少有針對實(shí)現(xiàn)層的形式化分析方法,難以找到其中存在的邏輯性問題。

圖1 協(xié)議分析層次Fig.1 Protocol analysis layer

傳統(tǒng)的協(xié)議實(shí)現(xiàn)的安全性分析主要通過測試的方式進(jìn)行,目前主流方向是使用程序測試的方式,對程序進(jìn)行模糊測試,以求達(dá)到覆蓋率盡可能高、測試深度盡可能深的目的[10]。然而,這種技術(shù)通常找到的是普通的程序錯誤,如緩沖區(qū)溢出漏洞或內(nèi)存二次釋放問題,卻無法發(fā)現(xiàn)程序中的邏輯問題[11]。

在對協(xié)議實(shí)現(xiàn)的研究過程中,研究者逐漸認(rèn)識到要想系統(tǒng)地分析協(xié)議實(shí)現(xiàn)在設(shè)計邏輯上的安全性,需要對協(xié)議實(shí)現(xiàn)建立嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)模型,并對此模型進(jìn)行形式化分析,才有可能達(dá)到目的。

狀態(tài)機(jī)建模是其中一種常用的建模方法[12]。Hsu等人通過提取微軟網(wǎng)絡(luò)服務(wù)(Microsoft service network,MSN)直接消息協(xié)議的狀態(tài)機(jī)模型指導(dǎo)模糊測試,發(fā)現(xiàn)了許多未知漏洞并成功觸發(fā)了多次系統(tǒng)崩潰[13]。Stone等人分析了802.11無線協(xié)議中握手協(xié)議的狀態(tài)機(jī)模型以及協(xié)議的安全性[14]。Danei等人通過協(xié)議模糊測試,得到了開放式虛擬專人網(wǎng)絡(luò)(open virtual private network,OpenVPN)協(xié)議實(shí)現(xiàn)庫的狀態(tài)機(jī)模型[15]。Stone等人擴(kuò)展?fàn)顟B(tài)機(jī)學(xué)習(xí)以處理超時行為和不可靠的通信介質(zhì),對802.11握手協(xié)議實(shí)施進(jìn)行了首次全自動分析[16]。Sivakorn等人通過自動機(jī)學(xué)習(xí)算法來推斷確定性有限自動機(jī),驗(yàn)證了TLS/SSL庫中的主機(jī)名驗(yàn)證實(shí)現(xiàn)[17]。Marallo等人對802.11握手協(xié)議背后的狀態(tài)機(jī)進(jìn)行了分析,發(fā)現(xiàn)其中存在安全性漏洞[18]。

同時研究人員也在嘗試直接對協(xié)議實(shí)現(xiàn)進(jìn)行模型檢測。但是Moura等人[19]證明,由于狀態(tài)爆炸問題,這種窮舉的模型檢測方式在實(shí)際操作中是不可行的。傳統(tǒng)的模型檢測方法仍無法有效地對安全協(xié)議進(jìn)行分析,但是當(dāng)前已有研究者開始對協(xié)議實(shí)現(xiàn)庫利用模型檢測方法進(jìn)行研究。Borisov等人通過謂詞公式對協(xié)議實(shí)現(xiàn)建模并用于錯誤搜索[20]。Harris等人對IP網(wǎng)絡(luò)語音電話中的會話啟動協(xié)議實(shí)現(xiàn)建立了狀態(tài)機(jī)模型并通過分析其中狀態(tài),發(fā)現(xiàn)了一個零日漏洞[21]。Chen等人通過模型檢測工具Spin對互聯(lián)網(wǎng)密鑰交換(Internet key exchange,IKEv2)協(xié)議進(jìn)行了安全驗(yàn)證[22]。Drury等人基于定時自動機(jī)網(wǎng)絡(luò),通過模型檢測器Uppaal驗(yàn)證了開放式最短路徑優(yōu)先(open shortest path first,OSPF)路由協(xié)議[23]。Xie等人應(yīng)用模型檢測技術(shù),系統(tǒng)地分析了Google帳戶注冊服務(wù)的安全隱患[24]。

2 TLS協(xié)議簡介

TLS協(xié)議由握手協(xié)議、更改密碼規(guī)范協(xié)議、警告協(xié)議和記錄協(xié)議組成。握手協(xié)議的目的是建立安全的數(shù)據(jù)傳輸信道,在實(shí)際通信過程中,客戶端首先向服務(wù)器端發(fā)送握手請求,服務(wù)器根據(jù)客戶端的握手請求給出響應(yīng)。更改密碼規(guī)范協(xié)議,規(guī)定了更改密碼規(guī)范的具體標(biāo)準(zhǔn),在協(xié)議握手階段結(jié)束后,客戶端向服務(wù)器端提出更改密碼規(guī)范請求,雙方協(xié)商使用的密碼標(biāo)準(zhǔn)后確定會話密鑰。警告協(xié)議規(guī)定了協(xié)議如何處理通信錯誤的情況,其作用是通過警告消息對通信錯誤的終端發(fā)出警告或告知對方通信結(jié)束,中斷連接。記錄協(xié)議用于進(jìn)行數(shù)據(jù)傳輸，在通信雙方握手結(jié)束后,根據(jù)協(xié)商好的會話密鑰對通信報文及握手協(xié)議處理過的數(shù)據(jù)進(jìn)行加密封裝后傳輸。

TLS協(xié)議實(shí)現(xiàn)庫是基于TLS協(xié)議規(guī)范開發(fā)的標(biāo)準(zhǔn)庫或平臺,是實(shí)現(xiàn)TLS協(xié)議的主要產(chǎn)品,實(shí)際中開發(fā)者可以根據(jù)規(guī)范自行開發(fā)相應(yīng)的TLS協(xié)議實(shí)現(xiàn)庫,目前應(yīng)用最多的TLS協(xié)議實(shí)現(xiàn)庫有OpenSSL,GnuTLS,網(wǎng)絡(luò)安全服務(wù)(network security services,NSS),Botan等。TLS協(xié)議執(zhí)行步驟如圖1所示。

圖2 TLS協(xié)議執(zhí)行過程Fig.2 TLS protocol executing process

3 TLS協(xié)議實(shí)現(xiàn)庫的狀態(tài)機(jī)提取

TLS協(xié)議實(shí)現(xiàn)庫的有限狀態(tài)機(jī)(finite state machine,FSM)模型提取,可以通過狀態(tài)機(jī)學(xué)習(xí)算法獲得。狀態(tài)機(jī)學(xué)習(xí)算法能夠假設(shè)協(xié)議的初始狀態(tài)機(jī)模型,根據(jù)目標(biāo)系統(tǒng)的輸入和響應(yīng),不斷修正模型,使其與目標(biāo)系統(tǒng)的差距越來越小。若對于所有的輸入,學(xué)習(xí)到的模型輸出都與目標(biāo)系統(tǒng)完全一致,可以等效認(rèn)為生成的模型與目標(biāo)系統(tǒng)的狀態(tài)機(jī)模型相同。若對模型與目標(biāo)系統(tǒng)的相同輸入對應(yīng)不同的輸出,則可以利用這個輸出作為反饋,構(gòu)造出模型反例,用于模型后續(xù)學(xué)習(xí)。狀態(tài)機(jī)學(xué)習(xí)算法利用反例改進(jìn)得到推斷模型,由于協(xié)議實(shí)現(xiàn)庫的輸出與其輸入和協(xié)議當(dāng)前狀態(tài)有關(guān),因此選擇Mealy狀態(tài)機(jī)對其進(jìn)行建模。

3.1 L*算法狀態(tài)機(jī)學(xué)習(xí)算法

L*算法[25]能夠?qū)W習(xí)給定協(xié)議實(shí)現(xiàn)庫的最小化FSM,包括學(xué)習(xí)者、目標(biāo)系統(tǒng)和預(yù)言機(jī)3種角色與成員查詢、等價查詢兩種查詢。學(xué)習(xí)者的初始知識為Mealy狀態(tài)機(jī)M的輸入字母表I及其對應(yīng)的輸出字母表O。學(xué)習(xí)者通過兩類查詢來得到目標(biāo)系統(tǒng)的狀態(tài)機(jī)模型。

在成員查詢中,學(xué)習(xí)者通過查詢一個字符串并判斷其輸出是否被目標(biāo)系統(tǒng)接受。在等價查詢中,學(xué)習(xí)者查詢一個假設(shè)的Mealy狀態(tài)機(jī)是否與目標(biāo)系統(tǒng)狀態(tài)機(jī)一致,如果一致,目標(biāo)系統(tǒng)回答為“是”。如果不一致,則目標(biāo)系統(tǒng)將響應(yīng)一個使得假設(shè)狀態(tài)機(jī)與目標(biāo)狀態(tài)機(jī)不同輸出序列的消息,稱之為反例。

學(xué)習(xí)者獲得提出假設(shè)信息的狀態(tài)機(jī),并將其作為等價查詢發(fā)給目標(biāo)系統(tǒng),目標(biāo)系統(tǒng)比對正確的規(guī)范,將會響應(yīng)符合目標(biāo)或給出反例,如果模型不相等,根據(jù)不同的響應(yīng),給狀態(tài)機(jī)學(xué)習(xí)算法返回一個反例,狀態(tài)機(jī)學(xué)習(xí)算法根據(jù)得到的反例修改當(dāng)前假設(shè),得到新的預(yù)估模型,重復(fù)這個過程,直到測試中假設(shè)模型和目標(biāo)系統(tǒng)的響應(yīng)完全一致。通過不斷的成員查詢,得到成員確認(rèn),最后學(xué)習(xí)得到協(xié)議的狀態(tài)機(jī)。

3.2 狀態(tài)機(jī)學(xué)習(xí)設(shè)置

為了推斷TLS協(xié)議實(shí)現(xiàn)的Mealy狀態(tài)機(jī),本文基于開源的狀態(tài)機(jī)學(xué)習(xí)框架LearnLib[26]對協(xié)議實(shí)現(xiàn)庫進(jìn)行狀態(tài)機(jī)學(xué)習(xí)。被測試系統(tǒng)(system under test,SUT)對于測試者是黑盒,測試者實(shí)際無法觀測出協(xié)議庫的實(shí)際執(zhí)行狀態(tài),需要通過其響應(yīng)來進(jìn)行推斷,因此狀態(tài)機(jī)學(xué)習(xí)過程中LearnLib需要相應(yīng)地給出輸入及響應(yīng)消息列表,同時能夠重置SUT的初始狀態(tài)機(jī)。

LearnLib能夠通過對協(xié)議交互消息進(jìn)行發(fā)送和讀取SUT的響應(yīng)消息,并不斷重置SUT的初始狀態(tài),根據(jù)SUT收到的消息及其實(shí)際響應(yīng)的消息序列,為狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)移關(guān)系建立預(yù)估模型假設(shè),并觀測實(shí)際狀態(tài)機(jī)是否與預(yù)估模型對相同的輸入產(chǎn)生等效的響應(yīng)。

LearnLib中規(guī)定通過設(shè)定狀態(tài)機(jī)的輸入字母表,能夠?qū)⒔换サ膮f(xié)議消息抽象映射為特定字符串,本文實(shí)驗(yàn)設(shè)定輸入輸出字母表為:客戶端握手、客戶端證書、完成、客戶端密鑰交換、客戶端證書驗(yàn)證、更改密碼規(guī)范、應(yīng)用數(shù)據(jù)等報文。在實(shí)際交互中通過服務(wù)端和客服端的響應(yīng)構(gòu)建對應(yīng)的轉(zhuǎn)移關(guān)系。同時,由于警告協(xié)議中的消息格式只在響應(yīng)中出現(xiàn),因此還需要在輸出表中加入:空報文、解密失敗和連接中斷的對應(yīng)響應(yīng)字符串。輸入輸出消息及其對應(yīng)字母表如表1所示。

表1 輸入輸出字母表Table 1 Input and output alphabet

4 協(xié)議狀態(tài)機(jī)的安全屬性建模

NuSMV模型由一組有限變量與轉(zhuǎn)移函數(shù)一起定義。在規(guī)范中的時態(tài)邏輯,利用線性時態(tài)邏輯可以在特定的模型上進(jìn)行檢測,并在給定規(guī)范不正確時生成反例。將TLS協(xié)議的RFC規(guī)范進(jìn)行安全屬性提取[27],可以將要驗(yàn)證的屬性分為3類。

(1) 安全屬性:這是每層協(xié)議主要安全目標(biāo)的基礎(chǔ),用于描述通信的安全交互規(guī)范,以進(jìn)行必要的身份認(rèn)證并保護(hù)通信的機(jī)密性,如中間人攻擊和拒絕服務(wù)攻擊。

(2) 密鑰交換屬性:用于衡量創(chuàng)建新的會話密鑰以檢查系統(tǒng)的前向機(jī)密性狀態(tài),并確保密鑰的新鮮性。

(3) 功能屬性:是RFC規(guī)范中應(yīng)該和必須有的功能,將對協(xié)議安全產(chǎn)生影響。

模型檢測難以對協(xié)議實(shí)現(xiàn)代碼進(jìn)行直接的模型檢測,本文通過對受測系統(tǒng)的抽象模型屬性進(jìn)行檢測。因此，當(dāng)對提取到的模型檢測結(jié)果進(jìn)行解釋時應(yīng)當(dāng)注意其抽象程度。最后,如果反例不正確,那么就證明了學(xué)習(xí)出來的模型不正確。

4.1 安全屬性建模

在TLS協(xié)議中,上層服務(wù)依賴于底層提供的安全保證,所以只有當(dāng)?shù)讓影踩淹晟坪蟛拍軕?yīng)用高層服務(wù)。例如,只有當(dāng)密鑰交換完成并在傳輸層建立了安全信道之后，才能進(jìn)行認(rèn)證服務(wù),否則認(rèn)證服務(wù)將在未加密的信道上運(yùn)行。因此,認(rèn)證服務(wù)在沒有成功進(jìn)行密鑰交換時是不能進(jìn)行的。

密鑰交換包含3個必須執(zhí)行的步驟,但這些步驟可能會與其他動作產(chǎn)生交織。一次成功認(rèn)證的前提是一次成功的密鑰交換。可以通過輸入與輸出變量的值來判斷密鑰交換步驟是否成功完成。通過謂詞AuthReq來表示成功的發(fā)送認(rèn)證請求。定義O為once算子通過這些原則,定義：

屬性1

G(AuthReq->
O((inp&=ClientHello&out=NoRESP)&
O((inp&=KeyEX&out=ChangeCipherSpec))))

除了安全連接外,記錄協(xié)議會認(rèn)為連接后的客戶端已經(jīng)經(jīng)過認(rèn)證。通過認(rèn)證機(jī)制確保認(rèn)證了的客戶端已經(jīng)提供有效的憑據(jù)。為了確保協(xié)議實(shí)現(xiàn)的安全,必須保證狀態(tài)轉(zhuǎn)移提供有效憑據(jù)才能由未認(rèn)證轉(zhuǎn)移到認(rèn)證狀態(tài)的路徑。那么其對應(yīng)的協(xié)議行為是當(dāng)輸入為ChangeCipherSpec時,對應(yīng)輸出不會失敗,則一個已認(rèn)證狀態(tài)必然是信道已經(jīng)成功建立,其對應(yīng)謂詞為OpenChannel。提供有效及無效的憑據(jù)對應(yīng)的輸出為SUCCESS和FAILURE，可定義：

屬性2

G(OpenChannel->
inp=ChangeCipherSpec&out!=FAILURE)

4.2 重協(xié)商屬性

在TLS協(xié)議的RFC文檔中,密鑰重協(xié)商是在協(xié)議的所有狀態(tài)中都允許進(jìn)行的,同時,其執(zhí)行以后不影響更高層的操作。現(xiàn)在考慮通用的協(xié)議狀態(tài),預(yù)認(rèn)證狀態(tài)(已發(fā)出認(rèn)證請求,但還未認(rèn)證)以及已認(rèn)證狀態(tài)。這兩種狀態(tài)可以映射到學(xué)習(xí)到的狀態(tài)機(jī)模型的多個狀態(tài)中去，形式化定義為兩種屬性。可以通過謂詞reAuthReq表示已成功發(fā)出認(rèn)證請求后再次發(fā)出認(rèn)證請求,此時已經(jīng)進(jìn)入預(yù)認(rèn)證狀態(tài)。接著可以成功接受重協(xié)商密鑰的輸入,直到連接斷開或已經(jīng)認(rèn)證,定義：

屬性3

G(reAuthReq->
X((inp=ClientHello->out=ChangeCipherSpec) &
X((inp=KeyEX->out=NEWKEYS) &
X(int=NEWKEYS->out=NoRESP))))W
(connLost|hasAuth))

4.3 功能屬性

除了以上屬性外,還有幾種屬性可以由RFC文檔中歸納得到。首先是DISCONNECT輸出。通過RFC規(guī)定一節(jié)點(diǎn)發(fā)出這個謂詞后,一定不再接受或發(fā)送任何信息。然而此時無法判斷在實(shí)際代碼中服務(wù)器是否真的停止接受消息,但是可以檢測服務(wù)器在發(fā)出ConnectionClosed消息后是否還發(fā)送消息。因此可以定義：

屬性4

G(out=ConnectionClosed->
XG(out!=Empty))

描述發(fā)出ConnectionClosed消息后的輸出是否符合RFC的規(guī)范。RFC文檔中規(guī)定在發(fā)送KeyEX消息后,節(jié)點(diǎn)必須不再(MUSTNOT)發(fā)送另外的KeyEX,直到發(fā)送一個NEWKEYS消息為止。定義：

屬性5

G(out=KeyEX->
X((out!=KeyEX)WreceivedNewKeys)

RFC聲明,服務(wù)器在認(rèn)證成功和建立信道后不能重新進(jìn)行密鑰交換。定義：

屬性6

G((HasAuth)->XG(!Finished))

RFC聲明,服務(wù)器在認(rèn)證成功后將保持持續(xù)通信直至?xí)捊Y(jié)束,同時應(yīng)該(SHOULD)忽視再次認(rèn)證的請求。定義：

屬性7

G(out=SUCCESS->
X(AuthReq->out=NoRESP)WendCondition)

對于認(rèn)證層的RFC,如果服務(wù)器拒絕認(rèn)證請求,必須(MUST)響應(yīng)FAILURE消息，被拒絕的請求由謂詞invalidAuthReq構(gòu)成。在有效憑據(jù)的請求中,NEWKEYS必須(MUST)只能發(fā)送一次。因此,可以定義兩個屬性,第一個屬性中,即使hasReqAuth可能在認(rèn)證成功后依然成立,但是由于只對認(rèn)證之前的結(jié)論有用,因此利用O算子，定義：

屬性8

G((hasAuth!O(out=SUCCESS))->
(invalidAuthReq->out=FAILURE)W.
(out=SUCCESS|endCondition))

5 實(shí)驗(yàn)及結(jié)果分析

本文研究了兩種TLS協(xié)議實(shí)現(xiàn)庫OpenSSL 1.0.1g服務(wù)器端及NSS 3.17.4的有限狀態(tài)機(jī)模型,并對其狀態(tài)機(jī)模型進(jìn)行模型檢測，驗(yàn)證是否可滿足聲明的安全屬性。

5.1 狀態(tài)機(jī)學(xué)習(xí)

為了推斷TLS協(xié)議實(shí)現(xiàn)的有限狀態(tài)機(jī),本文使用開源的狀態(tài)機(jī)學(xué)習(xí)框架LearnLib,對TLS協(xié)議實(shí)現(xiàn)庫使用改進(jìn)的L*算法得到協(xié)議實(shí)現(xiàn)庫狀態(tài)機(jī)。分別對TLS協(xié)議實(shí)現(xiàn)庫OpenSSL 1.0.1g和NSS 3.17.4進(jìn)行狀態(tài)機(jī)學(xué)習(xí),圖3和圖4分別為學(xué)習(xí)到的OpenSSL 1.0.1g和NSS 3.17.4的狀態(tài)機(jī)模型,這些協(xié)議模型體現(xiàn)了在協(xié)議實(shí)際運(yùn)行中的狀態(tài)轉(zhuǎn)移關(guān)系。可以看出,在協(xié)議的執(zhí)行過程中,會對相應(yīng)的狀態(tài)轉(zhuǎn)移做出不同響應(yīng)。接下來對學(xué)習(xí)到的協(xié)議實(shí)現(xiàn)庫的正常交互進(jìn)行一個簡單描述。

圖3 通過狀態(tài)機(jī)學(xué)習(xí)算法得到的OpenSSL 1.0.1g狀態(tài)機(jī)Fig.3 OpenSSL 1.0.1g state machine obtained by state machine learning algorithm

從圖3可以看到,OpenSSL 1.0.1g正常交互時的狀態(tài)轉(zhuǎn)移為虛線條所示,服務(wù)器在0狀態(tài)接收到客戶端發(fā)出的握手消息后給出服務(wù)器響應(yīng)進(jìn)入狀態(tài)1并響應(yīng)客戶端握手,在收到客戶端密鑰交換消息后進(jìn)入狀態(tài)4,客戶端與服務(wù)器端握手成功后進(jìn)入給出更改密碼規(guī)范消息,服務(wù)器端進(jìn)入狀態(tài)7,與客戶端建立信道后進(jìn)行狀態(tài)2,此后客戶端進(jìn)行加密通信。

從圖4可以看到，NSS 3.17.4正常協(xié)議交互時的狀態(tài)轉(zhuǎn)移為虛線所示路徑,服務(wù)器在0狀態(tài)接收到客戶端發(fā)出的握手消息后給出服務(wù)器響應(yīng)進(jìn)入狀態(tài)1,并在收到客戶端密鑰交換消息后進(jìn)入狀態(tài)2。

圖4 學(xué)習(xí)到的NSS 3.17.4狀態(tài)機(jī)Fig.4 NSS 3.17.4 state machine leamed

5.2 模型檢測檢驗(yàn)結(jié)果

NuSMV模型由一組有限變量與遷移函數(shù)一起定義。在規(guī)范中的線性時態(tài)邏輯,可以在特定的模型上進(jìn)行檢測,并在給定規(guī)范不正確時,生成反例。

通過學(xué)習(xí)到的狀態(tài)機(jī)模型作為NuSMV的輸入模型。該模型共有3個變量,分別對應(yīng)為輸入、輸出和狀態(tài)。

這里實(shí)際上并不是對協(xié)議實(shí)現(xiàn)代碼進(jìn)行直接的模型檢測,而是對受測系統(tǒng)抽象模型的屬性進(jìn)行檢測。因此,當(dāng)對學(xué)習(xí)到的模型檢測結(jié)果進(jìn)行解釋時應(yīng)當(dāng)注意這一點(diǎn)。其次，即使某些屬性對于抽象模型不成立,也需要對模型檢測器生成的反例在實(shí)際代碼上進(jìn)行運(yùn)行，來驗(yàn)證此反例是否在代碼上存在實(shí)際運(yùn)行。如果反例不正確,那么就證明了學(xué)習(xí)出來的模型不正確。

5.3 狀態(tài)機(jī)模型分析

對GnuTLS和OpenSSL驗(yàn)證的結(jié)果如表2所示。

表2 模型檢測結(jié)果Table 2 Model checking results

從表2發(fā)現(xiàn)，OpenSSL和NSS都不滿足屬性4,這是因?yàn)檫@兩個協(xié)議服務(wù)器端實(shí)現(xiàn)在會話結(jié)束后會發(fā)送異常消息(Unimpl),而不是按照RFC規(guī)范直接停止會話。在OpenSSL中,密鑰重協(xié)商屬性不滿足,對其進(jìn)行分析,發(fā)現(xiàn)圖3中加粗路徑為其攻擊路徑,這是一個經(jīng)典的EarlyCCS注入攻擊(CVE-2014-0224)。該攻擊路徑為:在TLS協(xié)議握手過程中,攻擊者向處于0狀態(tài)的服務(wù)器發(fā)送客戶端握手時,服務(wù)器響應(yīng)完成并進(jìn)入1狀態(tài)后立即發(fā)送一個更改密碼規(guī)范消息,此時雙方還沒有生成主密鑰,由于服務(wù)器在收到更改密碼規(guī)范消息時并沒有檢查自己的握手狀態(tài)機(jī)處于哪一步驟,接收到該消息后服務(wù)器進(jìn)入狀態(tài)6,此時服務(wù)器默認(rèn)使用一個空值代替主密鑰,并計算雙方會話密鑰,進(jìn)入狀態(tài)9。由于OpenSSL的實(shí)現(xiàn)庫原因,在一個回話中只要已經(jīng)經(jīng)過了密鑰的計算,以后就不會再次計算密鑰,雙方握手成功,服務(wù)器與攻擊者建立信道,服務(wù)器進(jìn)入狀態(tài)12,并開始進(jìn)行消息傳遞,服務(wù)器遷移至狀態(tài)2,在不安全的信道上傳輸信息。可以認(rèn)為,通過模型檢測方法,能夠有效發(fā)現(xiàn)協(xié)議實(shí)現(xiàn)中狀態(tài)機(jī)模型存在的漏洞和不足。

6 結(jié) 論

本文研究針對模型檢測技術(shù)不能直接應(yīng)用于協(xié)議實(shí)現(xiàn)庫分析的問題,對協(xié)議實(shí)現(xiàn)庫采用狀態(tài)機(jī)學(xué)習(xí)技術(shù),提取了協(xié)議實(shí)現(xiàn)庫的狀態(tài)機(jī)模型,同時對照RFC中的安全條件建立協(xié)議安全屬性模型,并通過模型檢測方法,利用形式化模型檢測工具NuSMV,完成對TLS協(xié)議實(shí)現(xiàn)庫的形式化分析,用于尋找TLS協(xié)議實(shí)現(xiàn)庫的邏輯漏洞。本研究將模型學(xué)習(xí)與模型檢查相結(jié)合，分析兩種TLS 1.2實(shí)現(xiàn)。研究執(zhí)行了基于狀態(tài)機(jī)學(xué)習(xí)的目標(biāo)系統(tǒng)黑盒測試，推斷狀態(tài)機(jī)模型,并提取TLS協(xié)議相關(guān)規(guī)范中的屬性,使用模型檢測技術(shù)自動化分析協(xié)議狀態(tài)機(jī)模型。通過分析推斷狀態(tài)機(jī)揭示系統(tǒng)的內(nèi)部結(jié)構(gòu),所得的模型檢測結(jié)果可以發(fā)現(xiàn)協(xié)議規(guī)范與協(xié)議實(shí)現(xiàn)之間的差異,以便在未來版本中對其進(jìn)行改進(jìn)。實(shí)驗(yàn)證明，所提方法能夠有效分析TLS協(xié)議實(shí)現(xiàn)庫的狀態(tài)機(jī)模型,找到協(xié)議實(shí)現(xiàn)庫存在的邏輯漏洞及與規(guī)范不一致的缺陷,包括導(dǎo)致服務(wù)器異常的錯誤交互以及某些違反規(guī)范的行為在內(nèi)的協(xié)議實(shí)現(xiàn)庫邏輯漏洞。

將來所提方法也可以應(yīng)用于分析分解其他協(xié)議實(shí)現(xiàn),例如物聯(lián)網(wǎng)中的認(rèn)證協(xié)議或通信協(xié)議實(shí)現(xiàn),這是該方法的一大優(yōu)勢。總的來說,本文研究擴(kuò)展了安全協(xié)議分析的安全性分析方法，并為其應(yīng)用場景做了有效補(bǔ)充。