基于狀態(tài)機(jī)模型的網(wǎng)絡(luò)安全策略驗(yàn)證方法研究

程曉榮，馮志偉

（華北電力大學(xué) 控制與計(jì)算機(jī)工程學(xué)院，河北 保定071003）

0 引 言

隨著信息系統(tǒng)面臨的安全威脅越來越嚴(yán)峻，需要制定安全策略實(shí)現(xiàn)安全設(shè)備的統(tǒng)一管理和有效聯(lián)動(dòng)，安全策略的表達(dá)和驗(yàn)證方法成為基于策略的安全管理研究重點(diǎn)。文獻(xiàn)[1，2]討論了安全策略的語法、語義和決策算法，但未考慮策略的驗(yàn)證；在此基礎(chǔ)上，文獻(xiàn)[3]基于一階邏輯提出了基于良基語義的安全策略驗(yàn)證方式，在訪問控制應(yīng)用中具有可靠的策略驗(yàn)證能力；文獻(xiàn)[4]提出用有向無環(huán)圖描述主 （客）體之間的關(guān)系，提出了一種基于有向圖的策略沖突檢測方法，檢測的復(fù)雜度是主 （客）體間關(guān)系的冪函數(shù)，當(dāng)系統(tǒng)中主 （客）體間的關(guān)系較為復(fù)雜時(shí)，該方法的耗時(shí)量較大；文獻(xiàn)[5]將安全策略描述為安全事件、規(guī)則、動(dòng)作三元組，驗(yàn)證安全策略的完備性、一致性和冗余性，由于未進(jìn)行安全域的劃分，隨著策略集的增加和系統(tǒng)復(fù)雜度的提升，策略驗(yàn)證方法復(fù)雜度較高；文獻(xiàn)[6]用安全域、觸發(fā)條件、執(zhí)行動(dòng)作和指導(dǎo)原則描述安全策略，設(shè)計(jì)了策略的正確性評(píng)估函數(shù)，并通過特征矩陣驗(yàn)證策略一致性，一致性檢測算法的復(fù)雜度為O（4n2）；文獻(xiàn)[7，8]分別運(yùn)用高級(jí)Petri網(wǎng)對(duì)策略規(guī)則進(jìn)行描述并對(duì)策略庫中的循環(huán)、冗余、矛盾等異常規(guī)則進(jìn)行驗(yàn)證。本文采用狀態(tài)機(jī)模型驗(yàn)證策略庫中的異常規(guī)則，在Petri網(wǎng)的基礎(chǔ)上分離了系統(tǒng)狀態(tài)、觸發(fā)條件和執(zhí)行動(dòng)作，用無環(huán)狀態(tài)有向圖描述系統(tǒng)的狀態(tài)變遷。并通過以子網(wǎng)劃分安全域的方式降低了有向圖的規(guī)模，使算法具有理想的執(zhí)行效率。

1 相關(guān)概念

在網(wǎng)絡(luò)信息安全系統(tǒng)中，安全域構(gòu)成環(huán)境的子集，是由一系列實(shí)體與資源構(gòu)成的[6]。安全域的劃分有多種方式，文獻(xiàn)[8]根據(jù)設(shè)備類型與業(yè)務(wù)將安全域劃分為安全業(yè)務(wù)域、安全用戶域、網(wǎng)絡(luò)設(shè)備域和安全網(wǎng)絡(luò)域。上述劃分方式雖然分離了不同安全域的職責(zé)，但當(dāng)網(wǎng)絡(luò)結(jié)構(gòu)較為復(fù)雜時(shí)，每個(gè)安全域的規(guī)模會(huì)非常龐大，不利于安全域中實(shí)體或資源的查詢。本文將安全域按照子網(wǎng)的方式劃分，因?yàn)樽泳W(wǎng)中同時(shí)包含了防火墻、IPS等安全設(shè)備和這些安全設(shè)備控制范圍內(nèi)的實(shí)體資源，安全事件的捕獲和策略的分發(fā)都可以在子網(wǎng)內(nèi)部完成。同時(shí)按照子網(wǎng)劃分安全域可以降低安全域的規(guī)模。

