基于ＳＰＩＮ的網絡脆弱性分析

摘 要：計算機脆弱性分析是指找出計算機系統的漏洞，以防危機計算機系統的安全。基于模型檢驗的分析方法不僅可以發現系統已知的漏洞，也可以發現系統未知的新的漏洞。在本篇文章中，我們利用模型驗證器SPIN對網絡系統脆弱性做了抽象的描述。建立了一個簡單的網絡脆弱性分析模型。

關鍵字：計算機脆弱性；滲透；模型檢驗；SPIN

0 引言

網絡系統及其應用擴展范圍廣闊，隨著網絡規模的擴大及應用的增加，網絡脆弱性（也叫做安全漏洞）也會不斷增加。在攻擊者對計算機系統進行攻擊之前，應明確要采取的技術，這種技術我們可以稱之為滲透。

計算機脆弱性的定義[1]：計算機系統是由一系列描述構成計算機系統的實體的當前配置的狀態（state）組成，系統通過應用狀態變換（state transitions）實現計算。從給定的初始狀態使用一組狀態變換可以到達的所有狀態從安全策略定義的角度講分為已授權的和未授權的兩種類型。脆弱狀態是指能夠使用已授權的狀態轉換到未授權狀態的已授權狀態，受損狀態是指通過上述方法到達的狀態。攻擊是指以受損狀態結束的已授權狀態變換順序，即攻擊開始于脆弱狀態。

脆弱性評估主要有兩種方法：一個是用于檢驗系統是否存在已有的滲透轉換的規則匹配法，還有一個是基于模型分析的方法，主要用于發現新的轉換或者轉換序列。

1 模型檢驗

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

模型檢驗已在硬件電路、協議的驗證、軟件系統規格與分析中得到成功的應用。常見的模型檢驗工具有SMV，Merφ，SPIN，FDR， PVS， VIS， HSIS等。

2 基于模型檢驗的網絡脆弱性分析

2.1 模型檢驗的優點

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

2.2 SPIN

SPIN（Simple Promela Interpreter）是一個由美國貝爾實驗室開發的用于分布式系統形式化驗證的軟件。

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

3 用SPIN 分析網絡脆弱性

安全模型是實際問題的抽象，只是涉及到整體的屬性而不關注細節的實現。我們可以依據主體對可以訪問的時序關系，主體訪問的可達性等來形式化驗證安全模型。基于模型的脆弱性評估就可以看作是尋找特定狀態的可達關系。比如：我們可以根據規則建立原子攻擊（atomic attack），模型中的每個狀態對應系統中的一個狀態，狀態之間的轉移對應一個相應的原子攻擊。轉移S1→S2是攻擊的前提條件在狀態S1滿足，攻擊的后續條件在S2成立的轉移。一個攻擊是一個狀態轉移序列，一直到攻擊者達到自己的攻擊目標為止。

3.1 模型初始化

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

主機描述包括主機存在的漏洞（如 操作系統的類型及版本，密碼的最大長度，提供的網絡服務類型）和當前的訪問權限。主機的連接性由一個連接矩陣表示，它包含了主機間的連接關系，這個關系在我們分析中不會更改。攻擊者的起始點描述了攻擊者所在的主機。滲透方法包括源主機訪問權限、目的主機訪問權限和滲透結果。

用Promela 語言定義相應的數據結構：

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

bool exploit[4];

bool vulnerability[10];

在Promela中，變量在定義之初就默認賦值為零。

3.2 分析模型

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

對滲透者的描述

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

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

結語：

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

參考文獻

[1]計算機系統脆弱性評估研究 邢栩嘉，林闖等 計算機學報. 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]韓俊剛等.數字硬件的形式化驗證.北京大學出版社2001年第1版.