基于狀態機學習算法的TLS實現庫安全性分析

畢 興,唐朝京

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

0 引 言

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

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

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

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

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

1 TLS協議

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

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

TLS執行步驟如圖1所示。

圖1 TLS執行過程Fig.1 TLS executing procedure

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

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

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

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

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

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

2 狀態機學習算法

狀態機學習算法試圖學習目標系統的模型。通過選擇輸入查詢目標系統,根據目標系統的響應,最終推斷出目標系統的模型。如果模型是正確的,即其與目標系統輸出一致,學習算法將認為生成的模型與目標系統的模型相同并停機。另一方面,如果模型不正確,目標系統和模型的輸入產生不同的輸出,根據這個不同的輸出可以構造出反例。學習算法利用反例改進推斷所得模型。重復這個流程直到學習算法產生正確的模型。由于協議實現庫的輸出不僅與其輸入有關,同時也與其當前狀態有關,因此選擇米利狀態機描述TLS實現庫的狀態機模型。

2.1 米利狀態機

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

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

其輸出依賴于狀態機當前狀態和輸入。米利狀態機的行為可以通過函數來定義,其中AM(σ)=λ(q0,σ)。當且僅當AM=AN時,狀態機M和N稱為等價的,記做M≈N。

2.2 狀態機學習算法

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

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

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

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

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

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

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

2.3.1 測試序列生成算法

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

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

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

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

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

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

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

2.3.2 套接字約簡方法

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

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

情況1連接中斷

在尋找反例時,連接關閉后的追蹤是沒有意義的,但是在與SUT的交互中,一旦會話結束,SUT仍然會產生連接斷開的響應,Wp方法會將此響應作為目標系統的輸出構造等價查詢尋找反例,而這些是無效的測試序列,需要終止后續測試序列生成。

情況2密鑰重協商

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

情況3異常消息警告

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

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

2.3.3 檢查點算法

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

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

表1 檢查點算法Table 1 Checkpoint algorithm

3 實驗及結果分析

本研究分析了兩種TLS實現庫OpenSSl及網絡安全服務(network security service,NSS)的米利狀態機模型。

3.1 測試過程設置

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

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

3.1.1 檢查深度

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

3.1.2 輸入輸出字母表

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

3.2 測試結果

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

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

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

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

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

3.3 狀態機模型分析

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

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

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

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

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

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

4 結 論

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

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