本文用狀態(tài)機(jī)模型描述安全域中實(shí)體與資源的狀態(tài)，安全策略的執(zhí)行實(shí)質(zhì)上直接反映為安全域中實(shí)體與資源狀態(tài)的變遷。比如在觸發(fā)條件TCP掃描事件的作用下，IPS的防TCP掃描模塊會(huì)變遷為開啟狀態(tài)，在殺毒程序執(zhí)行完成后掃描器會(huì)進(jìn)入到漏洞掃描狀態(tài)。通過分析安全域中設(shè)備的日志，可以及時(shí)捕獲安全域中發(fā)生的一系列安全事件。安全策略就是通過執(zhí)行相應(yīng)設(shè)備的配置動(dòng)作，實(shí)現(xiàn)系統(tǒng)狀態(tài)的切換，最終達(dá)到解決安全事件的效果。

下面介紹相關(guān)的定義:

定義1 狀態(tài)機(jī)，全稱為有限狀態(tài)機(jī) （finite－state machine，F(xiàn)SM），是表示有限個(gè)狀態(tài)以及在這些狀態(tài)之間的轉(zhuǎn)移和動(dòng)作等行為的數(shù)學(xué)模型。本文采用Mealy型狀態(tài)機(jī)，它的下一個(gè)狀態(tài)即輸出是由輸入和當(dāng)前狀態(tài)決定的[9]。本文闡述的狀態(tài)機(jī)考慮單向的狀態(tài)流動(dòng)，即從開始狀態(tài)到終止?fàn)顟B(tài)的變遷過程可由無環(huán)有向圖來描述。狀態(tài)機(jī)由五元組 （∑，S，s0，δ，F(xiàn)）構(gòu)成，它們的含義分別為:

∑表示輸入的非空有限集合，對(duì)應(yīng)系統(tǒng)的觸發(fā)條件集；

S表示狀態(tài)的非空有限集合，對(duì)應(yīng)系統(tǒng)的當(dāng)前狀態(tài)集和輸出狀態(tài)集；

s0表示初始狀態(tài)，其中s0∈S；

δ表示狀態(tài)轉(zhuǎn)移函數(shù)，即δ:S×∑→S，即系統(tǒng)當(dāng)前狀態(tài)集在觸發(fā)條件的作用下變遷為輸出狀態(tài)集；

F表示最終狀態(tài)的集合，到達(dá)最終狀態(tài)后不會(huì)再向其它狀態(tài)轉(zhuǎn)移，其中FS。

定義2 安全域D。安全域可以看作是系統(tǒng)中實(shí)體和安全策略的組合。安全域?qū)⒁?guī)模龐大的網(wǎng)絡(luò)信息系統(tǒng)劃分為較小的研究單元，對(duì)每個(gè)研究單元分別制定安全策略，通過將不同安全域中的安全策略相關(guān)聯(lián)，可以得到系統(tǒng)整體的安全策略。本文根據(jù)子網(wǎng)劃分安全策略，使子網(wǎng)間的安全策略執(zhí)行能夠相互獨(dú)立。網(wǎng)絡(luò)信息系統(tǒng)的安全策略知識(shí)庫是其包含的所有安全域的安全策略并集。

定義3 安全策略P。從廣義上講，安全策略是指實(shí)體為保證網(wǎng)絡(luò)的安全性，在面臨安全事件時(shí)對(duì)安全設(shè)備如何進(jìn)行控制的規(guī)則集合。本文將安全策略具體描述為P＝＜D，C，R＞。其中D表示安全域，C表示觸發(fā)條件，R表示策略包含的規(guī)則集，規(guī)則集中的每一條規(guī)則r對(duì)應(yīng)一個(gè)配置動(dòng)作，基于狀態(tài)機(jī)模型，將規(guī)則r定義為r＝＜i，o，s0，l＞，其中i表示規(guī)則的原狀態(tài)，o表示輸出狀態(tài)，則狀態(tài)機(jī)中的狀態(tài)轉(zhuǎn)移可以描述為i（C）→o，其中i，o∈S，C∈∑。例如當(dāng) “IPS開啟”時(shí) （記作IS），發(fā)生 “DoS攻擊”事件 （記作事件da），則系統(tǒng)執(zhí)行規(guī)則進(jìn)入 “IPS的防DoS攻擊模塊開啟狀態(tài)”（記作DO），則此策略規(guī)則可以表示為IS（da）→DO。s0表示規(guī)則所在安全域的初始狀態(tài)，l表示規(guī)則的輸出狀態(tài)是否為最終狀態(tài)。因?yàn)橐?guī)則的輸出狀態(tài)包含了策略執(zhí)行動(dòng)作達(dá)到的效果，因此不再將執(zhí)行動(dòng)作顯式地表現(xiàn)在策略中。每一條安全策略包含著一條或多條規(guī)則，每一條規(guī)則對(duì)應(yīng)狀態(tài)機(jī)中唯一的狀態(tài)變遷過程，它包含的配置動(dòng)作只包含完成一次狀態(tài)改變的配置。由于安全策略實(shí)質(zhì)上是規(guī)則的集合，因此只要系統(tǒng)的當(dāng)前狀態(tài)和觸發(fā)條件滿足，多個(gè)不矛盾規(guī)則中的配置動(dòng)作可以同時(shí)執(zhí)行。安全策略的執(zhí)行原理如圖1所示。

