基于狀態(tài)機(jī)學(xué)習(xí)算法的TLS實(shí)現(xiàn)庫(kù)安全性分析

畢 興,唐朝京

(國(guó)防科技大學(xué)電子科學(xué)學(xué)院,湖南 長(zhǎng)沙 410073)

0 引 言

傳輸層安全(transport layer security,TLS)協(xié)議用于為網(wǎng)絡(luò)提供安全及數(shù)據(jù)完整性保障。作為最廣泛使用的安全協(xié)議之一,其安全性引起了業(yè)界的高度關(guān)注,各類研究者及攻擊者對(duì)其進(jìn)行了細(xì)致深入的分析,它經(jīng)歷了從密碼學(xué)攻擊[1-3]到協(xié)議實(shí)現(xiàn)庫(kù)漏洞[4-6]等一系列安全威脅。其中TLS協(xié)議實(shí)現(xiàn)庫(kù)作為TLS協(xié)議的應(yīng)用載體,也被看作一個(gè)實(shí)施網(wǎng)絡(luò)攻擊的重點(diǎn)。因此,對(duì)其安全性的分析,有著重大而現(xiàn)實(shí)的意義。

傳統(tǒng)的TLS協(xié)議實(shí)現(xiàn)庫(kù)安全性分析大多立足于程序分析的角度,重在尋找實(shí)現(xiàn)庫(kù)的軟件脆弱性,該方法無(wú)法發(fā)現(xiàn)協(xié)議實(shí)現(xiàn)中存在的邏輯缺陷。另一方面,通過(guò)對(duì)協(xié)議規(guī)范的形式化安全分析又不足以保證其實(shí)現(xiàn)庫(kù)的安全性。

為了描述TLS或一般安全協(xié)議的實(shí)現(xiàn)庫(kù),可以使用有限狀態(tài)機(jī)指定發(fā)送和接收的消息的可能序列。使用狀態(tài)機(jī)學(xué)習(xí)技術(shù),能夠僅依賴于黑盒測(cè)試,不需要知道協(xié)議規(guī)范,就可以從協(xié)議實(shí)現(xiàn)庫(kù)中提取狀態(tài)機(jī)。通過(guò)分析這些狀態(tài)機(jī),可以發(fā)現(xiàn)協(xié)議的狀態(tài)遷移中存在的邏輯錯(cuò)誤。

協(xié)議狀態(tài)機(jī)學(xué)習(xí)可以分為被動(dòng)式學(xué)習(xí)和主動(dòng)式學(xué)習(xí)。文獻(xiàn)[7]提出了第一個(gè)多項(xiàng)式復(fù)雜度的摩爾狀態(tài)機(jī)學(xué)習(xí)算法,稱作L*算法。它是最經(jīng)典的狀態(tài)機(jī)學(xué)習(xí)算法,用來(lái)推斷最小化的確定的有限狀態(tài)機(jī)。被動(dòng)式學(xué)習(xí)技術(shù)通過(guò)觀測(cè)網(wǎng)絡(luò)中的流量來(lái)推斷協(xié)議的狀態(tài)機(jī),文獻(xiàn)[8]通過(guò)被動(dòng)學(xué)習(xí)的模型對(duì)網(wǎng)絡(luò)進(jìn)行了模糊測(cè)試。文獻(xiàn)[9]通過(guò)狀態(tài)機(jī)模型形式化分析了銀行卡的安全性。文獻(xiàn)[10]利用狀態(tài)機(jī)學(xué)習(xí)技術(shù)對(duì)TLS協(xié)議實(shí)現(xiàn)庫(kù)進(jìn)行了主機(jī)名驗(yàn)證分析,文獻(xiàn)[11]通過(guò)模型檢測(cè)方法分析了TLS協(xié)議的狀態(tài)機(jī)。

