拟态防御系统的时间自动机模型和验证

王 婷，项露露，陈铁明

(浙江工业大学 计算机科学与技术学院，杭州 310023)E-mail：tmchen@zjut.edu.cn

1 引 言

针对网络空间防御的被动局面，美国率先提出移动目标防御(MTD，moving target defense)思想[1].该技术通过提高网络灵活性、不断改变攻击面、减弱系统静态性，使攻击者难以定位攻击目标，减少被攻击的机会.国内研究者提出网络空间拟态防御(Cyber Mimic Defense，CMD)[2].该防御采用“动态、异构、冗余”机制，为受保护目标构建多种功能等效变体，组合构造搭建异构冗余池，动态选择安排变体并行运行，并采用仲裁机制来决定当前运行变量的结果是否正确，从而达到防御目的.

目前对安全防御行为过程的抽象化研究，难以对防御机制的可行性、安全性等进行评估和系统性分析.因此对网络空间拟态防御机制进行形式化规约，分析系统安全性成为当前研究的重点.

文献[3]中提出了使用贝叶斯网络的加权攻击路径建模技术模拟攻击路径.常用攻击树模型[4]等可对网络攻击进行建模，反映攻击与网络系统之间的状态关系.但是该模型侧重于对攻击成功特性的模型构建，很少考虑对防御行为的描述.单控制随机博弈[5]、贝叶斯随机博弈[6]、马尔可夫博弈模型[7]等经典博弈模型可用于防御系统的分析建模，但系统场景中的多状态、高动态使得模型难以描述，同时也无法描述多个组件的内在关系.文献[8]使用时间自动机构建EPC网络的入侵模型，包括入侵系统中网络环境实体、原子攻击和组合攻击的形式化描述，并展现了时间属性.文献[9]将SOC总线框架抽象为时间自动机网络，使用模型检查器UPPAAL验证SOC的安全属性.文献[10]通过时间自动机对RGMP-ROS系统进行形式化描述和分析以验证该系统的实时性.文献[11]使用UPPAAL对认知机器人的控制行为的正确性和实时性进行形式化分析和建模.文献[12]通过时间自动机对物联网网关安全系统的机密性、可用性、健壮性进行建模和验证.

综上所述，由于时间自动机是实时系统形式化建模和验证的主要手段，并且拟态防御系统模型除了行为过程以外也具有时间性要求，因此本文选用时间自动机对其进行建模和分析.模型描述了拟态防御系统的主动防御机制，以及清洗恢复、判决策略等逻辑过程，并基于PAT[13]模型检测工具对模型进行了自动化验证和分析，包括死锁检测、可达性验证、基于线性时序逻辑LTL的验证和语言包含[14]检查等多种方式.基于时间自动机理论的模型检测工具目前主要是UPPAAL[15]和PAT.PAT在UPPAAL所具备功能的基础上，增加了时间自动机的语言包含检查(将系统模型和待验证属性都用时间自动机表示，再使用自动化的语言包含检查算法)，能够验证跟时间有关的属性.因此本文采用了PAT工具对拟态防御系统进行建模和验证，并对系统正确性和有效性进行了分析.本文对验证属性的描述基于前面提到的多种方式，面向拟态防御系统中正常持续工作过程、攻击后清洗恢复、输出结果判定、执行体冗余和变换等关键方面的正确性.

本文第二节介绍时间自动机模型和工具；第三节介绍拟态防御系统架构并对拟态防御系统进行形式化建模；第四节给出拟态防御系统的判决策略、主动防御、清洗恢复等机制得时间自动机模型；第五节对系统需要满足的属性进行验证和分析.第六节对文章进行总结.

2 时间自动机介绍

时间自动机[16]由Alur和Dill于1994年首次提出，是配有一个或者多个时钟的有限状态机.将时间约束引入有限状态机能够更好地描述实时系统中的动作和状态，当满足时钟约束条件时，状态才发生转移，否则停留在当前状态；当满足状态上的状态不变式时，可以驻留当前状态，否则必须要离开当前状态.

