模型學習與符號執(zhí)行結(jié)合的安全協(xié)議代碼分析技術(shù)

張協(xié)力，祝躍飛，顧純祥，陳熹

模型學習與符號執(zhí)行結(jié)合的安全協(xié)議代碼分析技術(shù)

張協(xié)力1,2，祝躍飛1,2，顧純祥1,2，陳熹1,2

（1. 數(shù)學工程與先進計算國家重點實驗室，河南 鄭州 450001；2. 網(wǎng)絡(luò)密碼技術(shù)河南省重點實驗室，河南 鄭州 450002）

符號執(zhí)行技術(shù)從理論上可以全面分析程序執(zhí)行空間，但對安全協(xié)議這樣的大型程序，路徑空間爆炸和約束求解困難的局限性導致其在實踐上不可行。結(jié)合安全協(xié)議程序自身特點，提出用模型學習得到的協(xié)議狀態(tài)機信息指導安全協(xié)議代碼符號執(zhí)行思路；同時，通過將協(xié)議代碼中的密碼學邏輯與協(xié)議交互邏輯相分離，避免了因密碼邏輯的復雜性導致路徑約束無法求解的問題。在SSH協(xié)議開源項目Dropbear上的成功實踐表明了所提方法的可行性；通過與Dropbear自帶的模糊測試套件對比，驗證了所提方法在代碼覆蓋率與錯誤點發(fā)現(xiàn)上均具有一定優(yōu)勢。

模型學習；符號執(zhí)行；安全協(xié)議代碼；狀態(tài)驅(qū)動

1 引言

安全協(xié)議在理論設(shè)計和代碼實現(xiàn)中都極易出錯。針對協(xié)議規(guī)范的形式化驗證方法由于忽略了協(xié)議實現(xiàn)細節(jié)，無法保證協(xié)議實現(xiàn)的安全。而安全協(xié)議較大的代碼規(guī)模和復雜的交互邏輯讓協(xié)議代碼安全審計變得更加困難。研究新的技術(shù)和方法來輔助安全協(xié)議代碼檢測是一項挑戰(zhàn)性工作。

模型學習和模糊測試兩種技術(shù)在安全協(xié)議程序分析方面取得了許多有價值的研究成果。Paul等[1]通過MAT[2]（minimally adequate teacher）模型學習框架推斷得到協(xié)議程序狀態(tài)機信息，然后用模型檢測器檢測協(xié)議程序狀態(tài)機模型中是否存在與協(xié)議規(guī)范要求不一致的路徑。文獻[3]用類似的工作思路對安全協(xié)議IpSec的開源實現(xiàn)進行了分析，發(fā)現(xiàn)了一個違反狀態(tài)機時序邏輯的bug。文獻[4]進一步將模型學習與模糊測試技術(shù)相結(jié)合，對DTLS進行了分析。直接對模型學習得到的協(xié)議程序的狀態(tài)機進行模型檢測，其局限性在于僅能發(fā)現(xiàn)與狀態(tài)機的時序問題，不能用于發(fā)掘更細節(jié)的錯誤。符號執(zhí)行技術(shù)可以用較少的測試用例達到較大覆蓋率，在安全協(xié)議分析方面，文獻[5]用符號執(zhí)行技術(shù)分析了TLS的X.509證書解析代碼；文獻[6]提出在對安全協(xié)議符號執(zhí)行時將密碼原語采用重寫技術(shù)進行處理；文獻[7]用密碼原語重寫的方式分析了WPA2的4次握手協(xié)議并發(fā)現(xiàn)了其中的脆弱性。這些工作采用符號執(zhí)行技術(shù)分析安全協(xié)議中小部分重要代碼邏輯，規(guī)避了代碼路徑空間爆炸和約束求解困難問題，但未解決將符號執(zhí)行技術(shù)用于整個安全協(xié)議代碼的分析時所面臨的這兩個主要問題。例如，文獻[8]僅分析PKCS#1 v1.5的簽名驗證邏輯，文獻[5]只對X.509的證書驗證代碼進行了符號執(zhí)行等。文獻[9]中對安全協(xié)議實施的安全性驗證問題進行了全面綜述。常規(guī)的軟件測試方法（如模糊測試）通常依賴人工專家經(jīng)驗對協(xié)議規(guī)范分析后定制模糊測試策略[10]。文獻[11]將TCP的狀態(tài)機信息用于對TCP實現(xiàn)的模糊測試中，用協(xié)議狀態(tài)機信息生成Fuzz策略。文獻[12-13]也都使用協(xié)議規(guī)范信息來減少協(xié)議程序的搜索空間。文獻[14]基于協(xié)議規(guī)范利用符號執(zhí)行技術(shù)來檢測協(xié)議實現(xiàn)的脆弱性。文獻[15-16]將模糊處理與符號執(zhí)行相結(jié)合，使用模糊測試來初步探索網(wǎng)絡(luò)協(xié)議，同時執(zhí)行符號執(zhí)行探索程序路徑和協(xié)議狀態(tài)，比單獨使用兩項技術(shù)的代碼覆蓋率高。文獻[17]提出了用模型推斷指導協(xié)議的conclic執(zhí)行分析，方法的主要不足在于模型推斷和符號執(zhí)行交互迭代的過程十分耗時，且未對安全協(xié)議的密碼學模塊進行處理，仍可能面臨約束求解困難問題導致符號執(zhí)行無法繼續(xù)。

