基于靜態(tài)分析的密碼協(xié)議業(yè)務邏輯缺陷檢測方法

中國人民解放軍63891 部隊 王震 周超 苗泉強 樊永文

本文介紹了基于靜態(tài)分析的密碼協(xié)議業(yè)務邏輯缺陷檢測的具體方法，從檢測框架出發(fā)，引出了方法實現(xiàn)的三個關(guān)鍵問題，然后對模型代碼解析、協(xié)議代碼信息抽取以及映射關(guān)系建立這三個關(guān)鍵問題進行了詳細的分析論述。

對密碼協(xié)議進行形式化分析，從協(xié)議業(yè)務邏輯層面上證明密碼協(xié)議的安全或者是找出協(xié)議邏輯層面的缺陷，一旦發(fā)現(xiàn)協(xié)議的缺陷，協(xié)議規(guī)范需要重新修訂，并且協(xié)議代碼也要做相應的修改[1]。但是形式化驗證的依據(jù)是協(xié)議規(guī)范，而協(xié)議代碼與協(xié)議規(guī)范之間存在著一定的差異，如果僅靠人工去定位代碼中的缺陷那必定是效率極低的，所以本文提出一套基于靜態(tài)分析的協(xié)議業(yè)務邏輯缺陷檢測技術(shù)方法，利用已有的形式化驗證結(jié)果自動化地在協(xié)議代碼中定位缺陷[2-4]。該方法的整體思想是將源代碼轉(zhuǎn)換為程序抽象模式，比如函數(shù)調(diào)用圖(Call Graph，CG)和控制流圖(Control Flow Graph，CFG)，同時解析形式化模型，得到規(guī)則依賴圖(Dependency Graph，DG)，根據(jù)圖中的節(jié)點信息建立映射關(guān)系。得到映射關(guān)系后，當通過前述形式化驗證技術(shù)發(fā)現(xiàn)模型存在缺陷時，可定位協(xié)議代碼中的缺陷位置，并確定理論缺陷是否存在于實際代碼中[5，6]。業(yè)務邏輯缺陷檢測系統(tǒng)框架如圖1所示。

圖1 業(yè)務邏輯缺陷檢測系統(tǒng)框架圖Fig.1 Framework diagram of business logic defect detection system

為了實現(xiàn)上述技術(shù)方法，需要解決以下三個關(guān)鍵問題：模型代碼解析、協(xié)議代碼信息抽取以及映射關(guān)系建立。

1 模型代碼解析

模型代碼是一個形式化模型文件，解析后得到的是協(xié)議構(gòu)造的內(nèi)部表示以及形式化模型的規(guī)則依賴圖DG，首先需要對輸入文件進行預處理，方便后面更容易地進行解析。

1.1 預處理輸入文件

對形式化模型代碼進行解析之前，需要對其進行一些預處理，大致分為以下三步。首先，去除單行和多行注釋，形式化模型代碼采用C 風格注釋，“//”標識單行注釋，“/*”與“*/”標識多行注釋。其次，定位Lemma 關(guān)鍵詞，刪除所有的Lemma，因為Lemma 編寫了對安全屬性的驗證過程，而在此處只考慮對協(xié)議進行描述的Rules，不考慮Lemma 的內(nèi)容。最后，定位End關(guān)鍵詞并移除其后面的內(nèi)容。

1.2 中間表示

對模型代碼進行解析，也就是對其包含的Equations、Functions、Builtins 以及Rules 進行解析。其中，最為重要的是對Rules 進行解析，而要解析Rules 就需要對其包含的Facts 進行解析。為了解析這些結(jié)構(gòu)，在實現(xiàn)中創(chuàng)建了三種類型的對象：Operators、Rules 和Equations。

Operators 有一個名稱，由字符串和參數(shù)組成，其中參數(shù)也是Operators，可以獲取操作符的屬性，以及獲取和設置其名稱和參數(shù)。每個Operators 還有一個多重性和一個類型。Operators 的多重性只與Facts 相對應的運算符有關(guān)，它表示在協(xié)議中Facts 出現(xiàn)在規(guī)則左側(cè)的次數(shù)。類型與形式化驗證中的術(shù)語操作符相關(guān)，它可以是一個帶有參數(shù)的函數(shù)，也可以是None，用于區(qū)分函數(shù)與變量。

Rules 由名稱、左參數(shù)、右參數(shù)、連接關(guān)系和多重性組成。名稱為字符串，對應于規(guī)則的名稱。左右參數(shù)為Operators 數(shù)組，分別對應于左和右的Facts 集合。連接關(guān)系是一個Rules 數(shù)組，多重性是一個整數(shù)。

Equations 只有兩個部分，分別都是Operators，對應于方程式的左右兩項。