圖1 安全策略的執(zhí)行過程

2 策略知識(shí)庫與系統(tǒng)運(yùn)行分析

本節(jié)介紹通過狀態(tài)機(jī)模型建立特定安全域的策略規(guī)則庫的方法，一個(gè)安全域的全部策略規(guī)則對(duì)應(yīng)一個(gè)完整的狀態(tài)機(jī)，可以用無環(huán)狀態(tài)有向圖展現(xiàn)狀態(tài)之間的變遷關(guān)系，如圖2所示。下面有向圖中展現(xiàn)的一個(gè)或多個(gè)狀態(tài)變遷即構(gòu)成某個(gè)特定安全域的規(guī)則庫。

通過子網(wǎng)劃分的安全域中主要包含服務(wù)器，用戶主機(jī)，網(wǎng)絡(luò)設(shè)備和各類安全設(shè)備。其中安全設(shè)備主要包括防火墻、IPS、防病毒系統(tǒng)和掃描器等。圖2中狀態(tài)機(jī)的初始狀態(tài)為“系統(tǒng)運(yùn)行”狀態(tài)，狀態(tài)變遷包括系統(tǒng)自發(fā)的狀態(tài)變遷和因策略執(zhí)行由觸發(fā)動(dòng)作引發(fā)的狀態(tài)變遷兩類，前者不包含觸發(fā)條件，輸出的狀態(tài)在系統(tǒng)運(yùn)行過程中始終存在于當(dāng)前狀態(tài)集中，在狀態(tài)圖中用橢圓形的節(jié)點(diǎn)標(biāo)識(shí)；后者代表的策略規(guī)則統(tǒng)一存儲(chǔ)在策略知識(shí)庫中，是本文主要的研究對(duì)象，在狀態(tài)圖中用矩形節(jié)點(diǎn)標(biāo)識(shí)。

圖2 策略規(guī)則的無環(huán)狀態(tài)有向圖描述

采用具有強(qiáng)大數(shù)據(jù)處理能力的大型關(guān)系數(shù)據(jù)庫作為主要存儲(chǔ)部件，為便于尋址和易于擴(kuò)展，將數(shù)據(jù)表看作可操作的最小存儲(chǔ)單位，定義為存儲(chǔ)資源[10]。策略庫主要包含兩個(gè)數(shù)據(jù)表，一個(gè)表用來存儲(chǔ)安全策略，一個(gè)表用來存儲(chǔ)供安全策略調(diào)用的規(guī)則集。為了提高策略的搜索效率和策略規(guī)則的驗(yàn)證效率，對(duì)每個(gè)安全域中的策略和策略包含的規(guī)則分別建表。根據(jù)安全策略及其包含規(guī)則的定義，設(shè)定安全策略表包含的字段為:策略ID、所屬安全域ID、觸發(fā)條件、規(guī)則集、異常、備用策略；設(shè)定規(guī)則表的字段為:規(guī)則ID、原狀態(tài)、輸出狀態(tài)、在狀態(tài)有向圖中的初始狀態(tài)、輸出狀態(tài)是否為最終狀態(tài)。由于規(guī)則集中不包含觸發(fā)條件，所以必須保證在建立安全策略時(shí)，從規(guī)則集中選取合理有效的規(guī)則。