本文方法在文獻[17]思路基礎(chǔ)上，結(jié)合了文獻[5-8]方法上的優(yōu)勢，既處理對安全協(xié)議程序符號執(zhí)行時路徑空間爆炸問題，又解決因密碼學邏輯導致的求解困難問題。該技術(shù)將模型學習與符號執(zhí)行技術(shù)相結(jié)合來探索協(xié)議代碼的執(zhí)行空間，同時將協(xié)議中的密碼原語代碼空間與協(xié)議交互邏輯的代碼執(zhí)行空間相分離，降低安全協(xié)議代碼規(guī)模，更具體地：① 采用模型學習算法獲取協(xié)議程序的Mealy machine信息；② 以協(xié)議程序的狀態(tài)機信息為基礎(chǔ)，引導符號執(zhí)行來探索感興趣或重要狀態(tài)附近的代碼執(zhí)行空間；③ 在符號執(zhí)行探索代碼執(zhí)行空間時，繞過密碼原語相關(guān)函數(shù)邏輯，避免符號執(zhí)行引擎陷入復雜的密碼學相關(guān)代碼邏輯中。

符號執(zhí)行被視為可以檢測深層次語義邏輯問題的分析技術(shù)，其可以檢測深層代碼邏輯同時生成較小測試用例達到較大的代碼覆蓋率。但在實際分析復雜代碼時，通常受限于路徑空間爆炸和SMT約束求解難問題。這些技術(shù)局限性在安全協(xié)議代碼的邏輯分析上更為顯著。一方面，由于安全協(xié)議設(shè)計中并行交互執(zhí)行邏輯原本就復雜，交互邏輯中多伴隨協(xié)議狀態(tài)轉(zhuǎn)換，某些潛在的bug僅在特定的協(xié)議執(zhí)行狀態(tài)上下文中才能被觸發(fā)，而符號執(zhí)行難以或更快速抵達這些狀態(tài)。另一方面，安全協(xié)議中的密碼學邏輯，增加了協(xié)議代碼執(zhí)行空間規(guī)模，尤其密碼學中的加解密及哈希算法中的混淆置換等邏輯，使協(xié)議程序執(zhí)行空間急劇膨脹。

對于第一個問題，在協(xié)議代碼上采用符號執(zhí)行探索時，缺乏目標協(xié)議實現(xiàn)的協(xié)議狀態(tài)機信息，并未區(qū)分不同協(xié)議狀態(tài)。采用模型學習技術(shù)獲取目標協(xié)議程序的Mealy machine，以協(xié)議程序的Mealy machine信息引導符號執(zhí)行引擎進行協(xié)議執(zhí)行空間探索，從而可以靈活地切換感興趣或重要的協(xié)議狀態(tài)空間。對于第二個問題，基于完美密碼假設(shè)理論將密碼學函數(shù)的代碼邏輯與協(xié)議交互邏輯代碼空間相分離，符號執(zhí)行時不進入密碼學代碼空間。這樣既有效提高符號執(zhí)行的效率，又避免符號執(zhí)行陷入密碼學代碼邏輯或因混淆變換邏輯導致SMT無法求解得到符號公式。

本文在SSH協(xié)議的開源項目Dropbear上實踐了該方法，并通過與Dropbear源碼中自帶的模糊測試套件進行了對比，表明本文方法在協(xié)議代碼的測試覆蓋率和發(fā)現(xiàn)錯誤點數(shù)量上均有一定提高。

本文主要貢獻如下。

（1）提出了協(xié)議程序的狀態(tài)驅(qū)動來指導協(xié)議源碼符號執(zhí)行的技術(shù)思路，可以有效解決對協(xié)議源碼做符號執(zhí)行分析時面臨的路徑空間爆炸問題。

（2）基于完美密碼假設(shè)理論采用具體執(zhí)行和封裝策略處理安全協(xié)議代碼中的密碼學部分，可以避免在對安全協(xié)議代碼符號執(zhí)行時因密碼學邏輯造成的SMT求解困難問題。

（3）在SSH開源實現(xiàn)Dropbear上成功實踐了本文方法的技術(shù)思路，并通過與Dropbear自帶的模糊測試套件的對比實驗表明了本文方法的有效性。

2 基礎(chǔ)知識

2.1 符號執(zhí)行

符號執(zhí)行是一種用于為軟件生成高覆蓋率測試用例和發(fā)現(xiàn)程序中深層錯誤的技術(shù)。經(jīng)典符號執(zhí)行的基本思想是用符號變量替代具體值作為程序輸入，以模擬執(zhí)行方式為程序執(zhí)行空間中的每條執(zhí)行路徑生成輸入符號變量表達式作為路徑約束條件，通過SMT求解器對每條路徑（或感興趣路徑）的路徑約束進行求解來判斷其可達性。程序執(zhí)行時為程序維護一個當前執(zhí)行狀態(tài)和路徑約束，狀態(tài)內(nèi)容為變量到符號表達式的映射，路徑約束為符號表達式的無量詞一階邏輯公式。在程序執(zhí)行開始時，狀態(tài)為空集，路徑約束為true。在執(zhí)行過程中根據(jù)代碼邏輯不斷更新執(zhí)行狀態(tài)和路徑約束；最后通過SMT約束求解器求解路徑約束，若路徑對應的約束條件有解，則該條路徑可達，即存在具體輸入值可以使程序執(zhí)行該條路徑；反之，則該條路徑不可達。其基本思想是：如果程序在這些具體的輸入值上執(zhí)行，則將采用與符號執(zhí)行完全相同的路徑，并以相同的方式結(jié)束。

路徑爆炸及約束求解瓶頸是符號執(zhí)行技術(shù)當前面臨的關(guān)鍵挑戰(zhàn)。在理論上程序執(zhí)行路徑的數(shù)量與代碼中的條件分支數(shù)量成指數(shù)級關(guān)系，難以在給定時間內(nèi)探索所有執(zhí)行空間；此外，因為SMT問題本身是被證明的NPC問題，盡管現(xiàn)代SMT求解器采用了技巧使SMT求解可行，但仍可能存在為每條執(zhí)行路徑生成的路徑約束無法求解的情況，導致符號執(zhí)行引擎無法終止和繼續(xù)探索其他路徑。在代碼量較多的大型程序中這些限制尤為突出，特別是安全協(xié)議實現(xiàn)這樣邏輯復雜的程序，在利用符號執(zhí)行分析時，由于協(xié)議自身復雜的執(zhí)行交互設(shè)計和密碼學相關(guān)函數(shù)的混淆變換邏輯，加劇了符號執(zhí)行引擎的負擔。

