基于模型檢查的場景圖和攻擊圖研究.pdf

1、攻擊圖是一種簡潔的表現(xiàn)形式，它表現(xiàn)了一個系統(tǒng)中所有結(jié)束于一個不安全狀態(tài)的路徑，一個入侵者可以通過這些路徑實現(xiàn)他的目標(biāo)。系統(tǒng)管理員可以使用攻擊圖來確定他們的系統(tǒng)的脆弱程度，以及決定使用什么安全措施來加固系統(tǒng)。目前安全專家通過手動繪制攻擊圖來確定聯(lián)網(wǎng)系統(tǒng)的脆弱點，但是手繪攻擊圖非常繁瑣，且容易出錯，對于大型系統(tǒng)來說也不現(xiàn)實，因此如何自動地生成攻擊圖并對其進行自動分析就很有必要。如果把攻擊看成是對一個安全性屬性的違反，可以使用模型檢查來自動生

2、成攻擊圖，對于攻擊者來說一條成功的路徑就是模型檢查器產(chǎn)生一個反例。但傳統(tǒng)的模型檢查器只能為用戶從錯誤行為集合中提供一個反例，這就影響了模型檢查的效率，如何讓用戶可以得到全部的反例，也是需要研究的問題。 在本文中，介紹了如何通過規(guī)范的技術(shù)讓用戶可以自由地檢查由自動分析發(fā)現(xiàn)的設(shè)計缺陷。使用了模型檢查的方法來給出結(jié)果，并對傳統(tǒng)的模型檢查理論進行了改進，提出了新的模型檢查體系，即將所有的錯誤行為集定義成失敗場景圖。探討了兩種可以自動生成

3、失敗場景圖的算法及其性能，即符號模型檢查算法和明確狀態(tài)模型檢查算法。將該體系和算法應(yīng)用在了網(wǎng)絡(luò)安全領(lǐng)域，對網(wǎng)絡(luò)攻擊進行了建模，并定義了一種場景圖的實例：攻擊圖，用于表現(xiàn)入侵者攻擊計算機網(wǎng)絡(luò)的過程。集中研究了攻擊圖的自動生成、表現(xiàn)和分析的方法，以解決現(xiàn)實世界中與網(wǎng)絡(luò)安全有關(guān)的問題。 本文主要的組織結(jié)構(gòu)如下：首先定義了失敗場景圖，接著描述了根據(jù)有限模型生成場景圖的兩種算法并評測了它們的性能。隨后將這些規(guī)范的概念應(yīng)用在了安全領(lǐng)域，用場