王 婷，項露露，陳鐵明

(浙江工業(yè)大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，杭州 310023)E-mail：tmchen@zjut.edu.cn

1 引 言

針對網(wǎng)絡(luò)空間防御的被動局面，美國率先提出移動目標(biāo)防御(MTD，moving target defense)思想[1].該技術(shù)通過提高網(wǎng)絡(luò)靈活性、不斷改變攻擊面、減弱系統(tǒng)靜態(tài)性，使攻擊者難以定位攻擊目標(biāo)，減少被攻擊的機(jī)會.國內(nèi)研究者提出網(wǎng)絡(luò)空間擬態(tài)防御(Cyber Mimic Defense，CMD)[2].該防御采用“動態(tài)、異構(gòu)、冗余”機(jī)制，為受保護(hù)目標(biāo)構(gòu)建多種功能等效變體，組合構(gòu)造搭建異構(gòu)冗余池，動態(tài)選擇安排變體并行運(yùn)行，并采用仲裁機(jī)制來決定當(dāng)前運(yùn)行變量的結(jié)果是否正確，從而達(dá)到防御目的.

目前對安全防御行為過程的抽象化研究，難以對防御機(jī)制的可行性、安全性等進(jìn)行評估和系統(tǒng)性分析.因此對網(wǎng)絡(luò)空間擬態(tài)防御機(jī)制進(jìn)行形式化規(guī)約，分析系統(tǒng)安全性成為當(dāng)前研究的重點(diǎn).

文獻(xiàn)[3]中提出了使用貝葉斯網(wǎng)絡(luò)的加權(quán)攻擊路徑建模技術(shù)模擬攻擊路徑.常用攻擊樹模型[4]等可對網(wǎng)絡(luò)攻擊進(jìn)行建模，反映攻擊與網(wǎng)絡(luò)系統(tǒng)之間的狀態(tài)關(guān)系.但是該模型側(cè)重于對攻擊成功特性的模型構(gòu)建，很少考慮對防御行為的描述.單控制隨機(jī)博弈[5]、貝葉斯隨機(jī)博弈[6]、馬爾可夫博弈模型[7]等經(jīng)典博弈模型可用于防御系統(tǒng)的分析建模，但系統(tǒng)場景中的多狀態(tài)、高動態(tài)使得模型難以描述，同時也無法描述多個組件的內(nèi)在關(guān)系.文獻(xiàn)[8]使用時間自動機(jī)構(gòu)建EPC網(wǎng)絡(luò)的入侵模型，包括入侵系統(tǒng)中網(wǎng)絡(luò)環(huán)境實體、原子攻擊和組合攻擊的形式化描述，并展現(xiàn)了時間屬性.文獻(xiàn)[9]將SOC總線框架抽象為時間自動機(jī)網(wǎng)絡(luò)，使用模型檢查器UPPAAL驗證SOC的安全屬性.文獻(xiàn)[10]通過時間自動機(jī)對RGMP-ROS系統(tǒng)進(jìn)行形式化描述和分析以驗證該系統(tǒng)的實時性.文獻(xiàn)[11]使用UPPAAL對認(rèn)知機(jī)器人的控制行為的正確性和實時性進(jìn)行形式化分析和建模.文獻(xiàn)[12]通過時間自動機(jī)對物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的機(jī)密性、可用性、健壯性進(jìn)行建模和驗證.

綜上所述，由于時間自動機(jī)是實時系統(tǒng)形式化建模和驗證的主要手段，并且擬態(tài)防御系統(tǒng)模型除了行為過程以外也具有時間性要求，因此本文選用時間自動機(jī)對其進(jìn)行建模和分析.模型描述了擬態(tài)防御系統(tǒng)的主動防御機(jī)制，以及清洗恢復(fù)、判決策略等邏輯過程，并基于PAT[13]模型檢測工具對模型進(jìn)行了自動化驗證和分析，包括死鎖檢測、可達(dá)性驗證、基于線性時序邏輯LTL的驗證和語言包含[14]檢查等多種方式.基于時間自動機(jī)理論的模型檢測工具目前主要是UPPAAL[15]和PAT.PAT在UPPAAL所具備功能的基礎(chǔ)上，增加了時間自動機(jī)的語言包含檢查(將系統(tǒng)模型和待驗證屬性都用時間自動機(jī)表示，再使用自動化的語言包含檢查算法)，能夠驗證跟時間有關(guān)的屬性.因此本文采用了PAT工具對擬態(tài)防御系統(tǒng)進(jìn)行建模和驗證，并對系統(tǒng)正確性和有效性進(jìn)行了分析.本文對驗證屬性的描述基于前面提到的多種方式，面向擬態(tài)防御系統(tǒng)中正常持續(xù)工作過程、攻擊后清洗恢復(fù)、輸出結(jié)果判定、執(zhí)行體冗余和變換等關(guān)鍵方面的正確性.