系統(tǒng)運(yùn)行中，要明確狀態(tài)有向圖中哪些狀態(tài)是激活的，將安全域內(nèi)所有激活的狀態(tài)記做系統(tǒng)當(dāng)前狀態(tài)集。當(dāng)接收到新的觸發(fā)條件時(shí)，首先查看觸發(fā)條件對(duì)應(yīng)安全策略是否存在于知識(shí)庫中，若不存在，則不滿足策略完整性要求；若存在，查詢安全策略所包含規(guī)則的 “原狀態(tài)”，并確認(rèn)其是否屬于系統(tǒng)當(dāng)前狀態(tài)集。如果 “原狀態(tài)”存在于系統(tǒng)當(dāng)前狀態(tài)集，則符合安全策略的執(zhí)行條件，開始通過一系列配置動(dòng)作執(zhí)行安全策略；如果規(guī)則的 “原狀態(tài)”不在系統(tǒng)當(dāng)前狀態(tài)集中，則將安全策略置入緩存中等待，直到系統(tǒng)執(zhí)行完成特定數(shù)量的安全策略后再次考察緩存中等待的安全策略是否滿足執(zhí)行條件。系統(tǒng)在同一時(shí)間段內(nèi)可能會(huì)收到很多觸發(fā)條件，只要這些觸發(fā)條件對(duì)應(yīng)的安全策略都符合執(zhí)行條件，則系統(tǒng)中的多個(gè)狀態(tài)會(huì)同時(shí)發(fā)生變遷。在系統(tǒng)沒進(jìn)行到某些特定狀態(tài)之前，某些觸發(fā)條件是不可能發(fā)生的，比如系統(tǒng)未進(jìn)入 “郵件過濾”狀態(tài)，則不可能出現(xiàn)“郵件包含非法信息”觸發(fā)事件。當(dāng)狀態(tài)機(jī)的某一條路徑運(yùn)行到最終狀態(tài)時(shí)，最終狀態(tài)從當(dāng)前狀態(tài)集合中刪除，意味著一個(gè)完整工作流的結(jié)束。狀態(tài)機(jī)模型可以準(zhǔn)確地描述系統(tǒng)在各個(gè)狀態(tài)之間的切換情況。

3 策略庫知識(shí)庫驗(yàn)證

知識(shí)庫中的策略規(guī)則可能存在不合理性，需要對(duì)其進(jìn)行異常分析，策略規(guī)則的驗(yàn)證主要包括正確性分析、完整性分析、一致性分析、冗余性分析、可執(zhí)行性分析。針對(duì)特定安全域中的策略規(guī)則，通過以下幾個(gè)方面進(jìn)行規(guī)則驗(yàn)證。

（1）正確性分析:在策略規(guī)則的有向圖模型中，從某個(gè)原狀態(tài)到某個(gè)輸出狀態(tài)可能存在多條路徑，即多個(gè)不同的觸發(fā)條件可能引發(fā)相同的狀態(tài)變遷，但是必須保證這些觸發(fā)條件不能相互矛盾。

定義4 對(duì)于策略集P中的任意兩個(gè)策略Pi和Pj，滿足:

當(dāng)且僅當(dāng) （Pi·Ci，Pj·Cj）∈∝時(shí)，稱策略集P符合正確性要求，其中∝表示策略動(dòng)作的非矛盾關(guān)系集。

在實(shí)際應(yīng)用中，存在諸多的矛盾觸發(fā)條件，例如可信IP地址和不可信IP地址、登錄成功和登錄失敗、發(fā)現(xiàn)漏洞和未發(fā)現(xiàn)漏洞、系統(tǒng)無開發(fā)任務(wù)和開發(fā)任務(wù)等。舉例說明:

例1:策略P1＝＜D1，C1，＜r1＞＞，P2＝＜D2，C2，＜r2＞＞

規(guī)則r1:WB（tp，lf）→LP表示 “當(dāng)Web服務(wù)開啟時(shí)，檢測到連接的IP地址為可信IP地址且發(fā)生登錄失敗N次事件，則鎖定登錄用戶IP”；

規(guī)則r2→LP表示 “當(dāng)Web服務(wù)開啟時(shí)，檢測到連接的IP地址為不可信IP地址，則鎖定用戶IP”。

在上述兩條規(guī)則中，都是狀態(tài)WB向狀態(tài)LP變遷，但是r1中包含的觸發(fā)條件tp（可信IP地址）和r2中包含的觸發(fā)條件（不可信IP地址）相互矛盾，因此如果兩條安全策略作用的安全域存在交集，則不符合正確性要求。實(shí)際上，規(guī)則r1完全可以去掉觸發(fā)條件tp。