文獻(xiàn)[12]介紹了基于特征集的狀態(tài)機(jī)學(xué)習(xí)算法W算法,其通過(guò)狀態(tài)機(jī)的特征集構(gòu)造測(cè)試序列對(duì)目標(biāo)系統(tǒng)進(jìn)行測(cè)試。文獻(xiàn)[13]對(duì)W方法進(jìn)行了改進(jìn),提出了Wp方法,該方法通過(guò)狀態(tài)機(jī)的部分特征集構(gòu)造測(cè)試序列,通常此測(cè)試序列集小于W方法生成的測(cè)試序列集。但是此類方法并未考慮目標(biāo)系統(tǒng)自身的特性。本文通過(guò)套接字約簡(jiǎn),利用協(xié)議連接中交互消息的分類,對(duì)多余的測(cè)試序列進(jìn)行了剔除;同時(shí)利用檢查點(diǎn)算法,構(gòu)造測(cè)試用例的前綴樹,加速狀態(tài)機(jī)學(xué)習(xí)過(guò)程。達(dá)到了降低測(cè)試序列數(shù)量,減少狀態(tài)機(jī)學(xué)習(xí)時(shí)間,提高狀態(tài)機(jī)學(xué)習(xí)效率的目的。最后,對(duì)兩類TLS實(shí)現(xiàn)庫(kù)進(jìn)行了測(cè)試,并通過(guò)學(xué)習(xí)到的狀態(tài)機(jī)發(fā)現(xiàn)了一個(gè)協(xié)議庫(kù)的邏輯漏洞。

1 TLS協(xié)議

TLS的設(shè)計(jì)目標(biāo)是在傳輸層上構(gòu)建一個(gè)安全傳輸層,用來(lái)確保網(wǎng)絡(luò)通信中的3種主要安全性質(zhì):可靠性,認(rèn)證用戶和服務(wù)器,確保數(shù)據(jù)發(fā)送到正確的客戶機(jī)和服務(wù)器;機(jī)密性,加密數(shù)據(jù)以防止數(shù)據(jù)泄漏;完整性,維護(hù)數(shù)據(jù)的完整性,確保數(shù)據(jù)在傳輸過(guò)程中不被改變。

握手協(xié)議是TLS是最重要的部分,其主要作用是在客戶端和服務(wù)器之間建立安全的數(shù)據(jù)傳輸信道。更改密碼規(guī)范協(xié)議用于發(fā)送更改密碼規(guī)范消息。警告協(xié)議的作用是,如果通信中發(fā)現(xiàn)連接或傳輸錯(cuò)誤的一方,則通過(guò)警告協(xié)議向另一方發(fā)出警告;此外還可以在數(shù)據(jù)傳輸完成后,用于通知另一方斷開連接。警告協(xié)議由警告消息實(shí)現(xiàn)。記錄協(xié)議是TLS中用于數(shù)據(jù)傳輸?shù)膮f(xié)議,其通信的報(bào)文及握手協(xié)議處理過(guò)的數(shù)據(jù)都由記錄協(xié)議封裝為記錄報(bào)文并進(jìn)行傳輸。

TLS執(zhí)行步驟如圖1所示。

圖1 TLS執(zhí)行過(guò)程Fig.1 TLS executing procedure

步驟1客戶端向服務(wù)端發(fā)送服務(wù)器握手消息,這個(gè)消息里包括客戶端生成的隨機(jī)數(shù)、客戶端支持的加密套件等信息。

步驟2服務(wù)器向客戶端發(fā)送服務(wù)器消息,服務(wù)器在客戶端支持的密鑰組件中里選擇一份加密套件,該套件決定了后續(xù)加密和生成摘要時(shí)采用的算法,另外還會(huì)生成一份隨機(jī)數(shù)用于后續(xù)認(rèn)證。同時(shí)將服務(wù)器的證書發(fā)送給客戶端驗(yàn)證。

步驟3客戶端驗(yàn)證服務(wù)器證書通過(guò)后取出證書中的公鑰,將自身證書發(fā)送給服務(wù)器,通知服務(wù)器開始使用加密方式發(fā)送報(bào)文和計(jì)算消息認(rèn)證碼,并對(duì)之前握手的消息用主密鑰加密后傳輸。

步驟4TLS服務(wù)器驗(yàn)證客戶端證書后,發(fā)送更改密碼規(guī)范消息,確認(rèn)使用的密碼套件。

步驟5通信雙方以握手過(guò)程中協(xié)商好的安全參數(shù),進(jìn)行安全的應(yīng)用數(shù)據(jù)傳輸。

TLS實(shí)現(xiàn)庫(kù)是由開發(fā)者基于TLS協(xié)議規(guī)范開發(fā)的具體使用TLS協(xié)議進(jìn)行操作的標(biāo)準(zhǔn)庫(kù)或平臺(tái)。當(dāng)前應(yīng)用廣泛的TLS協(xié)議實(shí)現(xiàn)庫(kù)有OpenSSl,GnuTLS,Botan等。

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