本文第二節(jié)介紹時間自動機(jī)模型和工具；第三節(jié)介紹擬態(tài)防御系統(tǒng)架構(gòu)并對擬態(tài)防御系統(tǒng)進(jìn)行形式化建模；第四節(jié)給出擬態(tài)防御系統(tǒng)的判決策略、主動防御、清洗恢復(fù)等機(jī)制得時間自動機(jī)模型；第五節(jié)對系統(tǒng)需要滿足的屬性進(jìn)行驗證和分析.第六節(jié)對文章進(jìn)行總結(jié).

2 時間自動機(jī)介紹

時間自動機(jī)[16]由Alur和Dill于1994年首次提出，是配有一個或者多個時鐘的有限狀態(tài)機(jī).將時間約束引入有限狀態(tài)機(jī)能夠更好地描述實時系統(tǒng)中的動作和狀態(tài)，當(dāng)滿足時鐘約束條件時，狀態(tài)才發(fā)生轉(zhuǎn)移，否則停留在當(dāng)前狀態(tài)；當(dāng)滿足狀態(tài)上的狀態(tài)不變式時，可以駐留當(dāng)前狀態(tài)，否則必須要離開當(dāng)前狀態(tài).

時間自動機(jī)可以被視為一個六元組(L，L0，M，X，I，E)，其中L：狀態(tài)集合；L0：初始狀態(tài)集，L0L；M：事件集合；X：時鐘變量集合；I：狀態(tài)不變式；E：狀態(tài)轉(zhuǎn)移函數(shù).E?L×M×φ(X)×2X×L為帶時間約束的轉(zhuǎn)移關(guān)系，包含自動機(jī)中的所有邊.規(guī)則轉(zhuǎn)換(l，m，x，z，l′)表示處于狀態(tài)位置l的時，時鐘滿足約束條件x，系統(tǒng)可以發(fā)生事件m，從狀態(tài)l轉(zhuǎn)移到狀態(tài)l′并完成z中的時間重置為0.表1介紹了利用PAT建模過程中需要用到的符號.

表1 時間自動機(jī)常用符號

3 擬態(tài)防御架構(gòu)時間自動機(jī)描述

擬態(tài)防御系統(tǒng)采用動態(tài)異構(gòu)冗余結(jié)構(gòu)，以及清洗與重構(gòu)機(jī)制，將不確定性的干擾轉(zhuǎn)化為可控事件.動態(tài)異構(gòu)冗余結(jié)構(gòu)包括輸入代理、執(zhí)行體、異構(gòu)組件、裁決器和以及裁決組件.清洗與重構(gòu)可以使受到攻擊的執(zhí)行體恢復(fù)正常狀態(tài).擬態(tài)防御體系的架構(gòu)[17]如圖1(a)所示.

1. 系統(tǒng)接收到輸入請求；

2. 輸入代理向N個異構(gòu)執(zhí)行體分發(fā)請求；

3. N個異構(gòu)執(zhí)行體將計算結(jié)果反饋至裁決器；

4. 裁決器通過比較策略選擇輸出結(jié)果，同時判斷異構(gòu)執(zhí)行體是否受到攻擊，受到攻擊的執(zhí)行體需要進(jìn)入清洗狀態(tài)；

5. 裁決器分發(fā)關(guān)機(jī)信號.

我們使用時間自動機(jī)模擬抽象執(zhí)行體和裁決器相互通信，以及系統(tǒng)清洗等流程.

#define N 10；/*含有十個個執(zhí)行體*/

varworkNumber=0；/*開始后工作中執(zhí)行體個數(shù)*/

varwashNumber=0；/*開始后清洗中執(zhí)行體個數(shù)*/