2.2 模型學習

為符號執(zhí)行提供協(xié)議的抽象信息來引導其對協(xié)議執(zhí)行空間的探索。本文借鑒Paul等[1]工作思路，通過模型學習算法抽取協(xié)議的Mealy machine作為協(xié)議執(zhí)行的高級狀態(tài)信息。本節(jié)介紹Mealy machine和經(jīng)典的狀態(tài)機學習框架。

本節(jié)介紹經(jīng)典的模型學習框架MAT[2]（如圖1所示）。MAT框架適用于軟件系統(tǒng)的黑盒學習模型，將目標系統(tǒng)的模型學習看作Learner和Teacher之間的query-response游戲。Learner通過向Teacher query來推斷狀態(tài)機模型。Teacher為被測軟件系統(tǒng)，其擁有狀態(tài)機信息，故又稱其為SUL（system under learning）。Learner在學習初始階段，掌握輸入集合和輸出集合。

圖1 MAT學習框架

Figure 1 MAT framework

Learner通過以下兩種類型的查詢來獲取狀態(tài)機信息。

Membership query：Learner向Teacher查詢一個輸入序列對應的輸出序列，Teacher給出相應的輸出序列。如采用L*算法，從query得到的輸入序列/輸出序列信息，推斷出Mealy machine。

3 方法

3.1 方法概述

本文方法主要探索如何在安全協(xié)議代碼上利用符號執(zhí)行方法進行高效的代碼空間探索，檢查協(xié)議代碼實現(xiàn)中存在的問題。由于安全協(xié)議代碼邏輯復雜，直接對安全協(xié)議代碼采用符號執(zhí)行分析是不可行的。為此采用了兩種技巧來提高符號執(zhí)行引擎在安全協(xié)議代碼探索時的效率：①為符號執(zhí)行引擎提供協(xié)議目標代碼的高級抽象信息Mealy machine作為指導，便于符號執(zhí)行引擎探索感興趣的協(xié)議狀態(tài)附近的執(zhí)行空間；②將安全協(xié)議代碼中與密碼學相關(guān)的代碼從符號執(zhí)行分析的代碼空間中去除，以減少密碼學中混淆變換引入的不必要的邏輯，從而降低協(xié)議代碼執(zhí)行空間的分支路徑。

方案的整體思路如下。按照MAT框架，以協(xié)議二進制為學習目標（即Teacher/SUL），采用模型學習算法L*，學習出目標協(xié)議實現(xiàn)的Mealy machine；從Mealy machine中抽取從初始狀態(tài)到任意狀態(tài)的消息序列，以得到的消息序列集合近似代替Mealy machine的局部信息。對消息序列進行轉(zhuǎn)換，通過mapper程序?qū)⑵溆成錇閷嶋H的數(shù)據(jù)包序列；符號執(zhí)行引擎加載執(zhí)行協(xié)議代碼，以轉(zhuǎn)換后的數(shù)據(jù)包序列作為socket通信輸入，探索該消息序列下的安全協(xié)議代碼執(zhí)行空間。測試者可以自由選擇數(shù)據(jù)包序列并將感興趣的消息字段符號化進行定制化探索。在符號執(zhí)行引擎對協(xié)議代碼空間探索時，將密碼學相關(guān)函數(shù)套件進行屏蔽，可極大降低協(xié)議代碼復雜度，也可讓符號執(zhí)行引擎探索工作集中在協(xié)議代碼與環(huán)境交互時的協(xié)議執(zhí)行邏輯上。

3.2 模型學習抽取Mealy machine

本文根據(jù)MAT學習框架，以黑盒的方式學習目標協(xié)議程序的高級抽象信息Mealy machine。

為了避免模型學習陷入無法終止或者變?yōu)椴淮_定性狀態(tài)，需要保證學習的目標協(xié)議程序是一個確定性的程序，即在同一狀態(tài)下，對相同的報文數(shù)據(jù)輸入，輸出報文數(shù)據(jù)是相同的。換言之，在協(xié)議程序的初始狀態(tài)下，對于確定的報文序列，其輸出報文序列是確定的。這一點，通常需要將待學習的目標協(xié)議程序的初始化配置文件進行固定設(shè)置即可保證。本文的目標不包括檢測目標協(xié)議程序的配置是否存在問題，而關(guān)注于協(xié)議程序在其通用的初始化配置下與對等端的交互處理邏輯是否存在bug?？梢酝ㄟ^重設(shè)配置，重復整個方案工作來探索某一具體配置問題。

一個Mealy machine最根本的蘊含信息是輸入輸出序列，因為狀態(tài)是由輸入輸出序列確定的。在學習協(xié)議程序的Mealy machine前，需要先確定什么是抽象模型的輸入輸出集合。參考協(xié)議規(guī)范中狀態(tài)機描述方式，以消息類型來抽象表示一個具體的協(xié)議數(shù)據(jù)報文。自然地，一個輸入序列被抽象為輸入消息類型序列，一個輸出序列被抽象為輸出消息類型序列。根據(jù)協(xié)議規(guī)范，確定一個具體協(xié)議實現(xiàn)的輸入消息類型和輸出消息類型的有限集。

對于每一個待分析的協(xié)議程序，需要一個轉(zhuǎn)換程序?qū)⒊橄蟮南㈩愋娃D(zhuǎn)換為具體的、程序可接收的消息報文。這個轉(zhuǎn)換程序可以通過協(xié)議程序交互的對等端代碼進行改造實現(xiàn)，如在學習SSH協(xié)議服務(wù)端程序SSHD的Mealy machine信息時，通過改造SSH客戶端程序得到消息轉(zhuǎn)換程序。本文采用L*學習算法學習目標協(xié)議程序的Mealy machine信息，具體的學習步驟如下。