狀態(tài)機(jī)學(xué)習(xí)算法試圖學(xué)習(xí)目標(biāo)系統(tǒng)的模型。通過(guò)選擇輸入查詢目標(biāo)系統(tǒng),根據(jù)目標(biāo)系統(tǒng)的響應(yīng),最終推斷出目標(biāo)系統(tǒng)的模型。如果模型是正確的,即其與目標(biāo)系統(tǒng)輸出一致,學(xué)習(xí)算法將認(rèn)為生成的模型與目標(biāo)系統(tǒng)的模型相同并停機(jī)。另一方面,如果模型不正確,目標(biāo)系統(tǒng)和模型的輸入產(chǎn)生不同的輸出,根據(jù)這個(gè)不同的輸出可以構(gòu)造出反例。學(xué)習(xí)算法利用反例改進(jìn)推斷所得模型。重復(fù)這個(gè)流程直到學(xué)習(xí)算法產(chǎn)生正確的模型。由于協(xié)議實(shí)現(xiàn)庫(kù)的輸出不僅與其輸入有關(guān),同時(shí)也與其當(dāng)前狀態(tài)有關(guān),因此選擇米利狀態(tài)機(jī)描述TLS實(shí)現(xiàn)庫(kù)的狀態(tài)機(jī)模型。

2.1 米利狀態(tài)機(jī)

米利狀態(tài)機(jī)是一類有限狀態(tài)機(jī),可以形式化地描述為一個(gè)六元組M=,其中I是一組有限的輸入集；O是一組有限的輸出集；Q是一組有限的狀態(tài)集；q0∈Q是初始狀態(tài)；δ:Q×I→Q是遷移函數(shù)；λ:Q×I→O是輸出函數(shù)。根據(jù)定義,輸出函數(shù)λ滿足

λ(q,ε)=ε,λ(q,iσ)=λ(q,i)λ(δ(q,i),σ)

其輸出依賴于狀態(tài)機(jī)當(dāng)前狀態(tài)和輸入。米利狀態(tài)機(jī)的行為可以通過(guò)函數(shù)來(lái)定義,其中AM(σ)=λ(q0,σ)。當(dāng)且僅當(dāng)AM=AN時(shí),狀態(tài)機(jī)M和N稱為等價(jià)的,記做M≈N。

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

狀態(tài)機(jī)學(xué)習(xí)算法分為主動(dòng)學(xué)習(xí)算法和被動(dòng)學(xué)習(xí)算法,本文采用文獻(xiàn)[14]中的主動(dòng)學(xué)習(xí)算法,學(xué)習(xí)者(L*)算法。

L*算法用于學(xué)習(xí)目標(biāo)系統(tǒng)的有限狀態(tài)機(jī)(finite state machine,FSM),在學(xué)習(xí)算法中,包括了學(xué)習(xí)者、指導(dǎo)者、預(yù)言機(jī)3種角色和成員查詢、等價(jià)查詢兩種查詢。初始狀態(tài)下,學(xué)習(xí)者的初始知識(shí)為米利狀態(tài)機(jī)M的輸入字母表I以及輸出字母表O。指導(dǎo)者的知識(shí)為整個(gè)狀態(tài)機(jī),學(xué)習(xí)者通過(guò)兩類查詢來(lái)學(xué)習(xí)狀態(tài)機(jī)模型。

成員查詢:這類查詢中,學(xué)習(xí)者查詢一個(gè)字符串s以及其輸出是否與目標(biāo)系統(tǒng)一致,即σ∈I*,指導(dǎo)者通過(guò)AM(σ)中的輸出序列響應(yīng)。

等價(jià)查詢:這類查詢中,學(xué)習(xí)者查詢一個(gè)假設(shè)的米利狀態(tài)機(jī)H是否正確,即是否H≈M。如果正確,預(yù)言機(jī)回答為肯定:如果不正確,它會(huì)給出一個(gè)反例C,反例C是引起兩個(gè)狀態(tài)機(jī)不同輸出序列的消息σ∈I*,其滿足AH(σ)≠AM(σ)。

