基于狀態機模型的網絡安全策略驗證方法研究

程曉榮，馮志偉

（華北電力大學 控制與計算機工程學院，河北 保定071003）

0 引 言

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

1 相關概念

在網絡信息安全系統中，安全域構成環境的子集，是由一系列實體與資源構成的[6]。安全域的劃分有多種方式，文獻[8]根據設備類型與業務將安全域劃分為安全業務域、安全用戶域、網絡設備域和安全網絡域。上述劃分方式雖然分離了不同安全域的職責，但當網絡結構較為復雜時，每個安全域的規模會非常龐大，不利于安全域中實體或資源的查詢。本文將安全域按照子網的方式劃分，因為子網中同時包含了防火墻、IPS等安全設備和這些安全設備控制范圍內的實體資源，安全事件的捕獲和策略的分發都可以在子網內部完成。同時按照子網劃分安全域可以降低安全域的規模。

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

下面介紹相關的定義:

定義1 狀態機，全稱為有限狀態機 （finite－state machine，FSM），是表示有限個狀態以及在這些狀態之間的轉移和動作等行為的數學模型。本文采用Mealy型狀態機，它的下一個狀態即輸出是由輸入和當前狀態決定的[9]。本文闡述的狀態機考慮單向的狀態流動，即從開始狀態到終止狀態的變遷過程可由無環有向圖來描述。狀態機由五元組 （∑，S，s0，δ，F）構成，它們的含義分別為:

∑表示輸入的非空有限集合，對應系統的觸發條件集；

S表示狀態的非空有限集合，對應系統的當前狀態集和輸出狀態集；

s0表示初始狀態，其中s0∈S；

δ表示狀態轉移函數，即δ:S×∑→S，即系統當前狀態集在觸發條件的作用下變遷為輸出狀態集；

F表示最終狀態的集合，到達最終狀態后不會再向其它狀態轉移，其中FS。

定義2 安全域D。安全域可以看作是系統中實體和安全策略的組合。安全域將規模龐大的網絡信息系統劃分為較小的研究單元，對每個研究單元分別制定安全策略，通過將不同安全域中的安全策略相關聯，可以得到系統整體的安全策略。本文根據子網劃分安全策略，使子網間的安全策略執行能夠相互獨立。網絡信息系統的安全策略知識庫是其包含的所有安全域的安全策略并集。

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

圖1 安全策略的執行過程

2 策略知識庫與系統運行分析

本節介紹通過狀態機模型建立特定安全域的策略規則庫的方法，一個安全域的全部策略規則對應一個完整的狀態機，可以用無環狀態有向圖展現狀態之間的變遷關系，如圖2所示。下面有向圖中展現的一個或多個狀態變遷即構成某個特定安全域的規則庫。

通過子網劃分的安全域中主要包含服務器，用戶主機，網絡設備和各類安全設備。其中安全設備主要包括防火墻、IPS、防病毒系統和掃描器等。圖2中狀態機的初始狀態為“系統運行”狀態，狀態變遷包括系統自發的狀態變遷和因策略執行由觸發動作引發的狀態變遷兩類，前者不包含觸發條件，輸出的狀態在系統運行過程中始終存在于當前狀態集中，在狀態圖中用橢圓形的節點標識；后者代表的策略規則統一存儲在策略知識庫中，是本文主要的研究對象，在狀態圖中用矩形節點標識。

圖2 策略規則的無環狀態有向圖描述

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

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

3 策略庫知識庫驗證

知識庫中的策略規則可能存在不合理性，需要對其進行異常分析，策略規則的驗證主要包括正確性分析、完整性分析、一致性分析、冗余性分析、可執行性分析。針對特定安全域中的策略規則，通過以下幾個方面進行規則驗證。

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

定義4 對于策略集P中的任意兩個策略Pi和Pj，滿足:

當且僅當 （Pi·Ci，Pj·Cj）∈∝時，稱策略集P符合正確性要求，其中∝表示策略動作的非矛盾關系集。

