一種網(wǎng)絡可生存性檢驗模型的形式驗證

裴 斐,金 秋

(中原工學院,鄭州 450007)

一種網(wǎng)絡可生存性檢驗模型的形式驗證

裴 斐,金 秋

(中原工學院,鄭州 450007)

提出了一種基于分布式仿真平臺的可生存性驗證模型,實現(xiàn)了對不同種可生存性模型的統(tǒng)一檢驗.使用有色Petri網(wǎng)驗證表明,該模型滿足可達、有界、公平等基本性質(zhì),形式驗證為模型的實例化做好了準備.

可生存性;分布式仿真;有色 Petri

計算機網(wǎng)絡可生存性概念自提出之后,其定義一直尚未統(tǒng)一,按照CMU的權威定義[1],它是指系統(tǒng)處于侵入或混亂狀態(tài)下,對關鍵服務提供保障的能力.

目前,關于計算機網(wǎng)絡可生存性模型的研究已有多方面的研究成果,例如,Khin M i[2]在2005年提出了一種在DOS攻擊下的群組系統(tǒng)可生存性模型,能夠使系統(tǒng)在受到入侵攻擊時繼續(xù)運行,并且持續(xù)提供關鍵服務,溫和地降低非關鍵服務的功能性;Dong Seong Kim[3]提出了一種針對無線傳感器網(wǎng)絡(WSN)的可生存性模型的框架,用分層動態(tài)拓撲結(jié)構(gòu)實現(xiàn)對網(wǎng)絡安全的控制;Kerom ytis A D[4]在自動協(xié)調(diào)的模式下提出了運用多種安全機制和可生存性機制,能夠阻止、規(guī)避以及對多種攻擊進行反抗的一種可生存性模型;王衡軍[5]提出了一種采用分布式CA、安全簇和信任度評估的可生存性模型;Lima M N[6]提出了一種以預防式、反應式和容錯式為主要基礎的可生存性模型,該模型可以保障連通、路由和通信服務等關鍵服務.

考慮到網(wǎng)絡中的復雜性,各模型因為驗證環(huán)境和實施手段的不一致而缺乏有力的比較.本文從模型驗證的觀點出發(fā),提出了一種驗證系統(tǒng)可生存性的模型.利用仿真網(wǎng)絡環(huán)境,將不同的可生存性模型描述成一致的可生存性策略,進而在仿真環(huán)境下予以驗證和實現(xiàn).

1 驗證模型

1.1 基本概念

研究涉及的主要概念包括引發(fā)可生存性的外部因素和系統(tǒng)組成要素.

根據(jù)可生存性的定義,引起系統(tǒng)可生存性的外部因素主要包括攻擊(A)、故障(F)、事故(E),響應機制有識別(I)、抵抗(D)、恢復(R).

在可生存性驗證系統(tǒng)中,主要涉及的元素如表1所示.

表1 符號定義表

可生存性策略針對3種不同的外部因素,可表示為以下3種形式:

(S,A,I,D,R):表示關鍵服務在遭受到攻擊后,進行識別、抵抗、恢復;

(S,F,I,R):表示關鍵服務在遭受到故障后,進行識別和恢復;

(S,E,I,R):表示關鍵服務在遭受到事故后,進行識別和恢復.

1.2 理論模型

可生存性模型的驗證結(jié)構(gòu)如圖1所示.模型共分為6個組成部分,分別為模型描述模塊、拓撲發(fā)生模塊、策略抽取模塊、措施部署模塊、仿真任務部署模塊和仿真執(zhí)行模塊.

圖1 驗證模型層次結(jié)構(gòu)圖

(1)模型描述模塊.主要功能是實現(xiàn)模型的轉(zhuǎn)換,使用圖形的方式描述模型的轉(zhuǎn)換,并按照統(tǒng)一的描述語言語義給出模型描述.