學(xué)習(xí)者向指導(dǎo)者提出查詢獲得狀態(tài)機(jī)的信息,指導(dǎo)者回答學(xué)習(xí)者的成員查詢,預(yù)言機(jī)響應(yīng)等價(jià)確認(rèn)查詢判斷該狀態(tài)機(jī)能否正確代表協(xié)議規(guī)范中的狀態(tài)機(jī)。通過(guò)這三者可以構(gòu)建一個(gè)觀測(cè)表 。其中S是狀態(tài)標(biāo)記集,Exp為測(cè)試集,Ot為表坐標(biāo)的真值映射。學(xué)習(xí)者獲得信息提出假設(shè)的狀態(tài)機(jī),并將此狀態(tài)機(jī)作為等價(jià)查詢發(fā)給指導(dǎo)者,指導(dǎo)者比對(duì)正確的規(guī)范,將會(huì)響應(yīng)符合或給出反例。若給出反例,那么將該反例C及其前綴加入表中狀態(tài)集S并重復(fù)該算法;若觀測(cè)表為連續(xù)且封閉的,則可以定義相應(yīng)的狀態(tài)機(jī)。

2.3 改進(jìn)的測(cè)試序列生成算法

實(shí)際分析的目標(biāo)系統(tǒng)稱為被測(cè)系統(tǒng)(system under test,SUT)。在狀態(tài)機(jī)推斷中,并不知道協(xié)議實(shí)現(xiàn)庫(kù)實(shí)際的狀態(tài)機(jī),此時(shí)需要構(gòu)造測(cè)試序列作為等價(jià)查詢對(duì)SUT進(jìn)行測(cè)試以得到反例。

2.3.1 測(cè)試序列生成算法

利用Wp方法生成測(cè)試序列,該方法由兩個(gè)階段組成:

第一階段計(jì)算假設(shè)模型H的遷移覆蓋集P、狀態(tài)覆蓋集S、特征集W以及M的所有狀態(tài)機(jī)識(shí)別集Wi。構(gòu)造檢查所有規(guī)范M定義的狀態(tài)在實(shí)現(xiàn)庫(kù)中是否可識(shí)別,對(duì)每個(gè)S中的狀態(tài)Si,其識(shí)別集Wi是確定的,并且W是一組至少包含所有Wi輸入序列的集合。設(shè)所有識(shí)別集Wi的集合為W,通過(guò)P,S以及Wi的選擇,可以得到不同的測(cè)試序列。

第一階段中的測(cè)試序列由S,W生成。每個(gè)規(guī)范的狀態(tài)Si由W集檢測(cè)。如果所有的測(cè)試都成功了,則M≈Q.WH,此時(shí)協(xié)議實(shí)現(xiàn)庫(kù)中的狀態(tài)數(shù)與規(guī)范M中的狀態(tài)數(shù)相等。

H檢測(cè)每個(gè)狀態(tài)sj是否可以由最小識(shí)別集Wj識(shí)別。同時(shí),對(duì)從初始狀態(tài)到這些狀態(tài)的遷移進(jìn)行檢查。

第二階段對(duì)所有協(xié)議規(guī)范所確定的,但在第一階段中未檢測(cè)的遷移進(jìn)行檢測(cè)。

此時(shí)構(gòu)造測(cè)試序列屬于P而不屬于S,記R=P-S,則此時(shí)有

式中,Wj是W中Sj的識(shí)別集。這個(gè)階段對(duì)剩余的遷移關(guān)系進(jìn)行檢測(cè)。進(jìn)行完兩個(gè)階段即可生成正確的SUT狀態(tài)機(jī)。

2.3.2 套接字約簡(jiǎn)方法

通過(guò)Wp方法產(chǎn)生測(cè)試集的復(fù)雜度為O(n2|Σ|(m-n+1)),其中Σ是狀態(tài)機(jī)的輸入字母表；m是目標(biāo)系統(tǒng)的狀態(tài)數(shù)上界；n是狀態(tài)機(jī)的狀態(tài)數(shù)。因此,當(dāng)Wp方法的狀態(tài)數(shù)n較大時(shí),會(huì)造成測(cè)試序列數(shù)量呈指數(shù)性增長(zhǎng),不利于大狀態(tài)數(shù)系統(tǒng)的學(xué)習(xí)。需要對(duì)此算法中的查詢數(shù)量進(jìn)行簡(jiǎn)化。

可以利用協(xié)議交互中的消息跡的實(shí)際意義對(duì)測(cè)試序列生成進(jìn)行約簡(jiǎn),通過(guò)特定的套接字序列,簡(jiǎn)化測(cè)試序列的生成。