①學習程序通過決策生成輸入消息類型。

②轉(zhuǎn)換程序?qū)⑤斎胂㈩愋陀成錇榫唧w的輸入報文數(shù)據(jù)，發(fā)送給目標協(xié)議程序。

③目標協(xié)議程序在接收輸入報文數(shù)據(jù)后生成輸出報文數(shù)據(jù)。

④轉(zhuǎn)換程序?qū)⑤敵鰣笪臄?shù)據(jù)映射為抽象的輸出消息類型。

⑤學習程序根據(jù)輸出消息類型更新狀態(tài)信息并生成新的輸入消息類型。

⑥迭代步驟②～步驟⑤，直到完成學習目標，即模型收斂或達到設(shè)定學習時間。

⑦對學習到的模型采用隨機抽樣檢查一致性，若存在不一致，則修正(refine)模型。

3.3 狀態(tài)驅(qū)動：Mealy machine的抽象

由3.1節(jié)描述的模型學習方法，本文可以采用黑盒交互的方式學習到待分析協(xié)議程序的Mealy machine信息。這里基于假設(shè)學習到的Mealy machine是一個包含（或稱為實踐上近似包含）被分析的協(xié)議程序完整狀態(tài)集合和消息集合的高級抽象結(jié)構(gòu)，其中蘊含的協(xié)議狀態(tài)轉(zhuǎn)換關(guān)系是正確的。在此假設(shè)前提下，用其指導后續(xù)對協(xié)議程序代碼執(zhí)行空間的搜索分析。

按照上文學習到的Mealy machine是一個六元組集合，直接用其指導符號執(zhí)行是難以實踐的。學習到的Mealy machine可以看作節(jié)點之間有并行邊存在的有向圖結(jié)構(gòu)。節(jié)點表示協(xié)議程序的抽象狀態(tài)，邊代表狀態(tài)的變遷，而邊的屬性即input/output信息。為了將學習到的協(xié)議程序高級抽象信息Mealy machine作為安全協(xié)議代碼符號執(zhí)行時的指導信息，本文以狀態(tài)驅(qū)動集（state-driver set）來指導某一個具體協(xié)議狀態(tài)下的符號執(zhí)行。狀態(tài)驅(qū)動集定義如下。

性質(zhì)2 在性質(zhì)1中，轉(zhuǎn)換關(guān)系均不重復出現(xiàn)。

算法1 Mealy machine 狀態(tài)驅(qū)動集提取算法

3.4 用狀態(tài)驅(qū)動指導符號執(zhí)行

一個協(xié)議狀態(tài)的狀態(tài)驅(qū)動實質(zhì)是從協(xié)議程序的初始狀態(tài)到達該狀態(tài)的抽象消息序列。要將協(xié)議程序從初始的reset狀態(tài)引導到具體的協(xié)議狀態(tài)需要具體的數(shù)據(jù)包序列來觸發(fā)。這里可以重復利用模型學習時抽象消息到具體數(shù)據(jù)包的轉(zhuǎn)換器（Mapper）。轉(zhuǎn)換器可以根據(jù)協(xié)議規(guī)范，將一個狀態(tài)驅(qū)動中不同抽象消息拓展成具體的、協(xié)議程序可接收的數(shù)據(jù)包流。且因為Mealy machine是從協(xié)議程序中學習推斷得到的，這些具體的數(shù)據(jù)包按照狀態(tài)驅(qū)動中的順序可以依次被協(xié)議程序接收，并將協(xié)議程序的狀態(tài)調(diào)整到該狀態(tài)驅(qū)動對應的狀態(tài)上。

采用L*算法獲取到目標協(xié)議程序的狀態(tài)機信息后，可以根據(jù)分析需要選擇一個或多個協(xié)議狀態(tài)對其采用符號執(zhí)行技術(shù)做分析。首先依據(jù)算法1獲取感興趣狀態(tài)的驅(qū)動集，通過將狀態(tài)驅(qū)動集中的狀態(tài)驅(qū)動映射到具體數(shù)據(jù)流后輸入?yún)f(xié)議程序中，調(diào)整協(xié)議程序達到相應的協(xié)議狀態(tài)。盡管一個狀態(tài)的不同狀態(tài)驅(qū)動都能夠?qū)f(xié)議程序引導到該協(xié)議狀態(tài)，但不同狀態(tài)驅(qū)動引導的同一協(xié)議狀態(tài)的程序上下文會有差別。同一抽象狀態(tài)的不同上下文，也會造成符號執(zhí)行在分析過程中所覆蓋的路徑有所差異。僅一條狀態(tài)驅(qū)動不能完全覆蓋該協(xié)議狀態(tài)的執(zhí)行路徑。為此，在分析某一狀態(tài)時，多個協(xié)議程序在初始狀態(tài)下并行執(zhí)行，通過不同狀態(tài)驅(qū)動對應的packets flow來調(diào)整其符號執(zhí)行時的起始狀態(tài)，如圖2所示。

圖2 狀態(tài)驅(qū)動指導協(xié)議符號執(zhí)行

Figure 2 Protocol symbol execution under the guidance of state-driver set

因為有目標協(xié)議程序的Mealy machine的輔助信息，通過如圖2所示的操作過程，可以靈活選取某個協(xié)議狀態(tài)，自由控制協(xié)議程序執(zhí)行到該狀態(tài)并以此為起點對協(xié)議程序進行符號執(zhí)行分析。讓符號執(zhí)行引擎的注意力集中在某個指定狀態(tài)上，避免了因協(xié)議程序路徑復雜，符號執(zhí)行分析時無法及時有效探索重要程序空間。在由state-driver調(diào)整好協(xié)議程序到目標狀態(tài)后，利用該狀態(tài)的state-explorer集來制定具體的符號執(zhí)行策略，即確定一個state-explorer對應的數(shù)據(jù)包中哪些域是symbolic域，哪些是conclic域。一個狀態(tài)的state-explorer對應協(xié)議程序在該狀態(tài)下可接收的一個消息類型，所以該方法的符號執(zhí)行策略是一次符號執(zhí)行且僅利用一個數(shù)據(jù)包為基礎(chǔ)語料庫，即符號執(zhí)行所探索的協(xié)議狀態(tài)機的深度僅為1，如圖3所示。一方面，深度為2的探索空間可以在對該條state-driver對應的下一個狀態(tài)探索時覆蓋，更大的深度依次類推；另一方面，將探索空間限定在該協(xié)議狀態(tài)的局部可以進一步為符號執(zhí)行引擎減輕工作負荷。

