摘 要：計(jì)算機(jī)脆弱性分析是指找出計(jì)算機(jī)系統(tǒng)的漏洞，以防危機(jī)計(jì)算機(jī)系統(tǒng)的安全?；谀Ｐ蜋z驗(yàn)的分析方法不僅可以發(fā)現(xiàn)系統(tǒng)已知的漏洞，也可以發(fā)現(xiàn)系統(tǒng)未知的新的漏洞。在本篇文章中，我們利用模型驗(yàn)證器SPIN對網(wǎng)絡(luò)系統(tǒng)脆弱性做了抽象的描述。建立了一個(gè)簡單的網(wǎng)絡(luò)脆弱性分析模型。

關(guān)鍵字：計(jì)算機(jī)脆弱性；滲透；模型檢驗(yàn)；SPIN

0 引言

網(wǎng)絡(luò)系統(tǒng)及其應(yīng)用擴(kuò)展范圍廣闊，隨著網(wǎng)絡(luò)規(guī)模的擴(kuò)大及應(yīng)用的增加，網(wǎng)絡(luò)脆弱性（也叫做安全漏洞）也會不斷增加。在攻擊者對計(jì)算機(jī)系統(tǒng)進(jìn)行攻擊之前，應(yīng)明確要采取的技術(shù)，這種技術(shù)我們可以稱之為滲透。

計(jì)算機(jī)脆弱性的定義[1]：計(jì)算機(jī)系統(tǒng)是由一系列描述構(gòu)成計(jì)算機(jī)系統(tǒng)的實(shí)體的當(dāng)前配置的狀態(tài)（state）組成，系統(tǒng)通過應(yīng)用狀態(tài)變換（state transitions）實(shí)現(xiàn)計(jì)算。從給定的初始狀態(tài)使用一組狀態(tài)變換可以到達(dá)的所有狀態(tài)從安全策略定義的角度講分為已授權(quán)的和未授權(quán)的兩種類型。脆弱狀態(tài)是指能夠使用已授權(quán)的狀態(tài)轉(zhuǎn)換到未授權(quán)狀態(tài)的已授權(quán)狀態(tài)，受損狀態(tài)是指通過上述方法到達(dá)的狀態(tài)。攻擊是指以受損狀態(tài)結(jié)束的已授權(quán)狀態(tài)變換順序，即攻擊開始于脆弱狀態(tài)。

脆弱性評估主要有兩種方法：一個(gè)是用于檢驗(yàn)系統(tǒng)是否存在已有的滲透轉(zhuǎn)換的規(guī)則匹配法，還有一個(gè)是基于模型分析的方法，主要用于發(fā)現(xiàn)新的轉(zhuǎn)換或者轉(zhuǎn)換序列。

1 模型檢驗(yàn)

模型檢驗(yàn)是一種基于有限模型并檢驗(yàn)改模型的期望特性的一種技術(shù)。它通過將所要驗(yàn)證的系統(tǒng)行為描述為有限狀態(tài)自動機(jī)，然后建立對行為的時(shí)態(tài)邏輯限制。通過遍歷自動機(jī)上的所有可達(dá)狀態(tài)，找出不滿足邏輯表達(dá)式的路徑，同時(shí)提供違背公式的路徑。

模型檢驗(yàn)已在硬件電路、協(xié)議的驗(yàn)證、軟件系統(tǒng)規(guī)格與分析中得到成功的應(yīng)用。常見的模型檢驗(yàn)工具有SMV，Merφ，SPIN，F(xiàn)DR， PVS， VIS， HSIS等。

2 基于模型檢驗(yàn)的網(wǎng)絡(luò)脆弱性分析

2.1 模型檢驗(yàn)的優(yōu)點(diǎn)