(2)拓撲發(fā)生模塊.主要功能是將網(wǎng)絡拓撲結(jié)構(gòu)傳遞到措施部署模塊.

(3)策略抽取模塊.主要功能是實現(xiàn)可生存性模型中生存策略的轉(zhuǎn)換.其形式記作M odel?Policy.

(4)措施部署模塊.主要功能是根據(jù)網(wǎng)絡的實際拓撲和規(guī)則,產(chǎn)生相關的網(wǎng)絡可生存性措施部署.其形式記為Topology-Po licy measure.

(5)仿真任務部署模塊.主要功能是將可生存性策略和實際仿真主機性能進行匹配,給出較優(yōu)方案,交付仿真平臺實行.其形式記作 M easure-Capability Scheme.

(6)仿真執(zhí)行模塊.主要功能是將部署后的仿真任務交由仿真平臺執(zhí)行.其形式記作Scheme?Simulation.

驗證模型在初始階段分別輸入用戶構(gòu)建的可生存模型和網(wǎng)絡拓撲,可生存性模型轉(zhuǎn)化為可生存性策略,再和網(wǎng)絡拓撲一起通過措施部署模塊轉(zhuǎn)化成可部署的仿真任務,而后由任務部署模塊分配到仿真主機,實現(xiàn)仿真運行.

2 形式化分析

對以上驗證模型使用有色 Petri網(wǎng)建立模型,分析其系統(tǒng)的機制.本文對該模型的有色Petri網(wǎng)拓撲、顏色集合和變遷進行定義,總體模型如圖2所示.

圖2 Petri網(wǎng)總體模型

定義1 驗證模型VM=(P,T,M,T),其中:

P={Model,Topology,Policy,M easure,Task,Result}分別記錄模型、網(wǎng)絡拓撲、策略、措施、仿真任務和結(jié)果;T={M T,MC,DS,simulate},分別記錄模型到策略、策略到措施、措施到仿真任務部署和仿真任務實施等4個主要的變遷活動.

定義2 模型的托肯有色集合為:

可生存性服務server;

可生存事件集合Event={a,f,e};

生存機制集合Mechanism={i,d,r};

輸入集合Input={m,to},分別表示模型和網(wǎng)絡拓撲;

仿真任務集合Task={h,ta};

仿真結(jié)果集合{R}.

變遷M T的定義為:

指當模型庫所中存在托肯(可生存性模型)時,變遷觸發(fā).

變遷MC的定義為:

措施生成托肯可進一步擴展為2個變遷和1個庫所,如圖3所示.

圖3 措施生成擴展模型

