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

畢 興,唐朝京

(國防科技大學(xué)電子科學(xué)學(xué)院,湖南 長沙 410073)

0 引 言

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

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

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

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

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

1 TLS協(xié)議

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

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

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

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

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

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

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

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

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

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

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

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

2.1 米利狀態(tài)機

米利狀態(tài)機是一類有限狀態(tài)機,可以形式化地描述為一個六元組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)機當(dāng)前狀態(tài)和輸入。米利狀態(tài)機的行為可以通過函數(shù)來定義,其中AM(σ)=λ(q0,σ)。當(dāng)且僅當(dāng)AM=AN時,狀態(tài)機M和N稱為等價的,記做M≈N。

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

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

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

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

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

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

2.3 改進的測試序列生成算法

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

2.3.1 測試序列生成算法

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

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

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

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

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

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

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

2.3.2 套接字約簡方法

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

可以利用協(xié)議交互中的消息跡的實際意義對測試序列生成進行約簡,通過特定的套接字序列,簡化測試序列的生成。

情況1連接中斷

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

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

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

情況3異常消息警告

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

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

2.3.3 檢查點算法

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

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

表1 檢查點算法Table 1 Checkpoint algorithm

3 實驗及結(jié)果分析

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

3.1 測試過程設(shè)置

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

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

3.1.1 檢查深度

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

3.1.2 輸入輸出字母表

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

3.2 測試結(jié)果

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

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

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

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

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

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

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

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

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

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

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

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

4 結(jié) 論

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

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