3.5 密碼學代碼的處理

上文介紹了在對安全協(xié)議代碼采用符號執(zhí)行時路徑空間爆炸問題的解決方案，即用狀態(tài)驅(qū)動有針對性地引導符號執(zhí)行的路徑空間探索，而非常規(guī)地扁平化地執(zhí)行分析。本節(jié)介紹在安全協(xié)議代碼符號執(zhí)行時面臨的另一個典型問題，即符號表達式約束求解難的解決方法。

安全協(xié)議代碼中密碼學操作函數(shù)占據(jù)一定的比例，且屬于頻繁被調(diào)用的處理邏輯模塊。典型的安全協(xié)議（如TLS、SSH等）在會話協(xié)商完成之后，所有的消息都會有加解密和認證碼操作，用于確保通信數(shù)據(jù)的機密性和不可篡改性等。經(jīng)典的密碼算法會采取如擴散、混淆等技術(shù)對輸入進行處理，一般還要求具備雪崩效應，即對輸入的微小改變會導致輸出完全不同。但這些復雜的處理邏輯嚴重阻礙了協(xié)議代碼的符號執(zhí)行分析過程，主要原因有兩方面：第一，進入密碼算法中的迭代、混淆等處理邏輯內(nèi)部進行分析是復雜且收效甚微的，因為多數(shù)情況下安全協(xié)議中的密碼算法會采用NIST標準算法和成熟的密碼庫實現(xiàn)，這些算法由草案成為標準的過程中經(jīng)過了密碼學家和學者的專業(yè)經(jīng)驗分析；第二，當符號化變量經(jīng)過這些密碼算法的處理代碼后，路徑約束表達式會變得很復雜，當前最先進的SMT求解器（如Z3、STP等）需消耗大量運算時間來求解這些表達式。本文嘗試對常用的加密算法（AES、chacha20等），以及哈希算法（SHA-1、MD5等）的C代碼實現(xiàn)采用符號執(zhí)行分析，實踐結(jié)果表明，產(chǎn)生的路徑約束表達式會讓SMT求解器消耗相當長時間而致使符號執(zhí)行引擎難以有效分析。以AES-128-CBC的加密函數(shù)為例，僅將輸入的1字節(jié)符號化后產(chǎn)生的符號表達式，STP求解器耗費數(shù)十分鐘才求解完畢。即便采用具體執(zhí)行的窮舉策略，數(shù)秒內(nèi)就可窮盡出該問題的求解，這與符號執(zhí)行的技術(shù)原理有關(guān)。

為解決安全協(xié)議代碼中密碼學相關(guān)邏輯造成的路徑約束表達式復雜而難求解的問題，本文基于經(jīng)典協(xié)議形式化驗證理論中的Dolev-Yao模型來解決，即把Dolev-Yao敵手模型中的完美密碼假設(shè)理論拓展到密碼算法實現(xiàn)上。在分析時，本文將協(xié)議交互邏輯和密碼學模塊邏輯分離，并假設(shè)密碼學相關(guān)模塊的代碼實現(xiàn)是完美和值得信任的。盡管其中仍可能存在脆弱點，但這些問題的發(fā)掘需依賴較高的密碼學專業(yè)知識和經(jīng)驗，對密碼學相關(guān)代碼的安全性分析超出本文的研究范圍。當符號執(zhí)行分析到密碼學函數(shù)模塊時，根據(jù)協(xié)議狀態(tài)所處的不同階段分情況采取具體執(zhí)行和“繞過”兩種策略來分析密碼函數(shù)的代碼邏輯，以避免增加符號約束公式的求解復雜度。

典型的安全協(xié)議通?？梢苑譃闀拝f(xié)商和傳輸通信兩個階段，如圖4(a)所示。會話協(xié)商階段通信雙方除確定協(xié)議軟件和協(xié)議版本外，還會通過密鑰交換協(xié)商出后續(xù)傳輸通信階段所要使用的各種密碼套件和相應的密鑰。會話協(xié)商階段完成后，通信雙方或多方后續(xù)通信所使用的加解密、簽名、完整性校驗等各類密碼算法及密鑰信息已經(jīng)確定。在這之后的會話傳輸通信將在由會話協(xié)商階段產(chǎn)生的密鑰及密碼套件構(gòu)建的安全信道中進行。圖4(b)是相應的狀態(tài)轉(zhuǎn)換圖，此處省略了轉(zhuǎn)移條件信息。從初始狀態(tài)經(jīng)歷會話協(xié)商后到達會話協(xié)商完成狀態(tài)，會話通信階段的各個狀態(tài)均在此狀態(tài)基礎(chǔ)上根據(jù)相應的轉(zhuǎn)移條件觸發(fā)到達。

圖3 將state-driver和state-explorer組合對某一協(xié)議狀態(tài)符號執(zhí)行

Figure 3 Analyze a protocol state by combining state-driver and state-explorer

圖4 安全協(xié)議會話階段和狀態(tài)轉(zhuǎn)換

Figure 4 Session phases and state transitions of a security protocol