情況1連接中斷

在尋找反例時(shí),連接關(guān)閉后的追蹤是沒有意義的,但是在與SUT的交互中,一旦會(huì)話結(jié)束,SUT仍然會(huì)產(chǎn)生連接斷開的響應(yīng),Wp方法會(huì)將此響應(yīng)作為目標(biāo)系統(tǒng)的輸出構(gòu)造等價(jià)查詢尋找反例,而這些是無(wú)效的測(cè)試序列,需要終止后續(xù)測(cè)試序列生成。

情況2密鑰重協(xié)商

在協(xié)議的會(huì)話中,可以通過(guò)發(fā)送密鑰重協(xié)商消息進(jìn)行密鑰更改,這個(gè)過(guò)程可以看作是將協(xié)議狀態(tài)重新遷移到了握手協(xié)議中的更改密碼規(guī)范狀態(tài),二者在其后的測(cè)試序列生成一致,是多余的測(cè)試序列,因此可以停止生成重協(xié)商之后的測(cè)試序列的生成。

情況3異常消息警告

異常消息警告包括協(xié)議連接斷開通知、關(guān)鍵警告以及警告。其中連接斷開通知和關(guān)鍵警報(bào)會(huì)造成連接斷開,與情況1中的連接中斷類似,終止后續(xù)測(cè)試序列生成。

該改進(jìn)算法利用了協(xié)議交互中的連接特性,利用特定套接字對(duì)測(cè)試序列生成進(jìn)行了約簡(jiǎn)。

2.3.3 檢查點(diǎn)算法

考慮到在構(gòu)造測(cè)試序列時(shí),SUT有時(shí)需要處理大量具有相同前綴的查詢,從初始狀態(tài)開始處理查詢的話,在對(duì)查詢的相同前綴進(jìn)行處理時(shí),SUT進(jìn)行相同的狀態(tài)遷移。如果每次都對(duì)SUT進(jìn)行重置,需要大量的重復(fù)測(cè)試過(guò)程,因此需要對(duì)測(cè)試序列的處理進(jìn)行優(yōu)化,在處理SUT時(shí),對(duì)其可能遇到的前綴時(shí)的狀態(tài)及測(cè)試序列前綴進(jìn)行記錄,稱這個(gè)記錄點(diǎn)為檢查點(diǎn)。可以通過(guò)構(gòu)造前綴樹用來(lái)存儲(chǔ)之前執(zhí)行過(guò)的查詢,實(shí)現(xiàn)檢查點(diǎn)算法。

樹中每個(gè)節(jié)點(diǎn)記錄一個(gè)之前的輸入、相應(yīng)的輸出以及當(dāng)時(shí)的狀態(tài)的相關(guān)信息。在樹的輸出查詢中,從根節(jié)點(diǎn)開始對(duì)每個(gè)查詢中的輸入步驟選擇相應(yīng)的子節(jié)點(diǎn)。在這個(gè)過(guò)程中能夠找到對(duì)每個(gè)輸入步驟的相應(yīng)的輸出。一個(gè)查詢由已知輸出的前綴,以及其后綴還未執(zhí)行過(guò)未知其輸出的后綴組成。其形式化描述如表1所示。

表1 檢查點(diǎn)算法Table 1 Checkpoint algorithm

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

本研究分析了兩種TLS實(shí)現(xiàn)庫(kù)OpenSSl及網(wǎng)絡(luò)安全服務(wù)(network security service,NSS)的米利狀態(tài)機(jī)模型。

3.1 測(cè)試過(guò)程設(shè)置

為了推斷TLS協(xié)議實(shí)現(xiàn)的米利狀態(tài)機(jī),本文使用了開源的狀態(tài)機(jī)學(xué)習(xí)框架LearnLib[15],其使用了L*算法進(jìn)行學(xué)習(xí)。SUT對(duì)于測(cè)試者是黑盒,由于無(wú)法得知協(xié)議庫(kù)的實(shí)際執(zhí)行狀態(tài)。因此必須向LearnLib提供可以發(fā)送到SUT的消息列表以及將SUT重置為其初始狀態(tài)的命令。