时间自动机可以被视为一个六元组(L，L0，M，X，I，E)，其中L：状态集合；L0：初始状态集，L0L；M：事件集合；X：时钟变量集合；I：状态不变式；E：状态转移函数.E⊆L×M×φ(X)×2X×L为带时间约束的转移关系，包含自动机中的所有边.规则转换(l，m，x，z，l′)表示处于状态位置l的时，时钟满足约束条件x，系统可以发生事件m，从状态l转移到状态l′并完成z中的时间重置为0.表1介绍了利用PAT建模过程中需要用到的符号.

表1 时间自动机常用符号

3 拟态防御架构时间自动机描述

拟态防御系统采用动态异构冗余结构，以及清洗与重构机制，将不确定性的干扰转化为可控事件.动态异构冗余结构包括输入代理、执行体、异构组件、裁决器和以及裁决组件.清洗与重构可以使受到攻击的执行体恢复正常状态.拟态防御体系的架构[17]如图1(a)所示.

1. 系统接收到输入请求；

2. 输入代理向N个异构执行体分发请求；

3. N个异构执行体将计算结果反馈至裁决器；

4. 裁决器通过比较策略选择输出结果，同时判断异构执行体是否受到攻击，受到攻击的执行体需要进入清洗状态；

5. 裁决器分发关机信号.

我们使用时间自动机模拟抽象执行体和裁决器相互通信，以及系统清洗等流程.

#define N 10；/*含有十个个执行体*/

varworkNumber=0；/*开始后工作中执行体个数*/

varwashNumber=0；/*开始后清洗中执行体个数*/

varisWash[N]；/*为三个执行体标记是否处于清洗状态，数组下标为执行体序号，isWash[i]=0表示i号执行体不处于清洗状态，isWash[i]=1表示i号执行体处于清洗状态*/

varisOn=false；/*isOn=false时系统未正常启动，isOn=true时系统启动*/

varonNumber=0；/*启动成功执行体个数*/

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

channelready；/*执行体准备就绪信号*/

channelturnoff；/*裁决器向执行体发送关机信号*/

channelwash；/*清洗信号*/

拟态架构执行体(Process)时间自动机模型如图1(b)所示.执行体的时间自动机模型包含两个组件，一个为执行体组件，另一个为裁决器组件.执行体包含Start，Normal和Wash三个状态，分别代表启动，工作，清洗状态.该进程和裁决器进行交互，根据交互信息迁移状态，并记录正在清洗，正常工作的执行体数量.

图1 拟态防御系统架构时间自动机模型

拟态架构裁决器(Compare)时间自动机模型如图1(c)所示.裁决器有五个状态分别为Get_1、Get_n、Work、WashAll和Off状态.该模型描述裁决器与执行体之间的交互，以及模拟裁决器向执行体分发清洗关机信号，调度执行体.

多个进程之间需要进行复合从而能够并发执行，我们采用PAT中的混合进程符号||| 将三个执行体与裁决器联动，组合成一个完成的系统表述为：

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

4 拟态防御架构的判决策略建模

4.1 单选判决策略

单选判决是指裁决器在每个时间段或者程序段内选择一个执行体作为主要执行体，其结果作为正确结果输出.在建模过程中，我们将系统抽象为两个组件，一个为执行体组件，另一个为裁决器组件.

#define N 3；/*定义三个执行体*/

#define PRIMARY 0；/*0为主处理机序号*/

#define SUB 1；/*1为从处理机序号*/

#define SPARE 2；/*2为备处理机序号*/

varcount=0；/*执行体对应编号*/

varprocessSeq[N]=[PRIMARY，SUB，SPARE]；/*处理器序号*/

channelchange[N]；/*change信号用于裁决器向执行体发送轮换主执行体信号*/

