中國(guó)人民解放軍63891 部隊(duì) 王震 周超 苗泉強(qiáng) 樊永文

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

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

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

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

1 模型代碼解析

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

1.1 預(yù)處理輸入文件

對(duì)形式化模型代碼進(jìn)行解析之前，需要對(duì)其進(jìn)行一些預(yù)處理，大致分為以下三步。首先，去除單行和多行注釋?zhuān)问交Ｐ痛a采用C 風(fēng)格注釋?zhuān)?/”標(biāo)識(shí)單行注釋?zhuān)?*”與“*/”標(biāo)識(shí)多行注釋。其次，定位Lemma 關(guān)鍵詞，刪除所有的Lemma，因?yàn)長(zhǎng)emma 編寫(xiě)了對(duì)安全屬性的驗(yàn)證過(guò)程，而在此處只考慮對(duì)協(xié)議進(jìn)行描述的Rules，不考慮Lemma 的內(nèi)容。最后，定位End關(guān)鍵詞并移除其后面的內(nèi)容。

1.2 中間表示

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

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

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

Equations 只有兩個(gè)部分，分別都是Operators，對(duì)應(yīng)于方程式的左右兩項(xiàng)。

1.3 對(duì)預(yù)處理后的文件進(jìn)行解析

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

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

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

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

rule Fresh_rule：

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

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

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

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

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

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

令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’)

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

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

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

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

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

int foo(int t){

bar1()；

bar2()；

if(t ＞ 0) return t；

else return 0；

}

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

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

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

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

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

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

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

除此之外，本項(xiàng)目使用的建模語(yǔ)言規(guī)定了變量的四種類(lèi)型：

~x 表示x 是新鮮的

$x 表示x 是公開(kāi)的

#i 表示i 是暫時(shí)的

m 表示消息m

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

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

4 結(jié)語(yǔ)

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

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