通過(guò)發(fā)送消息和重置命令的序列,利用測(cè)試工具將抽象消息從輸入字母表轉(zhuǎn)換為可以發(fā)送到被測(cè)系統(tǒng)的具體消息,LearnLib嘗試根據(jù)從SUT收到的響應(yīng)為狀態(tài)機(jī)提出假設(shè)。然后檢查這些假設(shè)是否與實(shí)際狀態(tài)機(jī)等效。如果模型不相等,則返回一個(gè)反例,LearnLib將使用它來(lái)重新修改其假設(shè)模型。

3.1.1 檢查深度

對(duì)于LearnLib,在測(cè)試中首先需要指定等價(jià)檢查的深度:給定狀態(tài)機(jī)的假設(shè)H,需要將測(cè)試上限設(shè)置為找到的狀態(tài)數(shù)加上指定的深度。該算法僅查找其長(zhǎng)度最多為設(shè)定上限的反例跟蹤,如果無(wú)法找到,則假定狀態(tài)機(jī)的當(dāng)前假設(shè)與實(shí)現(xiàn)的假設(shè)等效。如果實(shí)際狀態(tài)機(jī)的狀態(tài)數(shù)多于找到的狀態(tài)數(shù)加上指定的深度,則認(rèn)為此假設(shè)是正確的。本文通過(guò)實(shí)際測(cè)試經(jīng)驗(yàn),取測(cè)試深度為5進(jìn)行測(cè)試。

3.1.2 輸入輸出字母表

為了使用LearnLib,還需要設(shè)定一個(gè)可利用的輸入字母表,其可以將實(shí)際發(fā)送和收到的消息抽象為一個(gè)字符串作為L(zhǎng)earnLib的輸入,設(shè)定輸入輸出字母表為:客戶端握手、客戶端證書、完成、客戶端密鑰交換、客戶端證書驗(yàn)證、更改密碼規(guī)范、應(yīng)用數(shù)據(jù)。由于有警告協(xié)議中的消息格式只在響應(yīng)中,因此在輸出表中加入空?qǐng)?bào)文,解密失敗以及連接中斷。

3.2 測(cè)試結(jié)果

表2為使用指定檢查深度為5的改進(jìn)Wp方法對(duì)輸入的常規(guī)字母表的協(xié)議服務(wù)器端進(jìn)行自動(dòng)測(cè)試的結(jié)果。

表2 改進(jìn)算法在測(cè)試深度為5條件下應(yīng)用輸入字母表對(duì)服務(wù)器端實(shí)現(xiàn)的自動(dòng)測(cè)試結(jié)果Table 2 Results of the automated analysis of server implementations for the alphabet of inputs using our modified method with depth=5

通過(guò)套接字約簡(jiǎn)方法,生成的等價(jià)查詢數(shù)顯著下降,這意味著改進(jìn)的測(cè)試序列生成方法能夠有效約簡(jiǎn)學(xué)習(xí)狀態(tài)機(jī)過(guò)程中所需的測(cè)試序列數(shù)量。從學(xué)習(xí)狀態(tài)機(jī)模型所用時(shí)間上看,生成模型所用時(shí)間顯著下降,這意味著該方法通過(guò)TLS的特定套接字,極大地減少了測(cè)試過(guò)程中的冗余信息。

實(shí)驗(yàn)結(jié)果表明,雖然只應(yīng)用檢查點(diǎn)算法的改進(jìn)算法無(wú)法減少所需的成員查詢和等價(jià)查詢數(shù)量,但是可以明顯減少狀態(tài)機(jī)學(xué)習(xí)所用時(shí)間。這說(shuō)明通過(guò)檢查點(diǎn)算法,能夠顯著降低SUT在測(cè)試過(guò)程中對(duì)測(cè)試序列的響應(yīng)時(shí)間,加速反例生成,提升狀態(tài)機(jī)學(xué)習(xí)效率。但其效果不如套接字約簡(jiǎn)明顯。

二者結(jié)合的改進(jìn)算法所需時(shí)間最少,效率最高,這是由于兩種方法從不同的角度對(duì)算法效率有提高。

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

在分析得到的模型時(shí),首先人工查看是否有比預(yù)期更多的路徑導(dǎo)致應(yīng)用程序數(shù)據(jù)的成功交換。其次確定模型是否包含多于必要的狀態(tài),并識(shí)別意外或多余的過(guò)渡狀態(tài)。還需要檢查可以指示異常狀態(tài)的消息。如果遇到任何異常,那么就要更深入的分析以確定原因及影響。一個(gè)明顯的觀察是服務(wù)器端實(shí)現(xiàn)庫(kù)的狀態(tài)機(jī)模型都有所不同,這意味著TLS實(shí)現(xiàn)庫(kù)在實(shí)現(xiàn)過(guò)程由于開發(fā)者對(duì)協(xié)議規(guī)范的理解不同。那么在實(shí)際應(yīng)用中,就存在著潛在的安全威脅。