varisWash[N]；/*為三個執(zhí)行體標(biāo)記是否處于清洗狀態(tài)，數(shù)組下標(biāo)為執(zhí)行體序號，isWash[i]=0表示i號執(zhí)行體不處于清洗狀態(tài)，isWash[i]=1表示i號執(zhí)行體處于清洗狀態(tài)*/

varisOn=false；/*isOn=false時系統(tǒng)未正常啟動，isOn=true時系統(tǒng)啟動*/

varonNumber=0；/*啟動成功執(zhí)行體個數(shù)*/

channelok；/*清洗完成信號*/

channelready；/*執(zhí)行體準(zhǔn)備就緒信號*/

channelturnoff；/*裁決器向執(zhí)行體發(fā)送關(guān)機(jī)信號*/

channelwash；/*清洗信號*/

擬態(tài)架構(gòu)執(zhí)行體(Process)時間自動機(jī)模型如圖1(b)所示.執(zhí)行體的時間自動機(jī)模型包含兩個組件，一個為執(zhí)行體組件，另一個為裁決器組件.執(zhí)行體包含Start，Normal和Wash三個狀態(tài)，分別代表啟動，工作，清洗狀態(tài).該進(jìn)程和裁決器進(jìn)行交互，根據(jù)交互信息遷移狀態(tài)，并記錄正在清洗，正常工作的執(zhí)行體數(shù)量.

圖1 擬態(tài)防御系統(tǒng)架構(gòu)時間自動機(jī)模型

擬態(tài)架構(gòu)裁決器(Compare)時間自動機(jī)模型如圖1(c)所示.裁決器有五個狀態(tài)分別為Get_1、Get_n、Work、WashAll和Off狀態(tài).該模型描述裁決器與執(zhí)行體之間的交互，以及模擬裁決器向執(zhí)行體分發(fā)清洗關(guān)機(jī)信號，調(diào)度執(zhí)行體.

多個進(jìn)程之間需要進(jìn)行復(fù)合從而能夠并發(fā)執(zhí)行，我們采用PAT中的混合進(jìn)程符號||| 將三個執(zhí)行體與裁決器聯(lián)動，組合成一個完成的系統(tǒng)表述為：

System=|||z：{0..N-1}@Process(z)||| Compare

4 擬態(tài)防御架構(gòu)的判決策略建模

4.1 單選判決策略

單選判決是指裁決器在每個時間段或者程序段內(nèi)選擇一個執(zhí)行體作為主要執(zhí)行體，其結(jié)果作為正確結(jié)果輸出.在建模過程中，我們將系統(tǒng)抽象為兩個組件，一個為執(zhí)行體組件，另一個為裁決器組件.

#define N 3；/*定義三個執(zhí)行體*/

#define PRIMARY 0；/*0為主處理機(jī)序號*/

#define SUB 1；/*1為從處理機(jī)序號*/

#define SPARE 2；/*2為備處理機(jī)序號*/

varcount=0；/*執(zhí)行體對應(yīng)編號*/

varprocessSeq[N]=[PRIMARY，SUB，SPARE]；/*處理器序號*/

channelchange[N]；/*change信號用于裁決器向執(zhí)行體發(fā)送輪換主執(zhí)行體信號*/

單選判決執(zhí)行體(Process)時間自動機(jī)模型如圖2(a)所示.執(zhí)行體組件含有四個狀態(tài)Start、State_primary、State_sub和State_spare狀態(tài).執(zhí)行體接收裁決器分發(fā)的信號進(jìn)行狀態(tài)轉(zhuǎn)換.當(dāng)執(zhí)行體處于State_primary狀態(tài)時，裁決器將選用該執(zhí)行體的輸出作為處理結(jié)果.

圖2 單選判決策略時間自動機(jī)模型

單選判決裁決器(Compare)時間自動機(jī)模型如圖2(b)所示.裁決器包含三個狀態(tài)Start、Send和Turn.裁決器每隔十秒向執(zhí)行體分發(fā)狀態(tài)轉(zhuǎn)移信號，使每個執(zhí)行體在狀態(tài)State_primary、State_sub和State_spare中輪換.

組合成一個完成的系統(tǒng)表述為：