（2）完整性分析：完整性是指對(duì)于系統(tǒng)能夠捕獲到的所有觸發(fā)事件，策略知識(shí)庫中都有相應(yīng)的處理策略。

定義5 對(duì)于系統(tǒng)觸發(fā)事件集conditions的任意一個(gè)觸發(fā)條件c，滿足：

在復(fù)雜的網(wǎng)絡(luò)環(huán)境中，不能確保所有安全事件都有相應(yīng)的處理策略，出現(xiàn)不完整的情況是很有可能的，此時(shí)可以構(gòu)造默認(rèn)策略滿足完整性要求，比如 “向管理員發(fā)出特殊事件告警”等默認(rèn)策略。

（3）一致性分析：策略的一致性保證策略集中不能發(fā)生同時(shí)應(yīng)用在同一個(gè)對(duì)象上的兩種不同策略［11］。如果策略作用于相同的安全域且觸發(fā)條件相同，那么在此安全域策略規(guī)則的狀態(tài)有向圖中，對(duì)于同一個(gè)原狀態(tài)，同一個(gè)它的觸發(fā)條件不能引發(fā)多個(gè)不同的輸出狀態(tài)。

定義6 對(duì)于策略集P中的任意兩個(gè)策略Pi和Pj，滿足：

則稱策略集P是一致的。

定義7 對(duì)于策略集P中的任意兩個(gè)策略Pi和Pj，若滿足：

當(dāng)且僅當(dāng)ri·oi≠rj·oj時(shí)，策略集P是一致的。

策略不一致往往是因?yàn)椴呗栽谔砑印⑿薷倪^程中更新后的安全策略與系統(tǒng)內(nèi)原有的其它安全策略發(fā)生一致性沖突；還有一種原因是安全策略對(duì)于處理某類安全事件的效果沒有明確之前，往往會(huì)出現(xiàn)備選策略，策略與其備選策略之間會(huì)存在不一致性，因此在策略知識(shí)庫驗(yàn)證時(shí)要排除備選策略的干擾。下面舉例說明違背一致性的策略：

例2：策略P3＝＜D3，C3，＜r3＞＞，P4＝＜D4，C4，＜r4＞＞

規(guī)則r3：V（v）→VK表示 “當(dāng)防病毒系統(tǒng)開啟時(shí)，檢測到發(fā)現(xiàn)病毒事件，則啟動(dòng)病毒查殺程序”；

規(guī)則r4：V（v）→SC表示 “當(dāng)防病毒系統(tǒng)開啟時(shí)，檢測到發(fā)現(xiàn)病毒事件，則進(jìn)行漏洞修復(fù)操作”。

在上述兩條策略中，規(guī)則的原狀態(tài)和觸發(fā)條件均相同，如果策略作用的安全域存在交集，則根據(jù)一致性的定義，上述兩條策略不符合一致性要求。

（4）冗余性分析：策略的冗余性包含兩種情況。如果兩條策略完全一致，即作用的安全域、觸發(fā)條件與執(zhí)行規(guī)則均完全一致，稱為重復(fù)冗余；如果策略作用的安全域中策略主體或策略客體因系統(tǒng)更新或網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)發(fā)生變化而脫離安全域，此時(shí)相關(guān)的策略無法執(zhí)行，稱為失效冗余。

定義8 對(duì)于策略集P中的任意兩個(gè)策略Pi和Pj，若滿足：

當(dāng)且僅當(dāng)ri·ii＝rj·ij且ri·oi＝rj·oj時(shí)，稱策略集P存在重復(fù)冗余。

定義9 設(shè)當(dāng)前安全域中設(shè)備包含的所有狀態(tài)集合為state－Di，對(duì)于策略集P中的任意策略Pi，-ri∈Pi·Ri，若ri·iistates－Di∨ri·oistates－Di，則P為失效冗余策略。

對(duì)于重復(fù)冗余的檢測，只需逐條對(duì)比兩條策略的所有參數(shù)；對(duì)于失效冗余的檢測，需要對(duì)設(shè)備進(jìn)行定期監(jiān)控，確保策略庫所有規(guī)則包含的狀態(tài)都屬于當(dāng)前安全域中設(shè)備能夠產(chǎn)生的狀態(tài)。

