擬態(tài)防御系統(tǒng)的時(shí)間自動(dòng)機(jī)模型和驗(yàn)證

王 婷，項(xiàng)露露，陳鐵明

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

1 引 言

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

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

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

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

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

2 時(shí)間自動(dòng)機(jī)介紹

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

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

表1 時(shí)間自動(dòng)機(jī)常用符號(hào)

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

擬態(tài)防御系統(tǒng)采用動(dòng)態(tài)異構(gòu)冗余結(jié)構(gòu)，以及清洗與重構(gòu)機(jī)制，將不確定性的干擾轉(zhuǎn)化為可控事件.動(dòng)態(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)接收到輸入請(qǐng)求；

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

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

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

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

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

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

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

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

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

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

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

channelok；/*清洗完成信號(hào)*/

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

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

channelwash；/*清洗信號(hào)*/

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

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

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

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

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

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

4.1 單選判決策略

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

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

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

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

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

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

varprocessSeq[N]=[PRIMARY，SUB，SPARE]；/*處理器序號(hào)*/

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

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

圖2 單選判決策略時(shí)間自動(dòng)機(jī)模型

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

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

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

4.2 多選判決策略

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

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

#define TOWASH -2；/*safe值為-2時(shí)表示進(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；/*輸入器計(jì)數(shù)器*/

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

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

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

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

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

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

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

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

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

圖3 多選判決策略時(shí)間自動(dòng)機(jī)模型

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

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

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

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

4.3 復(fù)合判決策略

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

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

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

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

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

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

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

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

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

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

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

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

varcount=0；/*change信號(hào)計(jì)數(shù)*/

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

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

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

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

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

復(fù)合判決裁決器(Compare)時(shí)間自動(dòng)機(jī)模型如圖4(c)所示.裁決器模型包含兩個(gè)狀態(tài)State_send和State_wash狀態(tài).State_send為初始狀態(tài)，接收?qǐng)?zhí)行體的輸入，當(dāng)收集全部的輸入后進(jìn)行判決，遷移狀態(tài)至State_wash，判斷需要清洗的執(zhí)行體并進(jìn)入清洗流程.然后重置temp1，重新記錄執(zhí)行體輸入，狀態(tài)遷移至State_send.算法二中首先比較主執(zhí)行體和從執(zhí)行體的輸出，當(dāng)兩者輸出相同時(shí)，主執(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)，同時(shí)從、備執(zhí)行體分別進(jìn)入主，從執(zhí)行體狀態(tài)，當(dāng)執(zhí)行體完成清洗，進(jìn)入備狀態(tài)后，按照單選規(guī)則輪換；如果兩者輸出不同，直接按照單選規(guī)則輪換.

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

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

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

5 系統(tǒng)驗(yàn)證

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

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)行時(shí)，所有執(zhí)行體都處于清洗狀態(tài)*/#define HAVE_WASH_0(isWash[0]==1)；/*0號(hào)執(zhí)行體正在清洗*/

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

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

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

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

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

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

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

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

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

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

圖5 Ready時(shí)間自動(dòng)機(jī)模型

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

5.2 單選判決策略

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

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

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

單選判決策略屬性驗(yàn)證：

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

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

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

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

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

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

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

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

以上所有驗(yàn)證運(yùn)行時(shí)間均小于1秒.以上所有驗(yàn)證表明了單選判決策略可用于擬態(tài)防御系統(tǒng)判決.系統(tǒng)運(yùn)行時(shí)，每個(gè)執(zhí)行體都會(huì)在一定時(shí)間內(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時(shí)安全度過(guò)低，需要清洗*/

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

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

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

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

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

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

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

多選判決策略驗(yàn)證：

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

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

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

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

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

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

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

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

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

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

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

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

圖6 Wash時(shí)間自動(dòng)機(jī)模型

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

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

5.4 復(fù)合選擇

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

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

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

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

復(fù)合選擇驗(yàn)證：

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

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

實(shí)驗(yàn)結(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號(hào)執(zhí)行體不能總是回到主執(zhí)行體的原因是，在被頻繁攻擊的情況下，它處于不斷被重新清洗的狀態(tài)，因此不能回到主執(zhí)行體狀態(tài).

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

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

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

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

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

6 結(jié)束語(yǔ)

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