畢 興,唐朝京

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

0 引 言

傳輸層安全(transport layer security,TLS)協(xié)議用于為網(wǎng)絡(luò)提供安全及數(shù)據(jù)完整性保障。作為最廣泛使用的安全協(xié)議之一,其安全性引起了業(yè)界的高度關(guān)注,各類研究者及攻擊者對其進行了細致深入的分析,它經(jīng)歷了從密碼學攻擊[1-3]到協(xié)議實現(xiàn)庫漏洞[4-6]等一系列安全威脅。其中TLS協(xié)議實現(xiàn)庫作為TLS協(xié)議的應用載體,也被看作一個實施網(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)機學習技術(shù),能夠僅依賴于黑盒測試,不需要知道協(xié)議規(guī)范,就可以從協(xié)議實現(xiàn)庫中提取狀態(tài)機。通過分析這些狀態(tài)機,可以發(fā)現(xiàn)協(xié)議的狀態(tài)遷移中存在的邏輯錯誤。

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

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

1 TLS協(xié)議

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

握手協(xié)議是TLS是最重要的部分,其主要作用是在客戶端和服務器之間建立安全的數(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客戶端向服務端發(fā)送服務器握手消息,這個消息里包括客戶端生成的隨機數(shù)、客戶端支持的加密套件等信息。

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

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

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

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

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

2 狀態(tài)機學習算法

狀態(tài)機學習算法試圖學習目標系統(tǒng)的模型。通過選擇輸入查詢目標系統(tǒng),根據(jù)目標系統(tǒng)的響應,最終推斷出目標系統(tǒng)的模型。如果模型是正確的,即其與目標系統(tǒng)輸出一致,學習算法將認為生成的模型與目標系統(tǒng)的模型相同并停機。另一方面,如果模型不正確,目標系統(tǒng)和模型的輸入產(chǎn)生不同的輸出,根據(jù)這個不同的輸出可以構(gòu)造出反例。學習算法利用反例改進推斷所得模型。重復這個流程直到學習算法產(chǎn)生正確的模型。由于協(xié)議實現(xiàn)庫的輸出不僅與其輸入有關(guān),同時也與其當前狀態(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)機當前狀態(tài)和輸入。米利狀態(tài)機的行為可以通過函數(shù)來定義,其中AM(σ)=λ(q0,σ)。當且僅當AM=AN時,狀態(tài)機M和N稱為等價的,記做M≈N。

2.2 狀態(tài)機學習算法

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

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

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

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

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

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

實際分析的目標系統(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)生測試集的復雜度為O(n2|Σ|(m-n+1)),其中Σ是狀態(tài)機的輸入字母表；m是目標系統(tǒng)的狀態(tài)數(shù)上界；n是狀態(tài)機的狀態(tài)數(shù)。因此,當Wp方法的狀態(tài)數(shù)n較大時,會造成測試序列數(shù)量呈指數(shù)性增長,不利于大狀態(tài)數(shù)系統(tǒng)的學習。需要對此算法中的查詢數(shù)量進行簡化。

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

情況1連接中斷

在尋找反例時,連接關(guān)閉后的追蹤是沒有意義的,但是在與SUT的交互中,一旦會話結(jié)束,SUT仍然會產(chǎn)生連接斷開的響應,Wp方法會將此響應作為目標系統(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進行重置,需要大量的重復測試過程,因此需要對測試序列的處理進行優(yōu)化,在處理SUT時,對其可能遇到的前綴時的狀態(tài)及測試序列前綴進行記錄,稱這個記錄點為檢查點?？梢酝ㄟ^構(gòu)造前綴樹用來存儲之前執(zhí)行過的查詢,實現(xiàn)檢查點算法。

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

表1 檢查點算法Table 1 Checkpoint algorithm

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

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

3.1 測試過程設(shè)置

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

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

3.1.1 檢查深度

對于LearnLib,在測試中首先需要指定等價檢查的深度:給定狀態(tài)機的假設(shè)H,需要將測試上限設(shè)置為找到的狀態(tài)數(shù)加上指定的深度。該算法僅查找其長度最多為設(shè)定上限的反例跟蹤,如果無法找到,則假定狀態(tài)機的當前假設(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ī)范、應用數(shù)據(jù)。由于有警告協(xié)議中的消息格式只在響應中,因此在輸出表中加入空報文,解密失敗以及連接中斷。

3.2 測試結(jié)果

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

表2 改進算法在測試深度為5條件下應用輸入字母表對服務器端實現(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ù)顯著下降,這意味著改進的測試序列生成方法能夠有效約簡學習狀態(tài)機過程中所需的測試序列數(shù)量。從學習狀態(tài)機模型所用時間上看,生成模型所用時間顯著下降,這意味著該方法通過TLS的特定套接字,極大地減少了測試過程中的冗余信息。

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

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

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

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

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

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

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

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

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

4 結(jié) 論

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

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