COPS（Computer Oracle and Password System ）， Cyber Cop by Network Associates， System Scanner by ISS，SATAN 都是不錯(cuò)的檢查主機(jī)脆弱性的分析工具，但是它們都是基于規(guī)則的，所以適用于發(fā)現(xiàn)已知的滲透轉(zhuǎn)移。而模型檢驗(yàn)的方法可以發(fā)現(xiàn)新的未曾找到的滲透。此外，模型檢驗(yàn)有著很好的模塊性。新的模塊可以很容易的加入模型中，而不用改變舊的模塊。不像基于規(guī)則的方法，一旦有新的規(guī)則加入，不但要建立新舊規(guī)則的接口，而且還要對舊的規(guī)則做相應(yīng)的修改。并且，模型檢驗(yàn)的方法可以對檢查到的違背邏輯公式的行為提供反例。即，提供攻擊的路徑。這樣便于我們進(jìn)一步完善系統(tǒng)的安全性。

2.2 SPIN

SPIN（Simple Promela Interpreter）是一個(gè)由美國貝爾實(shí)驗(yàn)室開發(fā)的用于分布式系統(tǒng)形式化驗(yàn)證的軟件。

在SPIN中，采用了on-the-fly 的機(jī)制來構(gòu)建自動機(jī)模型。主要步驟是：（1）首先將由LTL公式描述的系統(tǒng)性質(zhì)取反，建立Büchi自動機(jī)A（2）通過計(jì)算系統(tǒng)中的每個(gè)進(jìn)程的轉(zhuǎn)移子系統(tǒng)的乘積，得到系統(tǒng)的全局行為，從而建立Büchi自動機(jī)P (3)計(jì)算自動機(jī)A與P的乘積（4）檢查最后得到的自動機(jī)所能接受的語言是否為空，如果為空，則系統(tǒng)滿足描述的屬性要求，否則系統(tǒng)的行為不滿足我們定義的屬性要求。我們可以通過檢查是否存在一個(gè)從初始狀態(tài)可達(dá)的環(huán)路包含一個(gè)至少一個(gè)接受狀態(tài)來檢查積自動機(jī)是否為空。

3 用SPIN 分析網(wǎng)絡(luò)脆弱性

安全模型是實(shí)際問題的抽象，只是涉及到整體的屬性而不關(guān)注細(xì)節(jié)的實(shí)現(xiàn)。我們可以依據(jù)主體對可以訪問的時(shí)序關(guān)系，主體訪問的可達(dá)性等來形式化驗(yàn)證安全模型?；谀Ｐ偷拇嗳跣栽u估就可以看作是尋找特定狀態(tài)的可達(dá)關(guān)系。比如：我們可以根據(jù)規(guī)則建立原子攻擊（atomic attack），模型中的每個(gè)狀態(tài)對應(yīng)系統(tǒng)中的一個(gè)狀態(tài)，狀態(tài)之間的轉(zhuǎn)移對應(yīng)一個(gè)相應(yīng)的原子攻擊。轉(zhuǎn)移S1→S2是攻擊的前提條件在狀態(tài)S1滿足，攻擊的后續(xù)條件在S2成立的轉(zhuǎn)移。一個(gè)攻擊是一個(gè)狀態(tài)轉(zhuǎn)移序列，一直到攻擊者達(dá)到自己的攻擊目標(biāo)為止。

3.1 模型初始化

模型主要包括四部分：主機(jī)描述、主機(jī)連接性、攻擊者的起始點(diǎn)、滲透方法。

主機(jī)描述包括主機(jī)存在的漏洞（如 操作系統(tǒng)的類型及版本，密碼的最大長度，提供的網(wǎng)絡(luò)服務(wù)類型）和當(dāng)前的訪問權(quán)限。主機(jī)的連接性由一個(gè)連接矩陣表示，它包含了主機(jī)間的連接關(guān)系，這個(gè)關(guān)系在我們分析中不會更改。攻擊者的起始點(diǎn)描述了攻擊者所在的主機(jī)。滲透方法包括源主機(jī)訪問權(quán)限、目的主機(jī)訪問權(quán)限和滲透結(jié)果。