1.3 對預處理后的文件進行解析

（1）解析Functions，由Functions 關(guān)鍵字后面列出的所有函數(shù)組成，它們被表示為一個函數(shù)名，后面跟著一個斜杠，然后是函數(shù)的參數(shù)數(shù)量，內(nèi)部表示為一個元組數(shù)組，元組中第一個參數(shù)為函數(shù)名稱，第二個參數(shù)為函數(shù)的參數(shù)數(shù)量。

（2）解析Builtins，其內(nèi)部表示為字符串數(shù)組。在手動查找了所有包含Builtins 的形式化模型文件后，對其進行硬編碼，將所有函數(shù)添加到現(xiàn)有函數(shù)數(shù)組中，并將由Equations 關(guān)鍵字和方程列表組成的字符串附加到文件中，這樣就可以像處理其他方程一樣處理它們了。

（3）解析Equations，它包括一個左參數(shù)，后面跟著一個等號，再后面跟著一個右參數(shù)。這些參數(shù)在內(nèi)部表示為Operators。如果參數(shù)是一個函數(shù)，那么它的參數(shù)就是Operators 的參數(shù)，它的函數(shù)名就是Operators 的名稱。如果參數(shù)是一個變量，則對應的Operators 具有與該變量相同的名稱，并且沒有參數(shù)。

為了解析Rules，首先必須添加一個新的規(guī)則，該規(guī)則在形式化驗證工具內(nèi)部中存在，但是不在模型文件中。這個規(guī)則就是“新鮮規(guī)則”，定義如下：

rule Fresh_rule：

[]--＞ [Fr(~x)]

此規(guī)則用于創(chuàng)建新的變量，并且沒有前置條件，因此，它總是可以被執(zhí)行。這在執(zhí)行模擬中非常重要，表示從一個空狀態(tài)開始。

（4）解析Rules。在解析規(guī)則R 時，首先考慮let(R)。我們對left(R)和right(R)進行必要的替換。在left(R)和right(R)里面可以有零個、一個或多個Facts。因此，我們在內(nèi)部將這些Facts 表示為Operators。R 表示為一個名稱為R 的Rule，left(R)和right(R)分別表示左右facts 對應的Operators 數(shù)組，初始時沒有連接關(guān)系，多樣性為0。

如圖2所示顯示了Rules 的可視化解析過程，其中Rules 和Operators 用它們的名稱表示。在該規(guī)則中，左邊有兩個事實，右邊有兩個事實，它們由Operator 表示。所有操作符都可以連接到其他操作符的列表。如果一個操作符沒有任何參數(shù)，它對應于一個變量，如k_A或一元函數(shù)，如g。

圖2 形式化模型規(guī)則解析圖Fig.2 Formal model rule analysis diagram

接下來，為了得到規(guī)則之間可能的執(zhí)行順序，需要創(chuàng)建一個規(guī)則依賴圖DG，可以用一個有向無環(huán)圖來描述DG，節(jié)點是模型中的規(guī)則，邊代表著依賴關(guān)系，假定這個圖為G，點集為V(G)，邊集為E(G)，對于R1∈V(G)，R2∈V(G)，如果R2的左邊有一個Operator 與R1的右邊的一個Operators 具有相同的名稱和參數(shù)個數(shù)，并且參數(shù)是統(tǒng)一的，則這兩個節(jié)點之間存在一條邊。該圖顯示了為了能夠執(zhí)行給定的規(guī)則，可能需要已經(jīng)執(zhí)行了哪些規(guī)則。下面給出規(guī)則依賴圖的定義：

令R1，R2∈V(G)

(R1，R2)∈E(G) ?F ∈left(R2)，F(xiàn)’∈right(R1)，s.t.name(F) = name(F’)，

arity(F) = arity(F’)

至此，對輸入的模型文件的解析就完成了。其中有一點需要說明，對于那些右側(cè)只包含Out 事實，并且左邊只有持久事實或者新鮮事實的規(guī)則，在解析時都不做分析，而是直接進行了刪除，因為一般來說，這些規(guī)則不屬于協(xié)議參與方之間的交互，在協(xié)議代碼中不會存在與之相關(guān)的實現(xiàn)。

2 協(xié)議代碼信息抽取

協(xié)議代碼是對協(xié)議規(guī)范的實現(xiàn)，與協(xié)議規(guī)范之間存在差距，包含實現(xiàn)細節(jié)與底層操作，而協(xié)議的形式化模型是對協(xié)議規(guī)范的高度抽象，要建立二者之間的映射關(guān)系，首先需要對源代碼進行信息提取和變換，由于C/C++常常被用作安全協(xié)議開發(fā)所使用的高級語言，因此這里關(guān)注于由C/C++編寫的協(xié)議代碼。

