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

Time Automata Model and Verification of Mimic Defense System

网络空间拟态防御系统采用基于动态异构冗余架构的主动防御技术来提高网络系统安全性.然而,该过程目前缺乏抽象化理论研究,以及形式化的正确性验证、分析和评估.因此,本文首先以时间自动机为形式化建模语言,描述了拟态防御系统中冗余、清洗、选择判决等拟态机制和过程.然后,基于模型检测工具PAT,利用可达性、死锁、线性时序逻辑、语言包含等多种形式化验证方式对系统的不同方面进行了分析,最终得出了系统正确性和有效性相关的结论.

The mimetic defense system is based on dynamic heterogeneous redundant architecture to improve the security of the system.However,there is a lack of theoretical research on formal verification,analysis and evaluation.In this paper,we first use timed automata as a formal modeling language to describe the processes and mechanisms in the mimetic defense system,such as redundancy,cleaning and decision.Then,based on the model checking tool PAT,we analyze different aspects of the system by using various formal verification methods such as reachability,deadlockfree,model checking based on linear sequential logics and language inclusion checking.Finally,we drawa conclusion about the correctness and effectiveness of the system.