根據(jù)安全協(xié)議密碼算法應用的不同階段，對其處理有所不同。在會話協(xié)商階段的各個狀態(tài)探索時，輸入數(shù)據(jù)包序列中的密鑰參數(shù)字段，即密碼算法的輸入采用concrete execution策略；同時對非密鑰參數(shù)字段符號化來探索其他的路徑分支。采用具體值可以快速通過密碼算法代碼處理過程，而不至造成分析引擎停留在密碼函數(shù)處理邏輯的時間過長，更不會形成復雜的約束條件，concrete輸入即使經(jīng)過復雜處理過程的輸出仍是concrete值。對于會話通信階段，所有的數(shù)據(jù)都會被加密，若全都采用具體值分析，則僅能分析單一的執(zhí)行路徑，而采用符號執(zhí)行，則仍面臨約束表達式求解困難的問題。本文把一個密碼函數(shù)的符號執(zhí)行分析，改為對其替代封裝（wrapper）函數(shù)wrap_f的執(zhí)行。wrapper函數(shù)wrap_f與原密碼函數(shù)的輸入輸出具有相同的形式，但僅從代碼形式上的模擬并非執(zhí)行邏輯。圖5是加密函數(shù)cipher的wrapper函數(shù)wrap_cipher示例，經(jīng)過模擬函數(shù)wrap_cipher后得到的密文和明文是相同的，僅會對傳入?yún)?shù)做一些基本的合規(guī)性檢測。對密碼函數(shù)的輸入長度與輸出長度不等的情況，采用簡單的截取或填充的方式處理。符號變量sym_var經(jīng)過密碼函數(shù)后變?yōu)?sym_var)，在對應的path condtion符號公式求解時，會被替換成wrap_f(sym_var)。由于函數(shù)是一個復雜函數(shù)，而wrap_f是一個簡單函數(shù)，這樣的替換會極大降低SMT求解器的工作負擔。

圖5 密碼模塊模擬函數(shù)示例

Figure 5 An example of a cipher simulation function

4 實驗評估：在Dropbear上的實踐

為了評估方法在安全協(xié)議實現(xiàn)分析方面的有效性，本文選取了被廣泛使用的安全協(xié)議SSH以及其開源項目實現(xiàn)Dropbear源碼作為分析測試對象。SSH協(xié)議被設(shè)計用于在不受信任的網(wǎng)絡(luò)中實現(xiàn)安全遠程登錄和其他安全網(wǎng)絡(luò)服務(wù)，具體協(xié)議細節(jié)可參考RFC4251[18]。該協(xié)議由傳輸協(xié)議、用戶身份驗證協(xié)議和連接協(xié)議3個組件構(gòu)成。傳輸協(xié)議主要任務(wù)是在不安全網(wǎng)絡(luò)上提供安全通道，包括通信的機密性和完整性、可選的壓縮方案以及客戶端對服務(wù)端的身份認證方式等；用戶身份驗證協(xié)議規(guī)定了服務(wù)端對客戶端登錄用戶身份認證的機制；連接協(xié)議用于在安全的（機密性和完整性）和認證授權(quán)過的通道上以多路復用的方式傳輸應用數(shù)據(jù)。SSH協(xié)議被視為當前服務(wù)器遠程配置和運維的首選方案。Dropbear是輕量級的SSH協(xié)議開源項目，支持POSIX平臺且內(nèi)存占用量小，可以作為Openssh替代方案，當前被廣泛部署在嵌入式設(shè)備上。本文選取SSH協(xié)議和Dropbear作為評估測試對象的主要原因有兩點：第一，SSH協(xié)議是應用廣泛的典型安全協(xié)議，協(xié)議的復雜度適中且具有眾多開源實現(xiàn)，便于研究分析；第二，Dropbear是C代碼開源項目，代碼量適中，適合后續(xù)采用基于源碼的符號執(zhí)行KLEE來作分析，且Dropbear項目中自帶基于libFuzzer庫的模糊測試用例，便于測試方案的評估對比。

4.1 對Dropbear進行模型學習

方案實施的第一階段是模型學習，即利用MAT模型學習框架對DropbearSSH進行模型學習，推導其Mealy machine模型。這部分工作主要基于Paul等[1]SSH模型學習的開源工作并有少許細節(jié)上的改動。實驗設(shè)置如下：被測對象為在vmware虛擬機 ubuntu16.04系統(tǒng)中編譯運行Dropbear v2020.80版本服務(wù)端程序；Learner運行在4 GB內(nèi)存、處理器為Intel core i5-8500. Ubuntu16.04系統(tǒng)的虛擬機中。

在采用modellearning技術(shù)對Dropbear的模型之前，需要先確定輸入集合。本文沿用文獻[1]的策略把SSH消息類型作為輸入集合。同時，為了簡化狀態(tài)機規(guī)模便于后續(xù)符號執(zhí)行工作，本文對輸入集合進行了篩選，如去除了IGNORE、UNIMPL、DEBUG等。表1列出了實驗時采用的輸入消息集合、對應的消息類型，有關(guān)這些消息類型的詳細說明可參考SSH的RFC文檔[18]和文獻[1]。

最終確定的狀態(tài)數(shù)量為25個。如圖6所示，紅色軌跡標注了常規(guī)測試套件的協(xié)議測試路徑，將其稱為主干路徑。主干路徑的狀態(tài)遷移如下。

表1 Dropbear的模型學習輸入/輸出字母表

Figure 6 Learnedstatemachine (Mealy machine) model forDropbear

經(jīng)過簡單的分析，可以辨別出狀態(tài)編號對應的實際狀態(tài)含義。如s0為初始化狀態(tài)，s4為密鑰協(xié)商完成狀態(tài)，s6為用戶通過認證后的狀態(tài)等。學習得出的Mealy machine中包含的主干路徑為常規(guī)測試套件的測試路徑，因此可以得出初步的定性結(jié)論：學習得到的Mealy machine信息來指導符號執(zhí)行，在理論上不低于常規(guī)測試套件的代碼覆蓋率。

4.2 Dropbear源碼的符號執(zhí)行