（5）可執(zhí)行性分析：策略的可執(zhí)行性需要保證規(guī)則狀態(tài)有向圖中所有的狀態(tài)必須可達(dá)，同時(shí)保證所有的狀態(tài)節(jié)點(diǎn)都具有能達(dá)到最終狀態(tài)的路徑。一個(gè)安全域只對(duì)應(yīng)唯一的狀態(tài)有向圖，且狀態(tài)有向圖具有唯一的根節(jié)點(diǎn)。只需保證在有向圖的一次遍歷中能夠經(jīng)過安全域內(nèi)所有的狀態(tài)節(jié)點(diǎn)，且所有的葉子節(jié)點(diǎn)都為最終狀態(tài)節(jié)點(diǎn)，則能夠保證策略規(guī)則的可達(dá)性和可終止性。

通過遍歷所有安全域中策略規(guī)則的無環(huán)狀態(tài)有向圖對(duì)上述的所有異常情況進(jìn)行驗(yàn)證。為了便于執(zhí)行有向圖的深度優(yōu)先遍歷，降低復(fù)雜性，設(shè)置狀態(tài)有向圖不存在環(huán)路。在策略知識(shí)庫驗(yàn)證前，需要檢測安全域中的所有設(shè)備，明確所有設(shè)備能夠產(chǎn)生的狀態(tài)，構(gòu)建安全域狀態(tài)集state－Di，便于失效冗余檢測；同時(shí)，明確安全域中的安全設(shè)備能夠應(yīng)對(duì)的觸發(fā)條件集conditions，便于完整性檢測；還需明確狀態(tài)有向圖的根節(jié)點(diǎn) （初始狀態(tài)）和葉子節(jié)點(diǎn) （終止?fàn)顟B(tài)），便于可執(zhí)行性分析。

對(duì)系統(tǒng)中所有安全域?qū)?yīng)的無環(huán)狀態(tài)有向圖進(jìn)行深度優(yōu)先遍歷，可實(shí)現(xiàn)對(duì)策略規(guī)則的上述五類異常情況分析。在進(jìn)行正確性與一致性分析時(shí)，只需判斷狀態(tài)有向圖中由同一狀態(tài)節(jié)點(diǎn)出發(fā)的各條路徑中是否包含矛盾觸發(fā)條件，是否包含重復(fù)觸發(fā)條件。對(duì)于矛盾觸發(fā)條件引出的多個(gè)輸出狀態(tài)，如果相同，則違背正確性原則。對(duì)于重復(fù)觸發(fā)條件引出的多個(gè)輸出狀態(tài)，如果相同，則違背冗余性原則；如果不同，則違背一致性原則。

4 復(fù)雜度分析和實(shí)驗(yàn)

設(shè)系統(tǒng)中包含安全域的數(shù)量為k，設(shè)定安全域Di包含的狀態(tài)節(jié)點(diǎn)數(shù)為ni，邊數(shù)為ei，相鄰的兩個(gè)狀態(tài)之間可能有一條邊或多條邊。遍歷有向圖的時(shí)間復(fù)雜度為O（ni＋ei）。當(dāng)遍歷到某個(gè)節(jié)點(diǎn)時(shí)，將其引出的所有邊依次放在數(shù)組中，每條新加入的邊都要與數(shù)組中的邊進(jìn)行對(duì)比 （判斷是否重復(fù)或是否矛盾），考慮極端情況，即假設(shè)所有的邊都進(jìn)行對(duì)比，則比較次數(shù)為ei（ei－1）／2，時(shí)間復(fù)雜度為O2）?？紤]平均情況，設(shè)有向圖中有h個(gè)非葉子節(jié)點(diǎn)，且每個(gè)非葉子節(jié)點(diǎn)均引出e／h條邊，則比較總次數(shù)為ei（eih）／2h，對(duì)于一般的有向圖而言，h接近于ni／2，則有向邊之間進(jìn)行比較的時(shí)間復(fù)雜度一般為2／ni）。當(dāng)然，不管同一個(gè)狀態(tài)節(jié)點(diǎn)引出的有向邊之間重疊與否或矛盾與否，還需要對(duì)比其所有的輸出狀態(tài) （一致性檢驗(yàn)、重復(fù)性檢驗(yàn)和正確性檢驗(yàn)的需要），由于輸出狀態(tài)的數(shù)量不大于有向邊的數(shù)量 （兩個(gè)狀態(tài)之間可能出現(xiàn)多條路徑，但同一條邊不可能引出多個(gè)狀態(tài)），因此輸出狀態(tài)之間進(jìn)行比較的時(shí)間復(fù)雜度也可記作O2／ni）。另外，有向圖中的所有狀態(tài)與集合state－Di中元素進(jìn)行對(duì)比 （失效冗余檢驗(yàn)和可執(zhí)行性檢驗(yàn)）的時(shí)間復(fù)雜度為nisi（state－Di集合包含的元素個(gè)數(shù)為si）；所有邊與集合conditions中元素進(jìn)行對(duì)比 （完整性檢驗(yàn)）的時(shí)間復(fù)雜度為eici（conditions集合包含的元素個(gè)數(shù)為ci）。因此對(duì)于安全域Di中的策略進(jìn)行驗(yàn)證的平均時(shí)間復(fù)雜度為O（ni＋ei＋nisi＋eici＋2／ni），對(duì)于系統(tǒng)全體策略進(jìn)行驗(yàn)證的平均時(shí)間復(fù)雜度為