在實際應用中，存在諸多的矛盾觸發條件，例如可信IP地址和不可信IP地址、登錄成功和登錄失敗、發現漏洞和未發現漏洞、系統無開發任務和開發任務等。舉例說明:

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

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

規則r2→LP表示 “當Web服務開啟時，檢測到連接的IP地址為不可信IP地址，則鎖定用戶IP”。

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

（2）完整性分析：完整性是指對于系統能夠捕獲到的所有觸發事件，策略知識庫中都有相應的處理策略。

定義5 對于系統觸發事件集conditions的任意一個觸發條件c，滿足：

在復雜的網絡環境中，不能確保所有安全事件都有相應的處理策略，出現不完整的情況是很有可能的，此時可以構造默認策略滿足完整性要求，比如 “向管理員發出特殊事件告警”等默認策略。

（3）一致性分析：策略的一致性保證策略集中不能發生同時應用在同一個對象上的兩種不同策略［11］。如果策略作用于相同的安全域且觸發條件相同，那么在此安全域策略規則的狀態有向圖中，對于同一個原狀態，同一個它的觸發條件不能引發多個不同的輸出狀態。

定義6 對于策略集P中的任意兩個策略Pi和Pj，滿足：

則稱策略集P是一致的。

定義7 對于策略集P中的任意兩個策略Pi和Pj，若滿足：

當且僅當ri·oi≠rj·oj時，策略集P是一致的。

策略不一致往往是因為策略在添加、修改過程中更新后的安全策略與系統內原有的其它安全策略發生一致性沖突；還有一種原因是安全策略對于處理某類安全事件的效果沒有明確之前，往往會出現備選策略，策略與其備選策略之間會存在不一致性，因此在策略知識庫驗證時要排除備選策略的干擾。下面舉例說明違背一致性的策略：

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

規則r3：V（v）→VK表示 “當防病毒系統開啟時，檢測到發現病毒事件，則啟動病毒查殺程序”；

規則r4：V（v）→SC表示 “當防病毒系統開啟時，檢測到發現病毒事件，則進行漏洞修復操作”。

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

（4）冗余性分析：策略的冗余性包含兩種情況。如果兩條策略完全一致，即作用的安全域、觸發條件與執行規則均完全一致，稱為重復冗余；如果策略作用的安全域中策略主體或策略客體因系統更新或網絡拓撲結構發生變化而脫離安全域，此時相關的策略無法執行，稱為失效冗余。

定義8 對于策略集P中的任意兩個策略Pi和Pj，若滿足：

當且僅當ri·ii＝rj·ij且ri·oi＝rj·oj時，稱策略集P存在重復冗余。

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

對于重復冗余的檢測，只需逐條對比兩條策略的所有參數；對于失效冗余的檢測，需要對設備進行定期監控，確保策略庫所有規則包含的狀態都屬于當前安全域中設備能夠產生的狀態。

（5）可執行性分析：策略的可執行性需要保證規則狀態有向圖中所有的狀態必須可達，同時保證所有的狀態節點都具有能達到最終狀態的路徑。一個安全域只對應唯一的狀態有向圖，且狀態有向圖具有唯一的根節點。只需保證在有向圖的一次遍歷中能夠經過安全域內所有的狀態節點，且所有的葉子節點都為最終狀態節點，則能夠保證策略規則的可達性和可終止性。

通過遍歷所有安全域中策略規則的無環狀態有向圖對上述的所有異常情況進行驗證。為了便于執行有向圖的深度優先遍歷，降低復雜性，設置狀態有向圖不存在環路。在策略知識庫驗證前，需要檢測安全域中的所有設備，明確所有設備能夠產生的狀態，構建安全域狀態集state－Di，便于失效冗余檢測；同時，明確安全域中的安全設備能夠應對的觸發條件集conditions，便于完整性檢測；還需明確狀態有向圖的根節點 （初始狀態）和葉子節點 （終止狀態），便于可執行性分析。