變遷M[Preview表示由策略和拓撲生成可生存的場景,記作:

變遷M[Respond表示由可生存場景和反應機制生成安全任務,記作:

仿真任務部署可擴展為3個庫所和3個托肯,如圖4所示.其中變遷 M[Respond表示將仿真任務劃分為原子仿真任務,并生成主機性能測量托肯,記作:

圖4 仿真任務部署擴展模型

變遷M[Collect表示將主機性能測量庫所轉(zhuǎn)化為性能庫所,記作:

變遷 M[Collect＞ ?(?p)(p=h∧p∈Phost∧M

(Phost)≥1)

變遷M[Assign表示將仿真原子任務和主機性能進行配,獲得仿真任務托肯,記作:

M[Assign＞ ?(?p)(p=as∧p∈Passemble∧M

(Passemble≥1)

∧(?p)(p=ca∧p∈P capability∧M(Pcapability≥1)

變遷M[Sim ulate表示將分配任務交由仿真主機運行,獲得仿真運行結(jié)果,記作:

M[Sim u late＞ ?(?p)(p=∧ta∈Psimulate∧M(Psimulate≥1)

3 實現(xiàn)與驗證

根據(jù) Petri網(wǎng)形式化模型,使用CPN Tools軟件對模型進行實例化構(gòu)建,構(gòu)建的有色結(jié)構(gòu)如圖5所示.對模型的可達、有界、活性及公平性等特性進行分析.

圖5 有色 Petri模型圖

圖5中染色托肯的定義如表2所示.

系統(tǒng)的狀態(tài)分析結(jié)果顯示,系統(tǒng)的狀態(tài)空間節(jié)點數(shù)為2 429個,弧數(shù)為8 450個;與強連通圖(SCC)生成的節(jié)點數(shù)和弧數(shù)相同,從而證明系統(tǒng)不存在無限發(fā)生序列.

表2 符號定義

對該模型的可達性分析主要是通過添加不同的托肯集合,模擬運算實現(xiàn)的,其中模擬運算的結(jié)果如表3所示.

表3 確定托肯上下限測分析結(jié)果

系統(tǒng)的有界性通過對模型的上下確定集合表示,其分析結(jié)果如表4所示.

表4 有色集合上下限分析

通過對系統(tǒng)的主標記和活性分析可知,模型的主標記數(shù)為2 429,終止標記為2 429,二者相等;同時針對活性分析可知,系統(tǒng)無活變遷和終止變遷,從而證明系統(tǒng)為活性.

4 結(jié) 語

本文提出了一種網(wǎng)絡可生存性驗證系統(tǒng)的模型,該模型使用統(tǒng)一的模型描述語言完成對不同種可生存性模型的描述,并從中抽取出相關的安全策略,轉(zhuǎn)換成相應的仿真任務,在分布式仿真平臺上運行.對該模型的形式化驗證表明,該模型滿足模型描述的可達、有界、公平等一系列特性.

[1] Ellison R J,Moo re A P.Trustwo rthy Refinement through Intrusion-Aware Design(TRIAD)(CMU/SEI-03-TR-002)[R].Pittsburgh,PA,USA:Software Engineering Institute,2003:21-29.

[2] Aung K M,Park K,Park J S,et al.A Survivability Model fo r Cluster System Under DoS A ttacks[J].High Perfo rmance Computing and Communications(S0302-9743),2005,3726:567-572.

[3] Kim D S,Shazzad K M,Park J S.A Framewo rk of Survivability Model fo r W ireless Senso r Netwo rk[C]//.First International Conference on Availability and Security(ARES’06).Vienna Austria:IEEE Computer Society,2006:515-522.

[4] Keromytis A D,Parekh J,Gross P N,et al.A Holistic App roach to Service Survivability[C]//.10th ACM Conference on Computer and Communications Security.Fairfax,VA:ACM,2003:11-22.

[5] 王衡軍,王亞弟,韓繼紅.移動Ad hoc網(wǎng)絡安全分簇綜述[J].計算機科學,2009(10):38-41.

[6] Lima M N,Da Silva H W,Dos Santos A L,et al.An A rchitecture fo r Aurvivable Mesh Netwo rking[C]//.the 2008 IEEE Global Communications Conference(GLOBECOM’08).Los A lamitos,CA,USA:IEEECommunications Society,2008:688-692.

Formal Verification of a Network Survivability Validate Model

PEIFei,JIN Qiu
(Zhongyuan U niversity of Technology,Zhengzhou 450007,China)

Survivability is a focus of network security research.A kind of the unified verification mechanism is needed,because every kind of survivability model has itsow n execution environment.This paper introduces a netwo rk survivability validate model,w hich is based on a distributed sim ulation p latfo rm and can validate and verify different kinds of survivability models.The results of formal verification using colored Petri Nets demonstrates that the testing model has the basic p roperties such as accessibility,boundedness and fair.

survivability;distributed simulation;colored petri

TP309B

A DO I:10.3969/j.issn.1671-6906.2010.04.006

1671-6906(2010)04-0022-05

2010-07-06

河南省科技攻關計劃項目(092102310038);河南省自然科學基金項目(082102210082)

裴 斐(1977-),男,河北邯鄲人,實驗師,碩士.