动态异构冗余结构的拟态防御自动机模型

动态异构冗余结构是拟态防御技术的常用工程模型.然而，目前尚缺乏对该结构实施形式化分析的手段，因为该结构缺乏形式化建模方法.针对此问题，使用有穷状态自动机及其并行组合自动机为一些拟态攻防行为建立计算模型.首先，使用单个有穷状态自动机为单个执行体建模；其次，使用有穷状态自动机的并行组合为执行体组合建模；再次，修改状态迁移规则，得到可描述攻防行为的拟态防御自动机模型；最后，根据该自动机模型的状态条件，分析动态异构冗余结构上拟态攻防行为的安全性.此外，也可使用交替自动机为拟态攻防建模，并把安全性自动分析规约为交替自动机模型检测问题.

A Mimic Defense Automaton Model of Dynamic Heterogeneous Redundancy Structures

Up to now,the Dynamic Heterogeneous Redundancy (DHR) structure is a kind of important engineering model about the Mimic Defense (MD) technique.However,there is still a lack of way of formal analysis for DHR structures as there is no formal model available for a DHR structure.To address this problem,we use a Finite State Automaton (FSA) and its Parallel Automaton (PA) to establish a computing model for some attacks and mimic defenses.First,each FSA is employed to model each execution body,while there are a number of execution bodies in a DHR structure.Second,these FSAs are combined in parallel to model the combination of execution bodies.Third,one can get a model of MD automaton which can describe the attacks and MD actions,by modifying the state transition rules.Finally,one can analyse the attacks and MD actions on a DHR structure,according to the conditions of the PA states.Furthermore,we use an Alternating Finite Automaton (AFA) to model some attacks and MD actions.As a result,the automatic MD analysis problem is reduced to the solved AFA model checking problem.