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

畢 興,唐朝京

(1.國(guó)防科技大學(xué)前沿交叉學(xué)科學(xué)院,湖南 長(zhǎng)沙 410073;2.國(guó)防科技大學(xué)電子科學(xué)學(xué)院,湖南 長(zhǎng)沙 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)庫(kù)作為TLS協(xié)議的應(yīng)用載體,有許多對(duì)于協(xié)議的攻擊是針對(duì)TLS協(xié)議實(shí)現(xiàn)庫(kù)進(jìn)行的,如幸運(yùn)13漏洞(Lucky13)[2]、密文填塞攻擊(Padding-Oracle)[3]和貴賓犬攻擊(Poodle)[4]。但是,這些攻擊是對(duì)協(xié)議實(shí)現(xiàn)而非協(xié)規(guī)范的攻擊,并沒有方法能夠有效發(fā)現(xiàn)協(xié)議實(shí)現(xiàn)庫(kù)存在的邏輯漏洞。

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

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

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

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

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

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

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

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

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

2 TLS協(xié)議簡(jiǎn)介

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

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

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

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

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

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

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

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

學(xué)習(xí)者獲得提出假設(shè)信息的狀態(tài)機(jī),并將其作為等價(jià)查詢發(fā)給目標(biāo)系統(tǒng),目標(biāo)系統(tǒng)比對(duì)正確的規(guī)范,將會(huì)響應(yīng)符合目標(biāo)或給出反例,如果模型不相等,根據(jù)不同的響應(yīng),給狀態(tài)機(jī)學(xué)習(xí)算法返回一個(gè)反例,狀態(tài)機(jī)學(xué)習(xí)算法根據(jù)得到的反例修改當(dāng)前假設(shè),得到新的預(yù)估模型,重復(fù)這個(gè)過(guò)程,直到測(cè)試中假設(shè)模型和目標(biāo)系統(tǒng)的響應(yīng)完全一致。通過(guò)不斷的成員查詢,得到成員確認(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]對(duì)協(xié)議實(shí)現(xiàn)庫(kù)進(jìn)行狀態(tài)機(jī)學(xué)習(xí)。被測(cè)試系統(tǒng)(system under test,SUT)對(duì)于測(cè)試者是黑盒,測(cè)試者實(shí)際無(wú)法觀測(cè)出協(xié)議庫(kù)的實(shí)際執(zhí)行狀態(tài),需要通過(guò)其響應(yīng)來(lái)進(jìn)行推斷,因此狀態(tài)機(jī)學(xué)習(xí)過(guò)程中LearnLib需要相應(yīng)地給出輸入及響應(yīng)消息列表,同時(shí)能夠重置SUT的初始狀態(tài)機(jī)。

LearnLib能夠通過(guò)對(duì)協(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è),并觀測(cè)實(shí)際狀態(tài)機(jī)是否與預(yù)估模型對(duì)相同的輸入產(chǎn)生等效的響應(yīng)。

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

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

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

NuSMV模型由一組有限變量與轉(zhuǎn)移函數(shù)一起定義。在規(guī)范中的時(shí)態(tài)邏輯,利用線性時(shí)態(tài)邏輯可以在特定的模型上進(jìn)行檢測(cè),并在給定規(guī)范不正確時(shí)生成反例。將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)建新的會(huì)話密鑰以檢查系統(tǒng)的前向機(jī)密性狀態(tài),并確保密鑰的新鮮性。

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

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

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)行密鑰交換時(shí)是不能進(jìn)行的。

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

屬性1

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

除了安全連接外,記錄協(xié)議會(huì)認(rèn)為連接后的客戶端已經(jīng)經(jīng)過(guò)認(rèn)證。通過(guò)認(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)的路徑。那么其對(duì)應(yīng)的協(xié)議行為是當(dāng)輸入為ChangeCipherSpec時(shí),對(duì)應(yīng)輸出不會(huì)失敗,則一個(gè)已認(rèn)證狀態(tài)必然是信道已經(jīng)成功建立,其對(duì)應(yīng)謂詞為OpenChannel。提供有效及無(wú)效的憑據(jù)對(duì)應(yīng)的輸出為SUCCESS和FAILURE，可定義：

屬性2

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

4.2 重協(xié)商屬性

在TLS協(xié)議的RFC文檔中,密鑰重協(xié)商是在協(xié)議的所有狀態(tài)中都允許進(jìn)行的,同時(shí),其執(zhí)行以后不影響更高層的操作?，F(xiàn)在考慮通用的協(xié)議狀態(tài),預(yù)認(rèn)證狀態(tài)(已發(fā)出認(rèn)證請(qǐng)求,但還未認(rèn)證)以及已認(rèn)證狀態(tài)。這兩種狀態(tài)可以映射到學(xué)習(xí)到的狀態(tài)機(jī)模型的多個(gè)狀態(tài)中去，形式化定義為兩種屬性?？梢酝ㄟ^(guò)謂詞reAuthReq表示已成功發(fā)出認(rèn)證請(qǐng)求后再次發(fā)出認(rèn)證請(qǐng)求,此時(shí)已經(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輸出。通過(guò)RFC規(guī)定一節(jié)點(diǎn)發(fā)出這個(gè)謂詞后,一定不再接受或發(fā)送任何信息。然而此時(shí)無(wú)法判斷在實(shí)際代碼中服務(wù)器是否真的停止接受消息,但是可以檢測(cè)服務(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ā)送一個(gè)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é)束,同時(shí)應(yīng)該(SHOULD)忽視再次認(rèn)證的請(qǐng)求。定義：

屬性7

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

對(duì)于認(rèn)證層的RFC,如果服務(wù)器拒絕認(rèn)證請(qǐng)求,必須(MUST)響應(yīng)FAILURE消息，被拒絕的請(qǐng)求由謂詞invalidAuthReq構(gòu)成。在有效憑據(jù)的請(qǐng)求中,NEWKEYS必須(MUST)只能發(fā)送一次。因此,可以定義兩個(gè)屬性,第一個(gè)屬性中,即使hasReqAuth可能在認(rèn)證成功后依然成立,但是由于只對(duì)認(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)庫(kù)OpenSSL 1.0.1g服務(wù)器端及NSS 3.17.4的有限狀態(tài)機(jī)模型,并對(duì)其狀態(tài)機(jī)模型進(jìn)行模型檢測(cè)，驗(yàn)證是否可滿足聲明的安全屬性。

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

為了推斷TLS協(xié)議實(shí)現(xiàn)的有限狀態(tài)機(jī),本文使用開源的狀態(tài)機(jī)學(xué)習(xí)框架LearnLib,對(duì)TLS協(xié)議實(shí)現(xiàn)庫(kù)使用改進(jìn)的L*算法得到協(xié)議實(shí)現(xiàn)庫(kù)狀態(tài)機(jī)。分別對(duì)TLS協(xié)議實(shí)現(xiàn)庫(kù)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í)行過(guò)程中,會(huì)對(duì)相應(yīng)的狀態(tài)轉(zhuǎn)移做出不同響應(yīng)。接下來(lái)對(duì)學(xué)習(xí)到的協(xié)議實(shí)現(xiàn)庫(kù)的正常交互進(jìn)行一個(gè)簡(jiǎn)單描述。

圖3 通過(guò)狀態(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正常交互時(shí)的狀態(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é)議交互時(shí)的狀態(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 模型檢測(cè)檢驗(yàn)結(jié)果

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

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

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

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

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

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

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

6 結(jié) 論

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

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