李均濤++唐鄭熠++張金磊

【 摘 要 】 論文提出了一種基于行為時(shí)序邏輯和片面性理論的多方協(xié)作取證的形式化方法，有望在多方參與的調(diào)查取證中驗(yàn)證不可觀察的行為證據(jù)，并將其應(yīng)用到一個(gè)取證實(shí)例中。

【 關(guān)鍵詞 】 入侵取證；行為時(shí)序邏輯；片面性；多方協(xié)作取證

【 中圖分類號(hào) 】 TP309.2

【 文獻(xiàn)標(biāo)識(shí)碼 】 A

Multilateral Cooperation Intrusion Forensics Based onTemporal Logic of Actions

LI Jun-tao 1 Tang Zheng-yi 2 Zhang Jin-lei 1

（1.Information School of Guizhou University of Finance and Ecnomics GuizhouGuiyang 550025；

2.College of Information Science and Engineering， Fujian University of Technology FujianFuzhou 350118）

【 Abstract 】 Put foreword a formalist method of multi-party cooperation intrusion forensics based on Temporal Logic of Actions and Opacity Theory， expected to verify the evidence not easy observed， and apply it to an intrusion forensic instance.

【 Keywords 】 computer intrusion forensic； temporal logic of actions； opacity； multilateral cooperation intrusion forensics

1 引言

在取證調(diào)查時(shí)，調(diào)查者的主要難題就是證明入侵者行為是否蓄意而為，這可以用系統(tǒng)狀態(tài)的性質(zhì)來(lái)刻畫，即這些狀態(tài)是否是入侵者的偽裝，這使得對(duì)它們的計(jì)算更加難以執(zhí)行。對(duì)入侵者來(lái)說(shuō)，調(diào)查者作為第三方僅有有限的關(guān)于它們攻擊行為的觀測(cè)記錄，即所能收集到的不完備的證據(jù)集。舉例來(lái)說(shuō)，一個(gè)入侵檢測(cè)系統(tǒng)的報(bào)警文件僅僅給出了有關(guān)遠(yuǎn)程執(zhí)行命令集的信息，并不能向展示系統(tǒng)是如何被攻擊的。從這一考慮出發(fā)，有必要對(duì)文獻(xiàn)[1]提出的形式化方法進(jìn)行補(bǔ)充，使之能夠證明源于入侵活動(dòng)不完全觀測(cè)的數(shù)字證據(jù)。

2 多方協(xié)作取證的理論基礎(chǔ)

不同的觀察者從不同的角度觀察同一個(gè)事務(wù)往往會(huì)得出不同的觀察結(jié)果，瞎子摸象的故事就是這種現(xiàn)象的一個(gè)典型代表。對(duì)安全事件的取證調(diào)查也會(huì)碰到這樣的情況，即不同的調(diào)查者依據(jù)各自的知識(shí)和技術(shù)，對(duì)收集到的不同證據(jù)集進(jìn)行分析，這必然會(huì)產(chǎn)生相互間的合作問(wèn)題。而這種協(xié)作也必然會(huì)給取證調(diào)查工作帶來(lái)新的性質(zhì)。

為了更好地處理多方協(xié)作取證，提出了一種片面性理論。這種理論來(lái)源于文獻(xiàn)[2]中提出的不透明性（Opacity）概念。近十幾年來(lái)，有許多關(guān)于安全性描述問(wèn)題的研究，也提出不少有價(jià)值的理論方法，其中有一些就是基于不透明性的，它已被證明是描述安全性的一種很有前途的技術(shù)。為了使之更適于取證調(diào)查任務(wù)，對(duì)其進(jìn)行擴(kuò)展，使之支持多方觀察和協(xié)作，并稱之為片面性理論。

2.1 不透明性簡(jiǎn)介