SingleChoiceSystem=|||z：{0..n-1}@P1(z)|||Compare

4.2 多選判決策略

多選判決采用多個執(zhí)行體共同處理同一個事務(wù)，輸出同一個事務(wù)的多個結(jié)果，裁決器對多個結(jié)果進(jìn)行比較，選擇占多數(shù)的結(jié)果作為正確結(jié)果并輸出，每一個輸入對應(yīng)一個輸出.當(dāng)多個執(zhí)行體的計算結(jié)果不一致時，我們加入置信度來標(biāo)識每個執(zhí)行體收到攻擊的概率.置信度越高，歷史收到攻擊的概率越低，結(jié)果的可信程度越高.在多個結(jié)果不同的情況下，裁決器將輸出置信度最高的結(jié)果作為正確結(jié)果.

#define NOTATTACK 1；/*定義未受攻擊值為1*/

#define TOWASH -2；/*safe值為-2時表示進(jìn)入清洗狀態(tài)，不參與判決*/

#define NORMAL 5；/*表示safe的初始值*/

vardealResult[3]=[NOTATTACK，

NOTATTACK，NOTATTACK]；/*執(zhí)行體中輸出*/

varresult[3]=[NOTATTACK，NOTATTACK，

NOTATTACK]；/*裁決器中輸出*/

varsafe[3]：{-6..8}=[NORMAL，NORMAL，

NORMAL]；/*置信度賦初值為5*/

vartemp1=0；/*輸入器計數(shù)器*/

vartemp2=0；/*裁決器計數(shù)器*/

varflag=1；/*標(biāo)記一次事務(wù)處理過程*/

channelattacker[3]；/*攻擊信道，用于模擬攻擊器向執(zhí)行體發(fā)送攻擊*/

channelwash；/*清洗信道，用于裁決器向執(zhí)行體發(fā)送清洗信號*/

channelout[3]；/*輸出信號，用于執(zhí)行體向裁決器發(fā)送對請求的處理結(jié)果*/

channeliner[3]；/*輸入信號，用于輸入器向執(zhí)行體發(fā)送請求信號*/

模型包括四個組件，執(zhí)行體、輸入器、裁決器和攻擊器.

多選判決執(zhí)行體(Process)時間自動機(jī)模型如圖3(a)所示.執(zhí)行體有State_wash、State_normal、State_normalSend和State_washSend四個狀態(tài).State_normal為初始狀態(tài)，當(dāng)執(zhí)行體處于該狀態(tài)時，可能會被攻擊，接收到attack信號表示被攻擊，執(zhí)行體中運(yùn)行結(jié)果由NOATTACK改變?yōu)楫?dāng)前組件序號+5，以模擬受攻擊的不同組件的不同輸出.State_normal接收到一個iner輸入信號時，遷移狀態(tài)至State_normalSend，并重置時鐘x.狀態(tài)State_normalSend向裁決器傳遞輸出結(jié)果，由變量result記錄裁決器中執(zhí)行體輸出結(jié)果，并遷移狀態(tài)至State_normal.當(dāng)State_normal的safe值為2時，接收一個wash信號，將遷移狀態(tài)至State_wash，同時safe值修改為-1，代表不參與多選判決.處于State_wash狀態(tài)時，清洗時間設(shè)置為10秒，清洗完畢后遷移至State_normal，safe值恢復(fù)默認(rèn)值，dealResult恢復(fù)為NOATTACK.當(dāng)執(zhí)行體處于State_wash狀態(tài)時，也可以接收輸入，遷移至State_washSend.State_washSend即時反饋結(jié)果至裁決器，同時遷移至State_wash.

多選判決輸入器(In)時間自動機(jī)模型如圖3(b)所示.輸入器包含兩個狀態(tài)，State_sendIn和State_send.模擬將消息同時發(fā)送給所有執(zhí)行體.

圖3 多選判決策略時間自動機(jī)模型