单选判决执行体(Process)时间自动机模型如图2(a)所示.执行体组件含有四个状态Start、State_primary、State_sub和State_spare状态.执行体接收裁决器分发的信号进行状态转换.当执行体处于State_primary状态时，裁决器将选用该执行体的输出作为处理结果.

图2 单选判决策略时间自动机模型

单选判决裁决器(Compare)时间自动机模型如图2(b)所示.裁决器包含三个状态Start、Send和Turn.裁决器每隔十秒向执行体分发状态转移信号，使每个执行体在状态State_primary、State_sub和State_spare中轮换.

组合成一个完成的系统表述为：

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

4.2 多选判决策略

多选判决采用多个执行体共同处理同一个事务，输出同一个事务的多个结果，裁决器对多个结果进行比较，选择占多数的结果作为正确结果并输出，每一个输入对应一个输出.当多个执行体的计算结果不一致时，我们加入置信度来标识每个执行体收到攻击的概率.置信度越高，历史收到攻击的概率越低，结果的可信程度越高.在多个结果不同的情况下，裁决器将输出置信度最高的结果作为正确结果.

#define NOTATTACK 1；/*定义未受攻击值为1*/

#define TOWASH -2；/*safe值为-2时表示进入清洗状态，不参与判决*/

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

vardealResult[3]=[NOTATTACK，

NOTATTACK，NOTATTACK]；/*执行体中输出*/

varresult[3]=[NOTATTACK，NOTATTACK，

NOTATTACK]；/*裁决器中输出*/

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

NORMAL]；/*置信度赋初值为5*/

vartemp1=0；/*输入器计数器*/

vartemp2=0；/*裁决器计数器*/

varflag=1；/*标记一次事务处理过程*/

channelattacker[3]；/*攻击信道，用于模拟攻击器向执行体发送攻击*/

channelwash；/*清洗信道，用于裁决器向执行体发送清洗信号*/

channelout[3]；/*输出信号，用于执行体向裁决器发送对请求的处理结果*/

channeliner[3]；/*输入信号，用于输入器向执行体发送请求信号*/

模型包括四个组件，执行体、输入器、裁决器和攻击器.

多选判决执行体(Process)时间自动机模型如图3(a)所示.执行体有State_wash、State_normal、State_normalSend和State_washSend四个状态.State_normal为初始状态，当执行体处于该状态时，可能会被攻击，接收到attack信号表示被攻击，执行体中运行结果由NOATTACK改变为当前组件序号+5，以模拟受攻击的不同组件的不同输出.State_normal接收到一个iner输入信号时，迁移状态至State_normalSend，并重置时钟x.状态State_normalSend向裁决器传递输出结果，由变量result记录裁决器中执行体输出结果，并迁移状态至State_normal.当State_normal的safe值为2时，接收一个wash信号，将迁移状态至State_wash，同时safe值修改为-1，代表不参与多选判决.处于State_wash状态时，清洗时间设置为10秒，清洗完毕后迁移至State_normal，safe值恢复默认值，dealResult恢复为NOATTACK.当执行体处于State_wash状态时，也可以接收输入，迁移至State_washSend.State_washSend即时反馈结果至裁决器，同时迁移至State_wash.

多选判决输入器(In)时间自动机模型如图3(b)所示.输入器包含两个状态，State_sendIn和State_send.模拟将消息同时发送给所有执行体.

图3 多选判决策略时间自动机模型

多选判决裁决器(Compare)时间自动机模型如图3(c)所示.裁决器包含State_getIn、State_getIns和State_sendWash三个状态.裁决器判断多个执行体的输出，选择最有可能正确的输出作为结果，同时判断执行体是否需要清洗，向需要清洗的执行体发送清洗信号.模型算法一中首先判断多个执行体输出是否相同，选择相同数量最多的输出作为处理结果，同时safe+1，其余执行体safe-1；如果多个输出都不相同，以置信度最高的执行体输出作为结果，置信度相同时随机选择执行体输出，输出执行体safe+1，其余执行体safe-1.