一般來(lái)講，一個(gè)給定性質(zhì)的不透明性[2]就是指：一個(gè)第三方僅能訪問(wèn)整個(gè)系統(tǒng)運(yùn)行情況的一部分（稱之為可觀察部分），而不能推斷出系統(tǒng)性質(zhì)的全部真相。不透明性的一些研究成果在應(yīng)用開(kāi)發(fā)、系統(tǒng)驗(yàn)證和可判定性證明等領(lǐng)域被認(rèn)為前景廣闊。文獻(xiàn)[3]用通信順序進(jìn)程（CSP）的表達(dá)法給出了不透明性的形式定義，其在某種程度上為表達(dá)匿名安全性提供了一個(gè)獨(dú)特的方法。它采用模型檢測(cè)技術(shù)在有限狀態(tài)模型下判定這一性質(zhì)。文獻(xiàn)[4]提出了一種更一般的描述不透明性，但不處理可判定性問(wèn)題的框架。這一框架在文獻(xiàn)[2]中得到了應(yīng)用，并使用抽象技術(shù)對(duì)不透明性質(zhì)進(jìn)行驗(yàn)證。近來(lái)，不透明性概念已逐步被擴(kuò)展到一般性系統(tǒng)，不再僅限于密碼協(xié)議方面。其中最主要的擴(kuò)展是在PETRI網(wǎng)和標(biāo)號(hào)轉(zhuǎn)移系統(tǒng)（Labeled Transition Systems）中處理不透明性證明的可判定性。

2.2 系統(tǒng)狀態(tài)和運(yùn)轉(zhuǎn)的可見(jiàn)性

依賴于觀察者所使用的技術(shù)和手段，有些系統(tǒng)的狀態(tài)變量可以觀察到，而另一些可能觀察不到，這就是要說(shuō)的可見(jiàn)性。使用TLHA規(guī)約對(duì)調(diào)查者對(duì)系統(tǒng)的觀察進(jìn)行建模，當(dāng)然要考慮這一性質(zhì)，提出狀態(tài)標(biāo)簽的概念來(lái)表示這一性質(zhì)。用ls表示狀態(tài)s的標(biāo)簽，用ls（v）表示狀態(tài)s中的一個(gè)變量v的標(biāo)簽。根據(jù)變量的可見(jiàn)程度，變量的標(biāo)簽有如下三種形式：

變量值：當(dāng)對(duì)觀察者來(lái)講一個(gè)變量可見(jiàn)且其值也可解釋時(shí)，它的值當(dāng)然就是他在狀態(tài)s中的變量值，即ls（v）=s（v）。

假設(shè)值：當(dāng)一個(gè)變量可見(jiàn)但其值不能被觀察者理解，也就是說(shuō)它的改變不能給觀察者帶來(lái)更多的信息時(shí)，比如加密或壓縮的數(shù)據(jù)，則給它指派一個(gè)靜態(tài)標(biāo)簽，即一個(gè)假設(shè)值，ls（v）=x，x∈Vh。這里Vh表示假設(shè)變量值的集合。這一假設(shè)值在運(yùn)轉(zhuǎn)中任何狀態(tài)都不會(huì)改變。

空值：當(dāng)變量完全不可見(jiàn)，當(dāng)然也沒(méi)有可確定其值的任何信息時(shí)，則在運(yùn)轉(zhuǎn)中的所有狀態(tài)都給它指定一個(gè)空值，即ls（v）=？準(zhǔn)。

狀態(tài)s的可觀察部分可以用obs（s）來(lái)表示，而obs（s）是通過(guò)計(jì)算狀態(tài)s中的每個(gè)假設(shè)變量和非假設(shè)變量的標(biāo)簽來(lái)獲取。在觀測(cè)模型中，每一個(gè)狀態(tài)都可以表示為變量標(biāo)簽的序列：obs（s）=[ls（v1）ls（v2）…ls（vn）]，其中（v1，…，vn）表示狀態(tài)s中的所有變量，包括假設(shè)變量和非假設(shè)變量。那么，

3 支持片面性的假設(shè)行為時(shí)序邏輯