多選判決裁決器(Compare)時間自動機(jī)模型如圖3(c)所示.裁決器包含State_getIn、State_getIns和State_sendWash三個狀態(tài).裁決器判斷多個執(zhí)行體的輸出，選擇最有可能正確的輸出作為結(jié)果，同時判斷執(zhí)行體是否需要清洗，向需要清洗的執(zhí)行體發(fā)送清洗信號.模型算法一中首先判斷多個執(zhí)行體輸出是否相同，選擇相同數(shù)量最多的輸出作為處理結(jié)果，同時safe+1，其余執(zhí)行體safe-1；如果多個輸出都不相同，以置信度最高的執(zhí)行體輸出作為結(jié)果，置信度相同時隨機(jī)選擇執(zhí)行體輸出，輸出執(zhí)行體safe+1，其余執(zhí)行體safe-1.

多選判決攻擊器(Attacker)時間自動機(jī)模型如圖3(d)所示.攻擊器兩個狀態(tài)分別為Start和State_attack狀態(tài)，隨機(jī)向不同執(zhí)行體發(fā)送攻擊attcak信號后由Start遷移至State_attack.

組合成一個完成的系統(tǒng)表述為：

MultipleSelectionSystem=|||z：{0..2}@Process(z)|||Attacker|||Compare|||In

4.3 復(fù)合判決策略

復(fù)合判決策略標(biāo)識三個執(zhí)行體分別為主從備狀態(tài)，在一定時間內(nèi)直接以主處理機(jī)輸出結(jié)果作為標(biāo)準(zhǔn)結(jié)果.在一定時間之后，三個執(zhí)行體對同一個請求進(jìn)行計算，裁決器判決按照多選判決策略選擇判決輸出，同時更換執(zhí)行體主從備狀態(tài)；判斷執(zhí)行體是否受到攻擊，向受到攻擊的執(zhí)行體發(fā)送清洗信號.

#define N 3；/*定義三個執(zhí)行體*/

#define NORMAL 1；/*未受到攻擊時result的值*/

#define ABNORMAL -1；/*非正常狀態(tài)*/

#define PRIMARY 0；/*主執(zhí)行體序號*/

#define SUB 1；/*從執(zhí)行體序號*/

#define SPARE 2；/*備執(zhí)行體序號*/

#define ONATTACK0 7；/*0號處理機(jī)受到攻擊時result值為ONATTACK0*/

#define ONATTACK1 8；/* 1號處理機(jī)受到攻擊時result值為ONATTACK1*/

#define ONATTACK2 9；/* 2號處理機(jī)受到攻擊時result值為ONATTACK2*/

varnumber[N]=[PRIMARY，SUB，SPARE]；/*定義三個執(zhí)行體分別為主、從、備*/

varresult[N]=[NORMAL，NORMAL，NORMAL]；/*執(zhí)行體未受到攻擊之前輸出結(jié)果*/

varcount=0；/*change信號計數(shù)*/

channelchange[N]；/*裁決器向執(zhí)行體發(fā)送更換主從備狀態(tài)信號*/

channelattack[N]；/*攻擊器發(fā)送攻擊信號*/

channelwash；/*裁決器向執(zhí)行體發(fā)送清洗信號*/

復(fù)合判決執(zhí)行體時間(Process)自動機(jī)模型如圖4(a)所示.復(fù)合選擇執(zhí)行體包含三個組件攻擊器、執(zhí)行體和裁決器.執(zhí)行體包含兩個狀態(tài)State_normal和State_wash.State_normal可接收攻擊器攻擊attack，執(zhí)行體中的輸出結(jié)果值被改變.State_normal接收change信號，改變執(zhí)行體的主從備狀態(tài).State_normal接收裁決器發(fā)出的wash信號進(jìn)入State_wash.State_wash清洗完成后該處理機(jī)狀態(tài)轉(zhuǎn)變?yōu)閭涮幚頇C(jī)，同時遷移至State_normal.

復(fù)合判決攻擊器(Attacker)時間自動機(jī)模型如圖4(b)所示.攻擊器只有一個State_attack狀態(tài)，可隨機(jī)向不同執(zhí)行體發(fā)送攻擊attack信號.