多选判决攻击器(Attacker)时间自动机模型如图3(d)所示.攻击器两个状态分别为Start和State_attack状态，随机向不同执行体发送攻击attcak信号后由Start迁移至State_attack.

组合成一个完成的系统表述为：

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

4.3 复合判决策略

复合判决策略标识三个执行体分别为主从备状态，在一定时间内直接以主处理机输出结果作为标准结果.在一定时间之后，三个执行体对同一个请求进行计算，裁决器判决按照多选判决策略选择判决输出，同时更换执行体主从备状态；判断执行体是否受到攻击，向受到攻击的执行体发送清洗信号.

#define N 3；/*定义三个执行体*/

#define NORMAL 1；/*未受到攻击时result的值*/

#define ABNORMAL -1；/*非正常状态*/

#define PRIMARY 0；/*主执行体序号*/

#define SUB 1；/*从执行体序号*/

#define SPARE 2；/*备执行体序号*/

#define ONATTACK0 7；/*0号处理机受到攻击时result值为ONATTACK0*/

#define ONATTACK1 8；/* 1号处理机受到攻击时result值为ONATTACK1*/

#define ONATTACK2 9；/* 2号处理机受到攻击时result值为ONATTACK2*/

varnumber[N]=[PRIMARY，SUB，SPARE]；/*定义三个执行体分别为主、从、备*/

varresult[N]=[NORMAL，NORMAL，NORMAL]；/*执行体未受到攻击之前输出结果*/

varcount=0；/*change信号计数*/

channelchange[N]；/*裁决器向执行体发送更换主从备状态信号*/

channelattack[N]；/*攻击器发送攻击信号*/

channelwash；/*裁决器向执行体发送清洗信号*/

复合判决执行体时间(Process)自动机模型如图4(a)所示.复合选择执行体包含三个组件攻击器、执行体和裁决器.执行体包含两个状态State_normal和State_wash.State_normal可接收攻击器攻击attack，执行体中的输出结果值被改变.State_normal接收change信号，改变执行体的主从备状态.State_normal接收裁决器发出的wash信号进入State_wash.State_wash清洗完成后该处理机状态转变为备处理机，同时迁移至State_normal.

复合判决攻击器(Attacker)时间自动机模型如图4(b)所示.攻击器只有一个State_attack状态，可随机向不同执行体发送攻击attack信号.

复合判决裁决器(Compare)时间自动机模型如图4(c)所示.裁决器模型包含两个状态State_send和State_wash状态.State_send为初始状态，接收执行体的输入，当收集全部的输入后进行判决，迁移状态至State_wash，判断需要清洗的执行体并进入清洗流程.然后重置temp1，重新记录执行体输入，状态迁移至State_send.算法二中首先比较主执行体和从执行体的输出，当两者输出相同时，主执行体未受到攻击，裁决器按照单选规则进行轮换.当两者输出不同，先将主执行体于备执行体的输出进行比较，如果两者输出相同，则使从执行体进入清洗状态，备执行体进入从执行体状态，等清洗执行体完成后，清洗执行体进入备执行体状态，之后系统按照单选规则进行轮换；如果两者输出不同，则判断从执行体与备执行体输出，如果两者输出相同，主执行体进入清洗状态，同时从、备执行体分别进入主，从执行体状态，当执行体完成清洗，进入备状态后，按照单选规则轮换；如果两者输出不同，直接按照单选规则轮换.

图4 复合选择策略时间自动机模型

组合成一个完成的系统表述为：

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

5 系统验证

本章我们基于PAT工具对系统的各个机制进行分析验证，包括死锁、可达性、时序逻辑验证等.

5.1 拟态防御系统

#define ERRORSTATE1(worknumber+washnumber!=onNumber)；/*正常工作和正在清洗的执行体数量和与总执行体数量和不相等*/