用Promela 語言定義相應(yīng)的數(shù)據(jù)結(jié)構(gòu)：

mtype = { none， user， root }; /*定義了訪問權(quán)限變量，其中none 代表攻擊者不執(zhí)行主機(jī)上的程序，root 可以執(zhí)行主機(jī)上的所有程序*/

bool exploit[4];

bool vulnerability[10];

在Promela中，變量在定義之初就默認(rèn)賦值為零。

3.2 分析模型

在用SPIN分析模型之前，我們首先初步分析模型。首先，我們對模型整體關(guān)注的是攻擊者的訪問途徑以及主機(jī)所提供的脆弱性環(huán)境。其次，模型的改變將導(dǎo)致新的滲透的加入以及會使攻擊者對主機(jī)的訪問權(quán)限得到更新。模型的停止條件是要么系統(tǒng)再沒有新的滲透發(fā)生，要么是模型不再違背定義好的邏輯限制。

對滲透者的描述

對滲透者的描述是模型描述的重點(diǎn)，因?yàn)檫@些直接影響到分析的結(jié)果。對滲透者的描述包括：攻擊點(diǎn)的集合，源主機(jī)的訪問權(quán)限和目的主機(jī)的訪問權(quán)限，與主機(jī)的連接，滲透的結(jié)果（體現(xiàn)模型的動態(tài)性）。然后，我們需要將所有的描述轉(zhuǎn)化為邏輯公式的描述。例如：當(dāng)（（Statement=1）(Connectness-host=1)）滿足，則滲透成功。主機(jī)應(yīng)該根據(jù)滲透改變相應(yīng)的變量（向主機(jī)中加入新的滲透點(diǎn)、改變攻擊者對當(dāng)前主機(jī)的訪問權(quán)限等）。

LTL 公式斷言： [ ]! host.access =root 即 ，任何攻擊者都不能在給定的主機(jī)上提出請求

結(jié)語：

基于模型檢驗(yàn)的辦法可以發(fā)現(xiàn)新的很微小的脆弱性，并且我們可以通過修改模型的參數(shù)從而實(shí)現(xiàn)用一個(gè)模型去測試不同場景的攻擊。這樣一旦系統(tǒng)的模型建立完成，剩下的問題只是對攻擊者賦予不同層次的訪問權(quán)限，找到攻擊的路徑。雖然模型檢驗(yàn)仍面臨著狀態(tài)空間爆炸問題的制約使受系統(tǒng)的大小受到限制，但是我們可以在檢驗(yàn)的過程中使用抽象、基于限制條件的描述等手段來緩解這個(gè)問題。

參考文獻(xiàn)

[1]計(jì)算機(jī)系統(tǒng)脆弱性評估研究 邢栩嘉，林闖等 計(jì)算機(jī)學(xué)報(bào). Vol.27 No.1 1-11.

[2]Ritchey R.W. ，Ammann P.. Using model checking to analyze network vulnerabilities.In: Proceedings of 2000 IEEE Symposium on Security and Privacy，Oakland，CA，2000，156-165.

[3]Ramakrishnan C.R.，Sekar R.. Model-based analysis of configuration vulnerabilities. In: Proceedings of ACM CCIDS Workshop on Intrusion Detection and Prevention (WIDS)，Athens，Greece，2000.

[4] Internet Security Systems， System Scanner information on the web at http://www.iss.net.

[5] Network Associates， Cyber Cop Scanner information on the web at http://www.nai.com/asp_set/products/tns/ccscanner_intro.asp>.

[6]E. Clarke， O. Grumberg ， and D.Peled. Model Checking. MIT Press，2000.

[7]Gerard J.Holzmann.The Model Checker Spin.IEEE.TRANSACTIONS ONSOFTWARE ENGINEERING.VOL.23.NO.5 1-17.

[8]韓俊剛等.數(shù)字硬件的形式化驗(yàn)證.北京大學(xué)出版社2001年第1版.