文獻(xiàn)[4]中，針對(duì)所有策略主體和客體分別構(gòu)建有向圖，策略沖突驗(yàn)證的時(shí)間復(fù)雜度為O（｜V｜2／2＋｜V｜），當(dāng)有向圖的規(guī)模較大時(shí)，時(shí)間復(fù)雜度相當(dāng)可觀；本文中按照安全域?qū)ο到y(tǒng)資源進(jìn)行劃分，對(duì)每個(gè)安全域分別構(gòu)建有向圖，雖然時(shí)間復(fù)雜度中也包含二次項(xiàng)O（nisi＋eici），但ni與ei的值由于安全域的劃分明顯減小，同時(shí)由于各個(gè)安全域彼此相互獨(dú)立，因此本文的策略驗(yàn)證方法更利于在分布式系統(tǒng)中進(jìn)行并發(fā)處理。

文獻(xiàn)[6]中，一致性檢驗(yàn)的時(shí)間復(fù)雜度為O（4n2），n為策略規(guī)則的數(shù)量。而本文中的策略驗(yàn)證復(fù)雜度在一致性方面表現(xiàn)為O（ni＋ei＋2／ni），ei代表某一個(gè)有向圖中策略規(guī)則的數(shù)量。對(duì)于稠密的有向圖而言，任意兩個(gè)狀態(tài)之間均有變遷，此時(shí)ei＝ni（ni－1）／2。對(duì)于中等稠密的有向圖而言，ei接近于ni（ni－1）／4。則本文一致性檢驗(yàn)的復(fù)雜度按照中密圖的標(biāo)準(zhǔn)可轉(zhuǎn)化為其中最高次項(xiàng)為。因此本文的一致性檢驗(yàn)方法在理論上優(yōu)于文獻(xiàn)[6]中的一致性檢驗(yàn)方法。

實(shí)驗(yàn)環(huán)境為Intel Core 2Duo，2GHz，2GRAM，windows7，Java語言，使用MySQL數(shù)據(jù)庫存儲(chǔ)安全策略和規(guī)則，對(duì)有向圖采用深度優(yōu)先搜索遍歷。以一個(gè)安全域中的狀態(tài)有向圖作為研究對(duì)象，將有向圖中的策略規(guī)則由40條逐步增加到400條，隨著策略規(guī)則的增多，安全域中的狀態(tài)數(shù)增多，對(duì)應(yīng)的算法執(zhí)行時(shí)間隨之增加，如圖3所示，總體執(zhí)行效率比較理想。

圖3 策略庫驗(yàn)證算法執(zhí)行結(jié)果

5 結(jié)束語

安全策略的合理性決定了網(wǎng)絡(luò)信息系統(tǒng)的安全性，同時(shí)是安全設(shè)備協(xié)同工作的必要前提。本文根據(jù)子網(wǎng)劃分安全域，定義了安全策略并根據(jù)狀態(tài)機(jī)模型將安全策略規(guī)則用無環(huán)有向圖進(jìn)行描述，闡述了策略庫的構(gòu)建方法和通過深度優(yōu)先遍歷狀態(tài)有向圖的方式對(duì)特定安全域中的安全策略規(guī)則進(jìn)行驗(yàn)證。本文介紹的策略驗(yàn)證方法不僅綜合考慮并分析了策略的正確性、完整性、一致性、冗余性和可執(zhí)行性幾種情況，同時(shí)通過復(fù)雜度分析說明了本文驗(yàn)證方法相對(duì)于現(xiàn)有策略驗(yàn)證方法的優(yōu)勢。實(shí)驗(yàn)證明基于狀態(tài)機(jī)模型的策略規(guī)則描述方法和策略庫驗(yàn)證算法具有理想的執(zhí)行速度，是有效可行的。