程序分析一般分為兩類方法，動態(tài)分析和靜態(tài)分析。動態(tài)分析通過運行程序來得到程序運行的各個狀態(tài)，構(gòu)建程序模型的方法效率低、不適用于大規(guī)模程序，而網(wǎng)絡協(xié)議的代碼規(guī)模通常都很大，所以利用靜態(tài)分析更加合適，靜態(tài)分析不需要運行程序，通過詞法分析、語法分析、控制流、數(shù)據(jù)流分析等技術(shù)對程序代碼進行掃描來獲得程序的信息。相比之下，靜態(tài)分析可以做到更早、更全面、更高效和更低成本地發(fā)現(xiàn)程序的缺陷。

為了獲取函數(shù)名，構(gòu)建函數(shù)調(diào)用圖CG，圖中的節(jié)點是方法，邊表示調(diào)用關(guān)系。下面給出一個代碼片段作為示例：

int foo(int t){

bar1()；

bar2()；

if(t ＞ 0) return t；

else return 0；

}

在這段代碼中，方法foo()調(diào)用了方法bar1()和方法bar2()，則CG 中應有一條從foo()到bar1()的有向邊，以及一條從foo()到bar2()的有向邊，如圖3所示。

圖3 函數(shù)調(diào)用圖CGFig.3 Function call diagram CG

為了獲取程序在執(zhí)行過程中會遍歷到的路徑，構(gòu)建控制流圖CFG。控制流程圖是用在編譯器中的一個抽象數(shù)據(jù)結(jié)構(gòu)，由編譯器在內(nèi)部維護，是對程序的一個抽象表現(xiàn)，圖中的節(jié)點是語句或者是基本塊，在一個基本塊中，語句都是順序執(zhí)行的，只可以從入口語句開始執(zhí)行，直至執(zhí)行到最后一條語句，邊表示執(zhí)行流，在遇到條件語句時產(chǎn)生分支。例如語句A 執(zhí)行后的下一條語句是B，則CFG 中應有一條從A 到B 的有向邊。條件語句（if-else，while-do）之后可能執(zhí)行的語句不止一個，可能執(zhí)行true-branch 或false-branch，所以CFG 上條件語句節(jié)點的后綴會有多個，表示其后可能執(zhí)行的不同branches，上述代碼片段的CFG 如圖4所示。

圖4 控制流圖CFGFig.4 Control flow graph CFG

3 映射關(guān)系建立

通常情況下，研究人員在為協(xié)議建立形式化模型時，會遵循一定的規(guī)律，規(guī)則和變量的名稱都會有實際的含義，下面總結(jié)出了一般建模中命名的習慣，這在匹配中起到一定的輔助作用，如表1所示。

表1 形式化模型中變量含義Tab.1 The meaning of variables in the formal mode

除此之外，本項目使用的建模語言規(guī)定了變量的四種類型：

~x 表示x 是新鮮的

$x 表示x 是公開的

#i 表示i 是暫時的

m 表示消息m

首先，先序遍歷協(xié)議代碼的CG，利用形式化模型中的規(guī)則與協(xié)議代碼的方法進行模糊匹配，篩選掉大部分不匹配的代碼段，找出匹配度較高的代碼片段，偽代碼如下所示：

執(zhí)行匹配算法之后，可能會得到多個匹配代碼片段，或者是一個也沒有，對于沒有結(jié)果的情況，通過審查很容易分析出原因，而對于多重結(jié)果的情況，需要再去利用結(jié)果片段里的代碼CFG 來做篩查，通過類似的遍歷方式，獲取CFG 中的變量，與形式化模型中變量的形式進行對比，就可以選擇性地保留最終的結(jié)果。

4 結(jié)語

算法1： 匹配算法Input：協(xié)議代碼C，要匹配的規(guī)則R Output：代碼片段F 1 獲取CG 根節(jié)點作為當前節(jié)點tu；2 獲取當前節(jié)點屬性；3 利用R 與當前節(jié)點屬性進行模糊匹配，匹配分值超過閾值則將tu 加入F，否則繼續(xù)執(zhí)行；4 tu.getchildren()作為當前節(jié)點，重復2、3、4 步驟；5 返回F。

本文對基于靜態(tài)分析的安全協(xié)議業(yè)務邏輯缺陷檢測技術(shù)做了詳細闡述，從研究現(xiàn)狀分析出本方法的創(chuàng)新性，然后針對方法中的三個關(guān)鍵問題，進一步地描述了方法的實現(xiàn)細節(jié)，可以為下一步研究協(xié)議代碼底層的漏洞和基于機器學習的缺陷預測技術(shù)提供技術(shù)基礎(chǔ)。