裴 斐,金 秋

(中原工學(xué)院,鄭州 450007)

一種網(wǎng)絡(luò)可生存性檢驗(yàn)?zāi)Ｐ偷男问津?yàn)證

裴 斐,金 秋

(中原工學(xué)院,鄭州 450007)

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

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

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

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

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

1 驗(yàn)證模型

1.1 基本概念

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

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

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

表1 符號(hào)定義表

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

(S,A,I,D,R):表示關(guān)鍵服務(wù)在遭受到攻擊后,進(jìn)行識(shí)別、抵抗、恢復(fù);

(S,F,I,R):表示關(guān)鍵服務(wù)在遭受到故障后,進(jìn)行識(shí)別和恢復(fù);

(S,E,I,R):表示關(guān)鍵服務(wù)在遭受到事故后,進(jìn)行識(shí)別和恢復(fù).

1.2 理論模型

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

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

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

(2)拓?fù)浒l(fā)生模塊.主要功能是將網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)傳遞到措施部署模塊.

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

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

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

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

驗(yàn)證模型在初始階段分別輸入用戶構(gòu)建的可生存模型和網(wǎng)絡(luò)拓?fù)?可生存性模型轉(zhuǎn)化為可生存性策略,再和網(wǎng)絡(luò)拓?fù)湟黄鹜ㄟ^措施部署模塊轉(zhuǎn)化成可部署的仿真任務(wù),而后由任務(wù)部署模塊分配到仿真主機(jī),實(shí)現(xiàn)仿真運(yùn)行.

2 形式化分析

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

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

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

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

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

可生存性服務(wù)server;

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

生存機(jī)制集合Mechanism={i,d,r};

輸入集合Input={m,to},分別表示模型和網(wǎng)絡(luò)拓?fù)?

仿真任務(wù)集合Task={h,ta};

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

變遷M T的定義為:

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

變遷MC的定義為:

措施生成托肯可進(jìn)一步擴(kuò)展為2個(gè)變遷和1個(gè)庫所,如圖3所示.

圖3 措施生成擴(kuò)展模型

變遷M[Preview表示由策略和拓?fù)渖煽缮娴膱?chǎng)景,記作:

變遷M[Respond表示由可生存場(chǎng)景和反應(yīng)機(jī)制生成安全任務(wù),記作:

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

圖4 仿真任務(wù)部署擴(kuò)展模型

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

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

(Phost)≥1)

變遷M[Assign表示將仿真原子任務(wù)和主機(jī)性能進(jìn)行配,獲得仿真任務(wù)托肯,記作:

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

(Passemble≥1)

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

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

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

3 實(shí)現(xiàn)與驗(yàn)證

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

圖5 有色 Petri模型圖

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

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

表2 符號(hào)定義

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

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

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

表4 有色集合上下限分析

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

4 結(jié) 語

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

[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] 王衡軍,王亞弟,韓繼紅.移動(dòng)Ad hoc網(wǎng)絡(luò)安全分簇綜述[J].計(jì)算機(jī)科學(xué),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

河南省科技攻關(guān)計(jì)劃項(xiàng)目(092102310038);河南省自然科學(xué)基金項(xiàng)目(082102210082)

裴 斐(1977-),男,河北邯鄲人,實(shí)驗(yàn)師,碩士.