[1]Becker MY，F(xiàn)ournet C，Gorden AD.Design and semantics of a decentralized authorization language[C]／／Proc of the 20th IEEE Computer Security Foundations Symposium.Washington:IEEE Computer Society，2007.

[2]Gurevich Y，Neeman I.DKAL:Distributed Knowledge authorization language[C]／／Proc of the 21st IEEE Computer Security Foundations Symposium.Washington:IEEE Computer Society，2008.149－162.

[3]BAO Yibao，YIN Lihua，F(xiàn)ANG Binxing，et al.Approach of security policy expression and verification based on well－founded semantic[J].Journal of Software，2012，23 （4）:912－927（in Chinese）.[包義保，殷麗華，方濱興，等.基于良基語義的安全策略表達(dá)與驗(yàn)證方法[J]，軟件學(xué)報(bào)，2012，23（4）:912－927.]

[4]YAO Jian，MAO Bing，XIE Li.A Dag－based security policy conflicts detection method[J].Journal of Computer Research and Development，2005，42 （7）:1108－1114 （in Chinese）.[姚鍵，茅兵，謝立.一種基于有向圖模型的安全策略沖突檢測方法[J].計(jì) 算機(jī)研究與發(fā)展，2005，42 （7）:1108－1114.]

[5]ZHANG Huan，CAO Wanhua，F(xiàn)ENG Li，et al.A network security interaction policy model based on status transition[J].Ship Electric Engineering，2009，29 （3）:124－127 （in Chinese）.[張煥，曹萬華，馮力，等.基于狀態(tài)遷移的網(wǎng)絡(luò)安全聯(lián)動(dòng)策略模型[J].船舶電子工程，2009，29 （3）:124－127.]

[6]TANG Chenghua，YU Shunzheng.Verifying network security policy based on features[J].Journal of Computer Research and Decelopment，2009，46 （11）:1854－1861 （in Chinese）.[唐成華，余順爭.基于特征的網(wǎng)絡(luò)安全策略驗(yàn)證[J].計(jì)算機(jī)研究與發(fā)展，2009，46 （11）:1854－1861.]

[7]LIU Daobin，GUO Li，BAI Shuo.A methodology for analyzing security policy in workflow[J].Journal of Computer Research and Development，2008，45 （6）:967－973 （in Chinese）.[劉道斌，郭莉，白碩.一種工作流安全策略分析方法[J]，計(jì)算機(jī)研究與發(fā)展，2008，45 （6）:967－973.]

[8]TANG Chenghua.Research on key technologies of network security management policy[D].Beijing:Institute of Technology，2006:47－57 （in Chinese）.[唐成華.網(wǎng)絡(luò)安全管理策略關(guān)鍵技術(shù)研究[D].北京:北京理工大學(xué)，2006:47－57.]

[9]LI Li，LI Zhiping，WANG Liang，et al.A finite－state machine model for strategy table search and match of standardized stability control device[J].Automation of Electric Power Systems，2012，36 （17）:86－89 （in Chinese）.[李力，李志平，王亮，等.穩(wěn)定控制裝置中策略搜索匹配狀態(tài)機(jī)模型[J].電力系統(tǒng)自動(dòng)化，2012，36 （17）:86－89.]

[10]ZANG Tianning，YUN Xiaochun，ZHANG Yongzheng，et al.A model of network device coordinative run[J].Chinese Journal of Computers，2011，34 （2）:216－228 （in Chinese）.[臧天寧，云曉春，張永錚，等.網(wǎng)絡(luò)設(shè)備協(xié)同聯(lián)動(dòng)模型[J].計(jì)算機(jī)學(xué)報(bào)，2011，34 （2）:216－228.]

[11]TANG Chenghua，YAO Shuping，ZHANG Xiang，et al.Research on security policy in NSMP[J].Journal of Computer Research and Development，2006，43 （Suppl.）:430－436（in Chinese）.[唐成華，姚淑萍，張翔，等.網(wǎng)絡(luò)安全綜合監(jiān)控平臺(tái)中安全策略的研究[J].計(jì)算機(jī)研究與發(fā)展，2006，43 （增刊）:430－436.]