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

摘要：

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

关键词：网络安全、拟态防御、时间自动机、模型检测

所属期刊栏目：41

分类号：TP302(计算技术、计算机技术)

资助基金：浙江省自然科学基金项目;国家自然科学基金项目

在线出版日期：2020-09-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1718-1724