將對(duì)描述語(yǔ)言TLHA+[1]和驗(yàn)證工具TLHC[1]進(jìn)行改進(jìn)，修改TLHA行為的語(yǔ)義，使之支持全局片面性，以便在多個(gè)觀察者的情況下（或者說(shuō)多方參與的情況下）更好地生成攻擊場(chǎng)景。

3.1 TLHA+的改進(jìn)

下面將對(duì)TLHA的規(guī)約語(yǔ)言TLHA+進(jìn)行改進(jìn)，使之能夠支持片面性和調(diào)查者觀察的描述。當(dāng)然這里只著重介紹增加和修改的部分。

構(gòu)造語(yǔ)句：增加兩個(gè)構(gòu)造語(yǔ)句， OBSERVATIONS obs1，…，obsn和NOVAL noval1， …， novaln。他們分別用來(lái)聲明觀察函數(shù)和虛構(gòu)的假設(shè)值。

觀察到的狀態(tài)描述：每個(gè)觀察obsx（s）（s是一個(gè)狀態(tài)）都是由一些表達(dá)式ei的析取構(gòu)成。這里的每個(gè)ei都是一個(gè)非假設(shè)變量vi在觀察函數(shù)obsx下的一個(gè)觀察結(jié)果，它具有以下三種形式之一。

ls（v） = s（v），當(dāng)變量v在觀察函數(shù)obsx下可見(jiàn)且可以解釋。其標(biāo)簽等依賴于被觀察的狀態(tài)，且等于在此狀態(tài)的實(shí)際值；

l（v） = novalx，當(dāng)變量v在觀察函數(shù)obsx下可見(jiàn)但不可解釋。其標(biāo)簽在整個(gè)運(yùn)轉(zhuǎn)過(guò)程中都等于一個(gè)虛構(gòu)的值。

l（v） =，當(dāng)變量v在觀察函數(shù)obsx下不可見(jiàn)。其值被設(shè)置為空值。

片面性描述：以下語(yǔ)句以謂詞的形式描述各類片面性：AllObsOneSid_Init（P）、AllObsOneSid_fin（P）、AllObsOneSid_allways（P）、AllObsOneSid_total（P）和AllObsOneSid_semi（P）分別表示初始全局片面性、最終全局片面性、總是全局片面性、完全全局片面性和半全局片面性。

3.2 自動(dòng)驗(yàn)證工具TLHC的改進(jìn)

給定一個(gè)可達(dá)的系統(tǒng)狀態(tài)t，用（G， ？奐t）表示圖G從系統(tǒng)初始狀態(tài)直到狀態(tài)t的部分。另外，用（G， g， ？奐t）表示圖G的一條路徑g（即系統(tǒng)的一個(gè)運(yùn)轉(zhuǎn)）從初始狀態(tài)到狀態(tài)t這一段。給定個(gè)可達(dá)狀態(tài)s，改進(jìn)的TLHC算法會(huì)生成滿足如下條件的下一狀態(tài)集T=∪{ti}：1）所有攻擊場(chǎng)景片段的析取A，在狀態(tài)對(duì)（s，t）的值為true；2）t滿足約束謂詞Constraint；3）第i個(gè)調(diào)查者使用它的觀察函數(shù)obsi觀察（G， ？奐t）所得到的結(jié)果，用（G， ？奐ti）表示，作為他所收集到的證據(jù)OBSi；4）表示行為證據(jù)謂詞集C對(duì)每一個(gè)（G， ？奐ti）都為真；以及5）如果謂詞證據(jù)Pr的值為假，那么，從初始狀態(tài)到狀態(tài)ti，它的值也必須都為假。

在后向推理階段也未使用同樣的方法，這里不再贅述。

在生成表示可能攻擊場(chǎng)景集的圖G后，算法會(huì)驗(yàn)證額外的謂詞證據(jù)的片面性，比如半全局片面性可通過(guò)檢查下面的公式是否為真來(lái)進(jìn)行驗(yàn)證：