在得到Dropbear程序的Mealy machine信息后，可以選取感興趣的協(xié)議狀態(tài)，用算法1獲取該狀態(tài)的狀態(tài)驅(qū)動集。表2列出了Dropbear的各抽象狀態(tài)對應的狀態(tài)驅(qū)動集數(shù)量，即驅(qū)動集的基數(shù)。

表2 Dropbear各狀態(tài)對應的狀態(tài)驅(qū)動數(shù)（狀態(tài)驅(qū)動集基數(shù)）

以s15狀態(tài)為例，根據(jù)算法1得到的狀態(tài)驅(qū)動集共有54條狀態(tài)驅(qū)動，如圖7所示。從表1中可以看出，一部分狀態(tài)的狀態(tài)驅(qū)動數(shù)量達到幾百條甚至近千條的規(guī)模，如狀態(tài)s24的狀態(tài)驅(qū)動數(shù)量達972條。這意味著有972種不同的輸入可以讓Dropbear服務(wù)端程序從初始狀態(tài)到達狀態(tài)s24。Mealy machine僅是協(xié)議程序的高級抽象信息，到達一個狀態(tài)的路徑數(shù)量達幾百條，當對應到協(xié)議程序的執(zhí)行空間時，執(zhí)行路徑的分支數(shù)量會急劇增加。在沒有狀態(tài)信息指導的情況下，符號執(zhí)行引擎很難快速分析這些路徑分支。

圖7 狀態(tài)s15狀態(tài)驅(qū)動集

Figure 7 The state driver set of state s15

狀態(tài)驅(qū)動到具體數(shù)據(jù)包序列的轉(zhuǎn)換器mapper重用了模型學習階段的轉(zhuǎn)換模塊，調(diào)用了手工改寫的Paramiko庫。符號執(zhí)行工具采用了基于llvm的開源分析引擎KLEE，它可以對源碼編譯后的llvm字節(jié)碼進行符號執(zhí)行。由于KLEE不支持socket函數(shù)建模，但可以支持文件的靜態(tài)讀寫。為此，在實驗時socket相關(guān)的函數(shù)都采用文件讀寫操作進行了替代。

為了說明本文方法的有效性，對比實驗對象為Dropbear自帶的fuzz測試模塊fuzzer-preauth。主要對比SSH傳輸協(xié)議階段代碼的分析效率，主要的評價指標為代碼覆蓋率和檢出錯誤率。其中，代碼覆蓋率采用Clang基于源碼的覆蓋率功能(-fprofile-instr-generate -fcoverage-mapping選項)測算結(jié)果，以執(zhí)行的源代碼行數(shù)占比作為代碼覆蓋率的計算方式，并去除為測試添加的代碼及覆蓋率0%的代碼文件。檢測的目標代碼錯誤為人工設(shè)計并添加到分析對象代碼中的代碼問題。添加錯誤的位置平均分布在傳輸協(xié)議階段相關(guān)的4個消息處理例程（recv_msg_kexinit，recv_msg_ kexdh_init, recv_msg_newkeys, recv_msg_service_ request）以及公共代碼中，各部分各4個，即共有20個代碼錯誤，具體實驗結(jié)果如表3所示。

由于本文方法在NEWKEYS消息之前采用具體合法值輸入密碼學函數(shù)代碼中，NEWKEYS之后采用繞過策略，而Libfuzzer測試套件未對此有特殊區(qū)分，因此將Dropbear源碼中的libtocrypt庫源碼不計入源碼覆蓋率的計算中時，LibFuzzer測試套件的代碼覆蓋率上下降了約4%；而state-driver方式在不含libtocrypt庫時代碼覆蓋率優(yōu)于代碼覆蓋率。在檢測出錯誤方面，Libfuzzer測試套件可以檢測出13個設(shè)計的錯誤，而State-driver方式可以覆蓋到這些錯誤的執(zhí)行點。這與20個錯誤的構(gòu)造位置有關(guān)，在設(shè)計這些錯誤時特意選取了常規(guī)方式不容易到達的分支執(zhí)行點上，而這正是符號執(zhí)行技術(shù)的優(yōu)勢所在。對比實驗未采用Mealy machine信息指引的常規(guī)執(zhí)行策略，經(jīng)實踐發(fā)現(xiàn)，即使KLEE這樣先進的符號執(zhí)行引擎在處理類似Dropbear的安全協(xié)議源碼時也不能直接適用，最終會因系統(tǒng)資源耗盡而終止。

表3 方法與自帶測試套件對比

5 結(jié)束語

符號執(zhí)行在對安全協(xié)議程序分析時，存在路徑SMT求解困難等兩個顯著問題，這也是符號執(zhí)行技術(shù)對大型軟件程序分析所面臨的局限性。本文方法不改進通用符號執(zhí)行技術(shù)，而從安全協(xié)議程序的自身特點出發(fā)，提出了一種對安全協(xié)議代碼空間進行符號執(zhí)行的技術(shù)思路。通過將模型學習得到的狀態(tài)機信息轉(zhuǎn)換為狀態(tài)驅(qū)動集，以狀態(tài)驅(qū)動集指導符號執(zhí)行引擎對協(xié)議程序的某一狀態(tài)進行符號執(zhí)行分析，可以靈活高效地控制協(xié)議程序空間的路徑探索；基于Dolev-Yao模型的完美密碼假設(shè)理論，將密碼學函數(shù)邏輯空間與協(xié)議交互邏輯空間分離，可以避免因密碼學邏輯的復雜性造成路徑約束求解困難問題。

[1] FITER?U-BRO?TEAN P. Model learning and model checking of SSH implementations[C]//Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. 2017.

[2] ANGLUIN D. Learning regular sets from queries and counterexamples[J]. Information and Computation, 1987, 75(2): 87-106.

[3] GUO J, GU C, CHEN X, et al. Model learning and model checking of IPSec implementations for internet of things[J]. IEEE Access, 2019, 7: 171322-171332.