復(fù)合判決裁決器(Compare)時間自動機(jī)模型如圖4(c)所示.裁決器模型包含兩個狀態(tài)State_send和State_wash狀態(tài).State_send為初始狀態(tài)，接收執(zhí)行體的輸入，當(dāng)收集全部的輸入后進(jìn)行判決，遷移狀態(tài)至State_wash，判斷需要清洗的執(zhí)行體并進(jìn)入清洗流程.然后重置temp1，重新記錄執(zhí)行體輸入，狀態(tài)遷移至State_send.算法二中首先比較主執(zhí)行體和從執(zhí)行體的輸出，當(dāng)兩者輸出相同時，主執(zhí)行體未受到攻擊，裁決器按照單選規(guī)則進(jìn)行輪換.當(dāng)兩者輸出不同，先將主執(zhí)行體于備執(zhí)行體的輸出進(jìn)行比較，如果兩者輸出相同，則使從執(zhí)行體進(jìn)入清洗狀態(tài)，備執(zhí)行體進(jìn)入從執(zhí)行體狀態(tài)，等清洗執(zhí)行體完成后，清洗執(zhí)行體進(jìn)入備執(zhí)行體狀態(tài)，之后系統(tǒng)按照單選規(guī)則進(jìn)行輪換；如果兩者輸出不同，則判斷從執(zhí)行體與備執(zhí)行體輸出，如果兩者輸出相同，主執(zhí)行體進(jìn)入清洗狀態(tài)，同時從、備執(zhí)行體分別進(jìn)入主，從執(zhí)行體狀態(tài)，當(dāng)執(zhí)行體完成清洗，進(jìn)入備狀態(tài)后，按照單選規(guī)則輪換；如果兩者輸出不同，直接按照單選規(guī)則輪換.

圖4 復(fù)合選擇策略時間自動機(jī)模型

組合成一個完成的系統(tǒng)表述為：

CompoundSelectionSystem=|||z：{0..N-1}@Process(z) |||Compare|||Attacker.

5 系統(tǒng)驗證

本章我們基于PAT工具對系統(tǒng)的各個機(jī)制進(jìn)行分析驗證，包括死鎖、可達(dá)性、時序邏輯驗證等.

5.1 擬態(tài)防御系統(tǒng)

#define ERRORSTATE1(worknumber+washnumber!=onNumber)；/*正常工作和正在清洗的執(zhí)行體數(shù)量和與總執(zhí)行體數(shù)量和不相等*/

#define ERRORSTATE 2(isOn== true&&

washnumber>0&&worknumber>0&&washnumber==onNumber)；/*系統(tǒng)運(yùn)行時，所有執(zhí)行體都處于清洗狀態(tài)*/#define HAVE_WASH_0(isWash[0]==1)；/*0號執(zhí)行體正在清洗*/

#define WASH_SUCCESS_0(isWash[0]==0)；/*0號執(zhí)行體清洗成功*/

擬態(tài)防御系統(tǒng)的屬性驗證：

1)#assert System reaches ERRORSTATE1；/*檢查系統(tǒng)是否能到達(dá)ERRORSTATE1狀態(tài)*/

實驗結(jié)果：否；運(yùn)行狀態(tài)數(shù)：50.

2)#assert System reaches ERRORSTATE2；/*檢查系統(tǒng)是否到達(dá)ERRORSTATE2狀態(tài)*/

實驗結(jié)果：否；運(yùn)行狀態(tài)數(shù)：50.

3)#assert System|=[]( HAVE_WASH_0 -> <> WASH_SUCCESS_0)；/*檢查0號執(zhí)行體是否總是能從清洗狀態(tài)恢復(fù)到正常狀態(tài)*/

實驗結(jié)果：否；運(yùn)行狀態(tài)數(shù)：47.反例路徑：init->start->ready->ready->ready->gotowork->wash->(wash->ok)*>.驗證結(jié)果分析：當(dāng)出現(xiàn)兩個需要清洗的執(zhí)行體時，由于另一個執(zhí)行體清洗完畢很快又出錯，導(dǎo)致不斷反復(fù)清洗該執(zhí)行體，導(dǎo)致0號執(zhí)行體長時間不能接收wash信號.這是一種極端情況，現(xiàn)實中可以采用簡單策略避免.

4)#assert System deadlockfree；/*檢查系統(tǒng)是否不會出現(xiàn)死鎖*/實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：50.

5)#assert System refines Ready；/*時間自動機(jī)Ready如圖5所示，其含義為系統(tǒng)啟動后，要么在10個單位時間內(nèi)至少有一個執(zhí)行體參與到系統(tǒng)運(yùn)行，要么在超過10個單位時間后系統(tǒng)啟動失敗*/實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：51.

