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

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

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

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

1 模型代碼解析

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

1.1 預處理輸入文件

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

1.2 中間表示

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

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

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

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

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

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

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

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

為了解析Rules，首先必須添加一個新的規(guī)則，該規(guī)則在形式化驗證工具內部中存在，但是不在模型文件中。這個規(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。因此，我們在內部將這些Facts 表示為Operators。R 表示為一個名稱為R 的Rule，left(R)和right(R)分別表示左右facts 對應的Operators 數(shù)組，初始時沒有連接關系，多樣性為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ī)則，邊代表著依賴關系，假定這個圖為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’)

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

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

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

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

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

int foo(int t){

bar1()；

bar2()；

if(t ＞ 0) return t；

else return 0；

}

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

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

為了獲取程序在執(zhí)行過程中會遍歷到的路徑，構建控制流圖CFG?？刂屏鞒虉D是用在編譯器中的一個抽象數(shù)據(jù)結構，由編譯器在內部維護，是對程序的一個抽象表現(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 映射關系建立

通常情況下，研究人員在為協(xié)議建立形式化模型時，會遵循一定的規(guī)律，規(guī)則和變量的名稱都會有實際的含義，下面總結出了一般建模中命名的習慣，這在匹配中起到一定的輔助作用，如表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í)行匹配算法之后，可能會得到多個匹配代碼片段，或者是一個也沒有，對于沒有結果的情況，通過審查很容易分析出原因，而對于多重結果的情況，需要再去利用結果片段里的代碼CFG 來做篩查，通過類似的遍歷方式，獲取CFG 中的變量，與形式化模型中變量的形式進行對比，就可以選擇性地保留最終的結果。

4 結語

算法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è)務邏輯缺陷檢測技術做了詳細闡述，從研究現(xiàn)狀分析出本方法的創(chuàng)新性，然后針對方法中的三個關鍵問題，進一步地描述了方法的實現(xiàn)細節(jié)，可以為下一步研究協(xié)議代碼底層的漏洞和基于機器學習的缺陷預測技術提供技術基礎。