[4] FITERAU-BROSTEAN P, JONSSON B, MERGET R, et al. Analysis of DTLS implementations using protocol state fuzzing[C]//29th {USENIX} Security Symposium ({USENIX} Security 20). 2020: 2523-2540.

[5] CHAU S Y, CHOWDHURY O, HOQUE E, et al. Symcerts: practical symbolic execution for exposing noncompliance in X.509 certificate validation implementations[C]//2017 IEEE Symposium on Security and Privacy (SP). 2017: 503-520.

[6] CORIN R, MANZANO F A. Efficient symbolic execution for analysing cryptographic protocol implementations[C]//International Symposium on Engineering Secure Software and Systems. 2011: 58-72.

[7] VANHOEF M, PIESSENS F. Symbolic execution of security protocol implementations: handling cryptographic primitives[C]//12th {USENIX} Workshop on Offensive Technologies ({WOOT} 18). 2018.

[8] CHAU S Y, YAHYAZADEH M, CHOWDHURY O, et al. Analyzing semantic correctness with symbolic execution: a case study on pkcs# 1 v1. 5 signature verification[C]//Network and Distributed Systems Security (NDSS) Symposium 2019. 2019.

[9] 孟博, 魯金鈿, 王德軍,等. 安全協(xié)議實施安全性分析綜述[J]. 山東大學學報:理學版, 2018, 53(1): 1-18.

MENG B, LU J T, WANG D J, et al. Survey of security analysis of security protocol implementations[J]. Journal of Shandong University (Natural Science), 2018, 53(1): 1-18.

[10] AICHERNIG B K, MOSTOWSKI W, MOUSAVI M R, et al. Model learning and model-based testing[M]//Machine Learning for Dynamic Software Analysis: Potentials and Limits. 2018: 74-100.

[11] JERO S, HOQUE M E, CHOFFNES D R, et al. Automated attack discovery in TCP congestion control using a model-guided approach[C]//NDSS. 2018.

[12] JERO S, LEE H, NITA-ROTARU C. Leveraging state information for automated attack discovery in transport protocol implementations[C]//2015 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. 2015: 1-12.

[13] WALLS R J, BRUN Y, LIBERATORE M, et al. Discovering specification violations in networked software systems[C]//2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE). 2015: 496-506.

[14] SONG J S, CADAR C, PIETZUCH P. SymbexNet: testing network protocol implementations with symbolic execution and rule-based specifications[J]. IEEE Transactions on Software Engineering, 2014, 40(7): 695-709.

[15] ALSHMRANY K, CORDEIRO L. Finding security vulnerabilities in network protocol implementations[J]. arXiv preprint arXiv: 2001.09592, 2020.

[16] 謝肖飛, 李曉紅, 陳翔, 等.基于符號執(zhí)行與模糊測試的混合測試方法[J].軟件學報, 2019, 30(10): 3071-3089.

XIE X F, LI X H, CHEN X, et al. Hybrid testing based on symbolic execution and fuzzing[J]. Journal of Software, 2019, 30(10): 3071-3089.

[17] CHO C Y, BABIC D, POOSANKAM P, et al. MACE: model-inference-assisted concolic exploration for protocol and vulnerability discovery[C]//USENIX Security Symposium. 2011: 139.

[18] YLONEN T, LONVICK C. The secure shell (SSH) protocol architecture[S]. RFC4251, Internet Engineering Task Force, 2006.

Security protocol code analysis method combining model learning and symbolic execution

ZHANG Xieli1,2, ZHU Yuefei1,2, GU Chunxiang1,2, CHEN Xi1,2

1. State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou 450001, China 2.Henan Key Laboratory of Network Cryptography Technology, Zhengzhou 450002, China

Symbolic execution can comprehensively analyze program execution space in theory, but it is not feasible in practice for large programs like security protocols, due to the explosion of path space and the limitation of difficulty in solving path constraints. According to the characteristics of security protocol program, a method to guide the symbolic execution of security protocol code by using protocol state machine information obtained from model learning was proposed. At the same time, by separating cryptographic logic from protocol interaction logic, the problem that path constraints cannot be solved caused by the complexity of cryptographic logic is avoided. The feasibility of the method is demonstrated by the practice on the SSH open source project Dropbear. Compared with Dropbear's test suite, the proposed method has advantages in code coverage and error point discovery.

model learning, symbolic execution, security protocol code, state-driver

TP311

A

10.11959/j.issn.2096?109x.2021067

2021?02?19；

2021?03?29

顧純祥，gcxiang520@aliyun.com

國家重點研發(fā)計劃(2019QY1302)

TheNational Key R&D Program of China (2019QY1302)

張協(xié)力, 祝躍飛, 顧純祥, 等. 模型學習與符號執(zhí)行結(jié)合的安全協(xié)議代碼分析技術(shù)[J]. 網(wǎng)絡(luò)與信息安全學報, 2021, 7(5): 93-104.

ZHANG X L, ZHU Y F, GU C X, et al. Security protocol code analysis method combining model learning and symbolic execution[J]. Chinese Journal of Network and Information Security, 2021, 7(5): 93-104.

張協(xié)力（1992?），男，陜西興平人，數(shù)學工程與先進計算國家重點實驗室博士生，主要研究方向為網(wǎng)絡(luò)安全協(xié)議。

顧純祥（1976?），男，安徽霍山人，博士，數(shù)學工程與先進計算國家重點實驗室教授，主要研究方向為網(wǎng)絡(luò)安全、密碼學。

祝躍飛（1962?），男，浙江蘭溪人，博士，數(shù)學工程與先進計算國家重點實驗室教授、博士生導師，主要研究方向為網(wǎng)絡(luò)安全、密碼學。

陳熹（1988?），男，湖北建始人，碩士，數(shù)學工程與先進計算國家重點實驗室講師，主要研究方向為網(wǎng)絡(luò)安全、密碼學。