基于模型檢查的場(chǎng)景圖和攻擊圖研究.pdf

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

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

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