圖5 Ready時間自動機(jī)模型

以上所有驗證運(yùn)行時間均小于1秒.通過以上驗證，說明該擬態(tài)防御框架能夠正常運(yùn)行，系統(tǒng)在10個單位時間內(nèi)啟動完畢，其中裁決器能夠保證至少存在一個執(zhí)行體處于工作狀態(tài)，發(fā)生錯誤的執(zhí)行體可通過清洗恢復(fù)至正常狀態(tài).唯一需要避免的極端情況是，多個執(zhí)行體同時發(fā)生錯誤的時候，裁決器只不斷發(fā)送清洗信號給同一個需要反復(fù)清洗的執(zhí)行體，導(dǎo)致其他執(zhí)行體一直無法進(jìn)入清洗狀態(tài).

5.2 單選判決策略

#define PRIMIARY_0 (processSeq[0]==PRIMARY)；/*0號執(zhí)行體作為主執(zhí)行體*/

#define SUB_1 (processSeq[1]==SUB)；/*1號執(zhí)行體作為從執(zhí)行體*/

#define SPARE_2 (processSeq[2]==SPARE)；/*2號執(zhí)行體作為備執(zhí)行體*/

單選判決策略屬性驗證：

1)#assert System |=[]<>PRIMIARY_0；/*檢查0號執(zhí)行體總是能到達(dá)主執(zhí)行體狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：28.

2)#assert System |=[]<>SUB_1；/*檢查1號執(zhí)行體總是能到達(dá)從執(zhí)行體狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：28.

#assert System |=[]<>SPARE_2；/*檢查2號執(zhí)行體總是能到達(dá)備執(zhí)行體狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：28.

3)#assert System deadlockfree；/*檢查系統(tǒng)是否不會出現(xiàn)死鎖*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：18.

以上所有驗證運(yùn)行時間均小于1秒.以上所有驗證表明了單選判決策略可用于擬態(tài)防御系統(tǒng)判決.系統(tǒng)運(yùn)行時，每個執(zhí)行體都會在一定時間內(nèi)在主、從、備狀態(tài)之間輪換，系統(tǒng)將主執(zhí)行體的運(yùn)行結(jié)果輸出.

5.3 多選判決策略

#define SAFE_TOOLOW(Safe[0]==2‖Safe[1]==2‖Safe[2]==2)；/*定義執(zhí)行體置信度到達(dá)2時安全度過低，需要清洗*/

#define ATTACKED(Dealresult[0]==5‖Dealresult[0]==6‖Dealresult[0]==7)；/*執(zhí)行體被攻擊*/

#define RECOVER_0(result[0]==NOTATTACK)；/*0號執(zhí)行體恢復(fù)正常*/

#define SAFE_LOW_0(safe[0]<5)；/*0號執(zhí)行體的置信度低于5 */

#define NEED_WASH_0(safe[0]==2)；/*0號執(zhí)行體需要清洗*/

#define ATTACKED_0(dealResult[0]!=1)；/*0號執(zhí)行體受到攻擊*/

#define WASH_0(safe[0]==-1)；/*0號執(zhí)行體清洗*/

#define NORMAL_0(safe[0]==NORMAL)；/*0號執(zhí)行體清洗成功*/

多選判決策略驗證：

1)#assert System reaches SAFE_TOOLOW；/*檢查執(zhí)行體能否到達(dá)置信度過低狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：314.

2)#assert System |=[](ATTACKED -><>

SAFE_TOOLOW)；/*檢查0號執(zhí)行體在被攻擊后是否總是能到達(dá)置信度為2的狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：694.

3)#assert System |=[](SAFE_LOW_0-> <> ATTACKED _0)；/*檢查當(dāng)0號執(zhí)行體置信度降低時是否一定是被攻擊了*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：579.

4)#assert System |=[](NEED_WASH_0-> <> WASH_0)；/*檢查執(zhí)行體能否從需要清洗狀態(tài)到達(dá)清洗狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：580.

5)#assert System deadlockfree；/*檢查系統(tǒng)是否不會出現(xiàn)死鎖*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：579.

6)#assert System refines Wash；/*時間自動機(jī)Wash如圖6所示，其含義為系統(tǒng)在受到攻擊后一定會進(jìn)入清洗狀態(tài)，并在10個單位時間內(nèi)清洗完畢*/

