基于行為時序邏輯的多方協(xié)作取證研究

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

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

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

【 中圖分類號 】 TP309.2

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

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

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

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

2.1 不透明性簡介

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

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

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

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

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

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

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

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

將對描述語言TLHA+[1]和驗證工具TLHC[1]進行改進，修改TLHA行為的語義，使之支持全局片面性，以便在多個觀察者的情況下（或者說多方參與的情況下）更好地生成攻擊場景。

3.1 TLHA+的改進

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

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

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

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

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

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

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

3.2 自動驗證工具TLHC的改進

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

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

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

4 案例分析

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

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

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

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

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

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

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

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

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

（3）第三個調(diào)查者檢查了一個網(wǎng)絡(luò)入侵檢測系統(tǒng)（IDS），并從其日志文件中發(fā)現(xiàn)了一個作為緩沖區(qū)溢出攻擊的行為證據(jù)，這一證據(jù)在形式上可轉(zhuǎn)化為“同時”約束。實際上，緩沖區(qū)溢出漏洞在拒絕相關(guān)應(yīng)用時可提供一個授權(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ù)，并意識到受到攻擊時，可為調(diào)查者提供一個謂詞證據(jù)。其形式定義為：

Pr1 srv80= “noservice”

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

Init ∧Pr = 0 ∧srv80 = “http”

weblog = “_”∧srv81 = “noservice”

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

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

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

5 結(jié)束語

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

參考文獻(xiàn)

[1] 李均濤，唐鄭熠，李祥.基于行為時序邏輯的入侵取證研究[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.

作者簡介：

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

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

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