#define ERRORSTATE 2(isOn== true&&

washnumber>0&&worknumber>0&&washnumber==onNumber)；/*系统运行时，所有执行体都处于清洗状态*/#define HAVE_WASH_0(isWash[0]==1)；/*0号执行体正在清洗*/

#define WASH_SUCCESS_0(isWash[0]==0)；/*0号执行体清洗成功*/

拟态防御系统的属性验证：

1)#assert System reaches ERRORSTATE1；/*检查系统是否能到达ERRORSTATE1状态*/

实验结果：否；运行状态数：50.

2)#assert System reaches ERRORSTATE2；/*检查系统是否到达ERRORSTATE2状态*/

实验结果：否；运行状态数：50.

3)#assert System|=[]( HAVE_WASH_0 -> <> WASH_SUCCESS_0)；/*检查0号执行体是否总是能从清洗状态恢复到正常状态*/

实验结果：否；运行状态数：47.反例路径：init->start->ready->ready->ready->gotowork->wash->(wash->ok)*>.验证结果分析：当出现两个需要清洗的执行体时，由于另一个执行体清洗完毕很快又出错，导致不断反复清洗该执行体，导致0号执行体长时间不能接收wash信号.这是一种极端情况，现实中可以采用简单策略避免.

4)#assert System deadlockfree；/*检查系统是否不会出现死锁*/实验结果：是；运行状态数：50.

5)#assert System refines Ready；/*时间自动机Ready如图5所示，其含义为系统启动后，要么在10个单位时间内至少有一个执行体参与到系统运行，要么在超过10个单位时间后系统启动失败*/实验结果：是；运行状态数：51.

图5 Ready时间自动机模型

以上所有验证运行时间均小于1秒.通过以上验证，说明该拟态防御框架能够正常运行，系统在10个单位时间内启动完毕，其中裁决器能够保证至少存在一个执行体处于工作状态，发生错误的执行体可通过清洗恢复至正常状态.唯一需要避免的极端情况是，多个执行体同时发生错误的时候，裁决器只不断发送清洗信号给同一个需要反复清洗的执行体，导致其他执行体一直无法进入清洗状态.

5.2 单选判决策略

#define PRIMIARY_0 (processSeq[0]==PRIMARY)；/*0号执行体作为主执行体*/

#define SUB_1 (processSeq[1]==SUB)；/*1号执行体作为从执行体*/

#define SPARE_2 (processSeq[2]==SPARE)；/*2号执行体作为备执行体*/

单选判决策略属性验证：

1)#assert System |=[]<>PRIMIARY_0；/*检查0号执行体总是能到达主执行体状态*/

实验结果：是；运行状态数：28.

2)#assert System |=[]<>SUB_1；/*检查1号执行体总是能到达从执行体状态*/

实验结果：是；运行状态数：28.

#assert System |=[]<>SPARE_2；/*检查2号执行体总是能到达备执行体状态*/

实验结果：是；运行状态数：28.

3)#assert System deadlockfree；/*检查系统是否不会出现死锁*/

实验结果：是；运行状态数：18.

以上所有验证运行时间均小于1秒.以上所有验证表明了单选判决策略可用于拟态防御系统判决.系统运行时，每个执行体都会在一定时间内在主、从、备状态之间轮换，系统将主执行体的运行结果输出.

5.3 多选判决策略

#define SAFE_TOOLOW(Safe[0]==2‖Safe[1]==2‖Safe[2]==2)；/*定义执行体置信度到达2时安全度过低，需要清洗*/

#define ATTACKED(Dealresult[0]==5‖Dealresult[0]==6‖Dealresult[0]==7)；/*执行体被攻击*/

#define RECOVER_0(result[0]==NOTATTACK)；/*0号执行体恢复正常*/

#define SAFE_LOW_0(safe[0]<5)；/*0号执行体的置信度低于5 */

#define NEED_WASH_0(safe[0]==2)；/*0号执行体需要清洗*/