圖6 Wash時間自動機(jī)模型

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：584.

以上所有驗證運(yùn)行時間均小于1秒.通過以上所有驗證，說明多選判決可以用于擬態(tài)防御系統(tǒng)判決.系統(tǒng)運(yùn)行時，執(zhí)行體受到攻擊后置信度一定會慢慢降低，并在過低的情況下進(jìn)入清洗狀態(tài)，清洗過程將在10個單位時間內(nèi)完成.相比單選判決策略，多選判決在使系統(tǒng)安全性增加的同時也占用了更多的資源.

5.4 復(fù)合選擇

#define NUMBER0_ PRIMARY (number[0]==PRIMARY)；/*0號執(zhí)行體作為主執(zhí)行體*/

#define NUMBER1_ PRIMARY (number[1]==PRIMARY)；/*1號執(zhí)行體作為主執(zhí)行體*/

#define NUMBER0_WASH(number[0]==ABNORMAL)；/*0號執(zhí)行體清洗*/

#define NUMBER0_SPARE(number[0]==SPARE)；/*0號執(zhí)行體作為備執(zhí)行體*/

復(fù)合選擇驗證：

1)#assert System |=[]<>NUMBER0_PRIMARY；

/*檢查0號執(zhí)行體能否總是回到主執(zhí)行體狀態(tài)*/

實驗結(jié)果：否；運(yùn)行狀態(tài)數(shù)：182.反例路徑：init->change[0]->change[1]->change[2]->ratation->attack[1]->attack[0]->restart->change[0]->change[1]->change[2]->ratation->wash->washok->restart->change[0]->change[1]->change[2]->ratation->attack[2]->attack[1]->wash->washok->attack[0]->(restart->change[0]->change[1]->change[2]->ratation->wash->washok->attack[1]->restart->change[0]->change[1]->change[2]->ratation)*>.

0號執(zhí)行體不能總是回到主執(zhí)行體的原因是，在被頻繁攻擊的情況下，它處于不斷被重新清洗的狀態(tài)，因此不能回到主執(zhí)行體狀態(tài).

2)#assert System |=[](NUMBER0_WASH -> <> NUMBER0_SPARE)；/*每當(dāng)0號被清洗，它總是能清洗完畢回到備用狀態(tài)*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：332.

3)#assert System deadlockfree ；/*檢查系統(tǒng)是否不會出現(xiàn)死鎖*/

實驗結(jié)果：是；運(yùn)行狀態(tài)數(shù)：316.

以上所有驗證運(yùn)行時間均小于1秒.通過以上所有驗證，說明判決策略可用于擬態(tài)防御系統(tǒng)判決.在一段時間內(nèi)選擇一個執(zhí)行體作為主執(zhí)行體，將該執(zhí)行體的運(yùn)行結(jié)果作為輸出；一段時間后，比較各個執(zhí)行體的結(jié)果，輪換執(zhí)行體主、從、備狀態(tài).其中，系統(tǒng)可能會出現(xiàn)某個執(zhí)行體一直處于清洗、被攻擊的循環(huán)中而無法進(jìn)入主狀態(tài).復(fù)合判決策略平衡了單選判決和多選判決策略，系統(tǒng)可通過更改輪換時間間隔獲得需要的安全狀態(tài)和運(yùn)行速度.

6 結(jié)束語

將形式化建模和驗證方法應(yīng)用于安全防御系統(tǒng)構(gòu)建之前，驗證系統(tǒng)架構(gòu)和策略邏輯是否存在問題，從而能夠?qū)ο到y(tǒng)進(jìn)行改進(jìn)，以減少在實際搭建和使用過程中產(chǎn)生的問題，避免資源浪費(fèi).本文利用PAT工具，以時間自動機(jī)為形式化語言對新型擬態(tài)防御系統(tǒng)的框架和判決策略進(jìn)行建模、驗證和分析.驗證結(jié)果表明了擬態(tài)防御系統(tǒng)框架和判決策略的正確性和可行性.在未來工作方面，我們會進(jìn)一步將研究成果形成一套更為成熟的擬態(tài)安全防御系統(tǒng)的形式化驗證方法，應(yīng)用于系統(tǒng)目標(biāo)問題的驗證和評估.