4 案例分析

考慮一個(gè)針對(duì)Web服務(wù)器的拒絕服務(wù)攻擊。用4個(gè)變量來(lái)為其建模，分別是表示用戶權(quán)限的變量pr、運(yùn)行在80端口的服務(wù)srv80、HTTP服務(wù)器日志文件weblog、運(yùn)行在81端口的服務(wù)srv81。假設(shè)對(duì)系統(tǒng)的多方觀察獲得幾個(gè)結(jié)果。

（1）第一個(gè)調(diào)查者通過(guò)服務(wù)監(jiān)聽(tīng)程序搜集到一個(gè)證據(jù)，并可根據(jù)它對(duì)變量srv80進(jìn)行監(jiān)測(cè)和解釋。第一個(gè)調(diào)查者的觀察的形式定義如下：

obs1（ ） ∧l（Pr） = ∧ l（srv80） = srv80

∧l（weblog） = ∧ l（srv81） =

并且其收集到的歷史證據(jù)為OBS1=（"http"， "noservice"）。

（2）第二個(gè)調(diào)查者已經(jīng)進(jìn)行了服務(wù)器的文件系統(tǒng)調(diào)查并發(fā)現(xiàn)了一個(gè)針對(duì)日志文件的攻擊，入侵者將元數(shù)據(jù)中的日志文件條目指向了一個(gè)空塊。此調(diào)查者可以監(jiān)聽(tīng)并解釋變量weblog。第一個(gè)調(diào)查者的觀察的形式定義如下：

obs1（ ） ∧l（Pr） = ∧ l（srv80） =

∧ l（weblog） = weblog ∧ l（srv81） =

且它所收集到的歷史證據(jù)為OBS2=（"_"， "mfurl"， "_"），其中“_”表示內(nèi)容為空，“mfurl”表示一個(gè)誘使服務(wù)器拒絕服務(wù)的畸形URL。

（3）第三個(gè)調(diào)查者檢查了一個(gè)網(wǎng)絡(luò)入侵檢測(cè)系統(tǒng)（IDS），并從其日志文件中發(fā)現(xiàn)了一個(gè)作為緩沖區(qū)溢出攻擊的行為證據(jù)，這一證據(jù)在形式上可轉(zhuǎn)化為“同時(shí)”約束。實(shí)際上，緩沖區(qū)溢出漏洞在拒絕相關(guān)應(yīng)用時(shí)可提供一個(gè)授權(quán)外殼程序。此行為證據(jù)可形式地描述為：

c1（w=（s0， …， sn））？堝i∈[0..n-1]： （si（weblog）≠ “mfurl”∧ si+1（weblog）= “mfurl”）

？圯si（srv80）= “http”∧ si+1（srv80）=“noservice”）

最后，當(dāng)安全管理員發(fā)現(xiàn)Web服務(wù)器已經(jīng)停止了HTTP服務(wù)，并意識(shí)到受到攻擊時(shí)，可為調(diào)查者提供一個(gè)謂詞證據(jù)。其形式定義為：

Pr1 srv80= “noservice”

系統(tǒng)的初始狀態(tài)為：沒(méi)有向用戶提供授權(quán)、一個(gè)HTTP服務(wù)正運(yùn)行在80端口、日志文件為空、且81端口沒(méi)有運(yùn)行任何服務(wù)。其形式定義如下：

Init ∧Pr = 0 ∧srv80 = “http”

weblog = “_”∧srv81 = “noservice”

現(xiàn)在，若一個(gè)調(diào)查者想要形式地證明入侵者在81端口安裝了后門外殼程序。把這一想證明的結(jié)果描述為一個(gè)謂詞證據(jù)Pr2 srv81 = “/bin/sh”，此問(wèn)題就轉(zhuǎn)化為證明Pr2是否是半全局片面性。