#define ATTACKED_0(dealResult[0]!=1)；/*0号执行体受到攻击*/

#define WASH_0(safe[0]==-1)；/*0号执行体清洗*/

#define NORMAL_0(safe[0]==NORMAL)；/*0号执行体清洗成功*/

多选判决策略验证：

1)#assert System reaches SAFE_TOOLOW；/*检查执行体能否到达置信度过低状态*/

实验结果：是；运行状态数：314.

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

SAFE_TOOLOW)；/*检查0号执行体在被攻击后是否总是能到达置信度为2的状态*/

实验结果：是；运行状态数：694.

3)#assert System |=[](SAFE_LOW_0-> <> ATTACKED _0)；/*检查当0号执行体置信度降低时是否一定是被攻击了*/

实验结果：是；运行状态数：579.

4)#assert System |=[](NEED_WASH_0-> <> WASH_0)；/*检查执行体能否从需要清洗状态到达清洗状态*/

实验结果：是；运行状态数：580.

5)#assert System deadlockfree；/*检查系统是否不会出现死锁*/

实验结果：是；运行状态数：579.

6)#assert System refines Wash；/*时间自动机Wash如图6所示，其含义为系统在受到攻击后一定会进入清洗状态，并在10个单位时间内清洗完毕*/

图6 Wash时间自动机模型

实验结果：是；运行状态数：584.

以上所有验证运行时间均小于1秒.通过以上所有验证，说明多选判决可以用于拟态防御系统判决.系统运行时，执行体受到攻击后置信度一定会慢慢降低，并在过低的情况下进入清洗状态，清洗过程将在10个单位时间内完成.相比单选判决策略，多选判决在使系统安全性增加的同时也占用了更多的资源.

5.4 复合选择

#define NUMBER0_ PRIMARY (number[0]==PRIMARY)；/*0号执行体作为主执行体*/

#define NUMBER1_ PRIMARY (number[1]==PRIMARY)；/*1号执行体作为主执行体*/

#define NUMBER0_WASH(number[0]==ABNORMAL)；/*0号执行体清洗*/

#define NUMBER0_SPARE(number[0]==SPARE)；/*0号执行体作为备执行体*/

复合选择验证：

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

/*检查0号执行体能否总是回到主执行体状态*/

实验结果：否；运行状态数：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号执行体不能总是回到主执行体的原因是，在被频繁攻击的情况下，它处于不断被重新清洗的状态，因此不能回到主执行体状态.

2)#assert System |=[](NUMBER0_WASH -> <> NUMBER0_SPARE)；/*每当0号被清洗，它总是能清洗完毕回到备用状态*/

实验结果：是；运行状态数：332.

3)#assert System deadlockfree ；/*检查系统是否不会出现死锁*/

实验结果：是；运行状态数：316.

以上所有验证运行时间均小于1秒.通过以上所有验证，说明判决策略可用于拟态防御系统判决.在一段时间内选择一个执行体作为主执行体，将该执行体的运行结果作为输出；一段时间后，比较各个执行体的结果，轮换执行体主、从、备状态.其中，系统可能会出现某个执行体一直处于清洗、被攻击的循环中而无法进入主状态.复合判决策略平衡了单选判决和多选判决策略，系统可通过更改轮换时间间隔获得需要的安全状态和运行速度.

6 结束语

将形式化建模和验证方法应用于安全防御系统构建之前，验证系统架构和策略逻辑是否存在问题，从而能够对系统进行改进，以减少在实际搭建和使用过程中产生的问题，避免资源浪费.本文利用PAT工具，以时间自动机为形式化语言对新型拟态防御系统的框架和判决策略进行建模、验证和分析.验证结果表明了拟态防御系统框架和判决策略的正确性和可行性.在未来工作方面，我们会进一步将研究成果形成一套更为成熟的拟态安全防御系统的形式化验证方法，应用于系统目标问题的验证和评估.