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

A Mimic Defense Automaton Model of Dynamic Heterogeneous Redundancy Structures

作　　者：朱维军[1,2] 郭渊博 黄伯虎[4] ZHU Wei-jun;GUO Yuan-bo;HUANG Bo-hu(School of Information Engineering, Zhengzhou University, Zhengzhou, Henan 450001 , China;School of Electronics Engineering and Computer Science, Peking University, Beijing 100871 , China;Cryptography Engineering Institute, Information Engineering University, Zhengzhou , Henan 450001 , China;School of Computer Science, Xi'an University,Xi'an , Shaanxi 710071 , China)

机构地区：[1]郑州大学信息工程学院,河南郑州450001 [2]北京大学信息科学技术学院,北京100871 [3]信息工程大学密码工程学院,河南郑州450001 [4]西安电子科技大学计算机学院,陕西西安710071

出　　处：《电子学报》2019年第10期2025-2031,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.U1204608);国家重点研发计划(No.2016YFB0800100)

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

关 键 词：动态异构冗余 拟态防御 自动机 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP309[自动化与计算机技术—计算机科学与技术]