對系統中所有安全域對應的無環狀態有向圖進行深度優先遍歷，可實現對策略規則的上述五類異常情況分析。在進行正確性與一致性分析時，只需判斷狀態有向圖中由同一狀態節點出發的各條路徑中是否包含矛盾觸發條件，是否包含重復觸發條件。對于矛盾觸發條件引出的多個輸出狀態，如果相同，則違背正確性原則。對于重復觸發條件引出的多個輸出狀態，如果相同，則違背冗余性原則；如果不同，則違背一致性原則。

4 復雜度分析和實驗

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

文獻[4]中，針對所有策略主體和客體分別構建有向圖，策略沖突驗證的時間復雜度為O（｜V｜2／2＋｜V｜），當有向圖的規模較大時，時間復雜度相當可觀；本文中按照安全域對系統資源進行劃分，對每個安全域分別構建有向圖，雖然時間復雜度中也包含二次項O（nisi＋eici），但ni與ei的值由于安全域的劃分明顯減小，同時由于各個安全域彼此相互獨立，因此本文的策略驗證方法更利于在分布式系統中進行并發處理。

文獻[6]中，一致性檢驗的時間復雜度為O（4n2），n為策略規則的數量。而本文中的策略驗證復雜度在一致性方面表現為O（ni＋ei＋2／ni），ei代表某一個有向圖中策略規則的數量。對于稠密的有向圖而言，任意兩個狀態之間均有變遷，此時ei＝ni（ni－1）／2。對于中等稠密的有向圖而言，ei接近于ni（ni－1）／4。則本文一致性檢驗的復雜度按照中密圖的標準可轉化為其中最高次項為。因此本文的一致性檢驗方法在理論上優于文獻[6]中的一致性檢驗方法。

實驗環境為Intel Core 2Duo，2GHz，2GRAM，windows7，Java語言，使用MySQL數據庫存儲安全策略和規則，對有向圖采用深度優先搜索遍歷。以一個安全域中的狀態有向圖作為研究對象，將有向圖中的策略規則由40條逐步增加到400條，隨著策略規則的增多，安全域中的狀態數增多，對應的算法執行時間隨之增加，如圖3所示，總體執行效率比較理想。

圖3 策略庫驗證算法執行結果

5 結束語

安全策略的合理性決定了網絡信息系統的安全性，同時是安全設備協同工作的必要前提。本文根據子網劃分安全域，定義了安全策略并根據狀態機模型將安全策略規則用無環有向圖進行描述，闡述了策略庫的構建方法和通過深度優先遍歷狀態有向圖的方式對特定安全域中的安全策略規則進行驗證。本文介紹的策略驗證方法不僅綜合考慮并分析了策略的正確性、完整性、一致性、冗余性和可執行性幾種情況，同時通過復雜度分析說明了本文驗證方法相對于現有策略驗證方法的優勢。實驗證明基于狀態機模型的策略規則描述方法和策略庫驗證算法具有理想的執行速度，是有效可行的。

[1]Becker MY，Fournet 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，FANG 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）.[包義保，殷麗華，方濱興，等.基于良基語義的安全策略表達與驗證方法[J]，軟件學報，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].計 算機研究與發展，2005，42 （7）:1108－1114.]

[5]ZHANG Huan，CAO Wanhua，FENG Li，et al.A network security interaction policy model based on status transition[J].Ship Electric Engineering，2009，29 （3）:124－127 （in Chinese）.[張煥，曹萬華，馮力，等.基于狀態遷移的網絡安全聯動策略模型[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）.[唐成華，余順爭.基于特征的網絡安全策略驗證[J].計算機研究與發展，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]，計算機研究與發展，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）.[唐成華.網絡安全管理策略關鍵技術研究[D].北京:北京理工大學，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）.[李力，李志平，王亮，等.穩定控制裝置中策略搜索匹配狀態機模型[J].電力系統自動化，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）.[臧天寧，云曉春，張永錚，等.網絡設備協同聯動模型[J].計算機學報，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）.[唐成華，姚淑萍，張翔，等.網絡安全綜合監控平臺中安全策略的研究[J].計算機研究與發展，2006，43 （增刊）:430－436.]