特別是,協(xié)議狀態(tài)機(jī)學(xué)習(xí)涉及一種被動(dòng)測(cè)試:在狀態(tài)機(jī)學(xué)習(xí)期間執(zhí)行的測(cè)試包括錯(cuò)誤測(cè)試,即消息以意外命令發(fā)送的測(cè)試,人們期望這會(huì)導(dǎo)致連接中斷,而如果連接并沒有按照規(guī)范設(shè)定的中斷的話,則需要深入調(diào)查其原因。圖2是OpenSSL 1.0.1g服務(wù)器端學(xué)習(xí)到的狀態(tài)機(jī)模型。對(duì)此狀態(tài)機(jī)進(jìn)行分析,可以看到一條可疑路徑(狀態(tài)0,1,6,9,12)。

如圖2虛線所示的路徑中,當(dāng)服務(wù)器收到更改密碼規(guī)范消息時(shí),就會(huì)開始計(jì)算會(huì)話密鑰,然而此時(shí)還沒有發(fā)送客戶端密鑰交換消息,因此實(shí)際上服務(wù)器端用的是一個(gè)空的主密鑰,這意味著在通信過(guò)程中,實(shí)際使用的密鑰是通過(guò)傳遞的消息計(jì)算所得的。攻擊者就能輕易計(jì)算出接下來(lái)的會(huì)話所用的密鑰。

這意味著攻擊者能夠在握手初期通過(guò)向客戶端和服務(wù)器發(fā)送更改密碼規(guī)范消息來(lái)劫持一段會(huì)話。

通過(guò)上述分析可以看到,通過(guò)狀態(tài)機(jī)學(xué)習(xí)得到的狀態(tài)機(jī)模型,可以尋找在協(xié)議實(shí)現(xiàn)庫(kù)的邏輯缺陷,完成對(duì)協(xié)議實(shí)現(xiàn)庫(kù)的安全性分析的目的,這證明了通過(guò)改進(jìn)算法提取的協(xié)議狀態(tài)機(jī)是有效的。

圖2 通過(guò)改進(jìn)算法學(xué)習(xí)到的OpenSSL 1.0.1 g狀態(tài)機(jī)Fig.2 Learned state machine model for OpenSSL 1.0.1 g

4 結(jié) 論

本文提出了一種改進(jìn)的測(cè)試序列構(gòu)造方法,其利用套接字約簡(jiǎn),能夠有效減少在對(duì)目標(biāo)系統(tǒng)黑盒測(cè)試中所用到的測(cè)試序列數(shù)量,減少運(yùn)算量;同時(shí)利用檢查點(diǎn)算法,降低分析的運(yùn)行時(shí)間,從而提高狀態(tài)機(jī)學(xué)習(xí)效率,在未知目標(biāo)系統(tǒng)規(guī)范的黑盒測(cè)試中具有很好的效果,從而使得分析復(fù)雜狀態(tài)機(jī)運(yùn)行成為可能。實(shí)驗(yàn)結(jié)果表明,完整改進(jìn)算法效率最高,既結(jié)合了套接字約簡(jiǎn)的等價(jià)查詢數(shù)減少,又通過(guò)檢查點(diǎn)算法提高了測(cè)試效率。整體上看,套接字約簡(jiǎn)對(duì)學(xué)習(xí)效率的提升效果好于檢查點(diǎn)算法。

本文結(jié)合狀態(tài)機(jī)學(xué)習(xí)的L*算法以及等價(jià)查詢算法Wp方法,成功地提取了OpenSSH,NSS兩類TLS協(xié)議實(shí)現(xiàn)庫(kù)的狀態(tài)機(jī)模型。并以此為基礎(chǔ)對(duì)TLS協(xié)議實(shí)現(xiàn)庫(kù)進(jìn)行深入的分析。通過(guò)狀態(tài)機(jī)學(xué)習(xí)技術(shù)來(lái)測(cè)試協(xié)議實(shí)現(xiàn)庫(kù),能夠有效發(fā)現(xiàn)其中存在的邏輯缺陷。