在運(yùn)行改進(jìn)后的TLHC算法后，獲得如圖1所示的兩個(gè)攻擊場(chǎng)景：一用戶使用較低的權(quán)限向HTTP服務(wù)器提交一個(gè)探查Web服務(wù)版本請(qǐng)求“get/？”，隨后通過(guò)向服務(wù)器發(fā)送特定的溢出數(shù)據(jù)，利用該版本的緩沖區(qū)溢出漏洞，在服務(wù)被終止的同時(shí)入侵服務(wù)器并獲取最高用戶權(quán)限，然后攻擊文件系統(tǒng)，隱藏HTTP服務(wù)日志的真實(shí)內(nèi)容，使它的元數(shù)據(jù)條目指向一個(gè)空的數(shù)據(jù)塊。這樣，入侵者就可以在81端口安裝后門程序或立即退出服務(wù)器。

容易看出，這些攻擊與歷史證據(jù)、行為證據(jù)和謂詞證據(jù)Pr1相符合。至于Pr2，它屬于半全局片面性，即在第一個(gè)攻擊場(chǎng)景，它的值開(kāi)始為假，而后來(lái)變?yōu)檎?；而在第二個(gè)攻擊場(chǎng)景，它的值在所有狀態(tài)都為假。

5 結(jié)束語(yǔ)

本文提出了一種基于片面性理論的適于多方協(xié)作的入侵取證調(diào)查方法，這種方法利用提出的片面性理論建立取證性質(zhì)并證明已完成的攻擊場(chǎng)景。把這一理論整合進(jìn)了前文提出的假設(shè)行為時(shí)序邏輯TLHA及其自動(dòng)驗(yàn)證工具TLHC。另外，為了處理多方觀察，還提出了“全局片面性”和比較特殊的“半全局片面性”，用來(lái)驗(yàn)證不可證明的證據(jù)。最后用實(shí)例證明了這一理論的有效性。

參考文獻(xiàn)

[1] 李均濤，唐鄭熠，李祥.基于行為時(shí)序邏輯的入侵取證研究[J].計(jì)算機(jī)應(yīng)用研究，2011，28（7）： 2742-2745.

[2] JeremyW. Bryans， Maciej Koutny， and Peter Y.A. Ryan. Modelling Opacity Using Petri Nets. Electronic Notes in Theoretical Computer Science， 121：101-115， 2005.

[3] Steve Schneider and Abraham Sidiropoulos. Csp and anonymity. In ESORICS 96： Proceedings of the 4th European Symposium on Research in Computer Security， pages 198-218， London， UK， 1996. Springer-Verlag.

[4] Dominic Hughes and Vitaly Shmatikov. Information Hiding， Anonymity and Privacy： a Modular Approach. Journal of Computer Security， 12（1）：3-36， 2004.

[5] Peter Y.A. Ryan Jeremy W. Bryans， Maciej Koutny. Modelling Dynamic Opacity using Petri Nets with Silent Actions. In Proceedings of the Workshop on Formal Aspects in Security and Trust （FAST）， Toulouse， France， August 2004. Kluwer Academic Press.

作者簡(jiǎn)介：

李均濤（1969-），男，漢族，山東微山人，博士，畢業(yè)于貴州大學(xué)計(jì)算機(jī)信息工程學(xué)院，副教授；主要研究方向和關(guān)注領(lǐng)域：密碼學(xué)與信息安全、形式化理論、模型檢測(cè)。

唐鄭熠（1984-），男，漢族，福建福州人，博士，畢業(yè)于貴州大學(xué)計(jì)算機(jī)信息工程學(xué)院，副教授；主要研究方向和關(guān)注領(lǐng)域：形式化方法與服務(wù)計(jì)算。

張金磊（1991-），男，漢族，內(nèi)蒙古赤峰人，貴州財(cái)經(jīng)大學(xué)，碩士研究生；主要研究方向和關(guān)注領(lǐng)域：決策分析與決策支持。