作战任务协同过程形式化表达方法

为实现联合作战条件下诸军兵种和各作战层级对作战任务的一致理解,更好组织和实施作战协同,从本体属性、相互间关系和所属行动3个方面对作战任务进行了形式化表达。基于形式化表达,提出了一种作战协同过程描述方法,该方法能够促进各级指挥员形成一致理解,有利于作战行动的组织实施。最后以美军伊拉克战争中的"5个同时攻击"为例,对作战任务协同过程形式化表达方法进行说明,验证了该方法的可行性和合理性。     

Casper/FDR和串空间在物联网通信协议中的形式化分析

通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析:用Casper/FDR对协议的有穷状态进行穷举验证,当发现协议漏洞时会自动给出攻击的迹,但是此方法会产生状态爆炸的问题;串空间方法正好可以解决状态爆炸问题,用串空间对协议的各种状态进行证明,但是如果发现了协议漏洞,该方法不能给出攻击者的迹。     

安全访问的轻量级完整性模型研究及实施*

对传统的完整性模型进行了分析,并对其完整性给予形式化描述.在此基础上,提出了轻量级的Clark-Wilson模型,并给出了其在安全增强操作系统SELinux中的实施.     

基于WPKI的移动通信端到端认证协议*

提出了一个在不同移动运营商中移动终端的相互认证协议.该协议利用WPKI机制,实现对双方公钥证书的认证.最后采用BAN逻辑,对协议的形式化分析表明协议达到了认证目标.     

形式化方法在机载电子硬件研制中的应用研究

详细设计规范是机载电子硬件适航性设计流程中的关键文档.通过对形式化方法特点分析,给出基于模型检验的设计规范提取步骤,以提高设计的正确性和完整性.以ARINC429总线传输模块设计为例,基于形式化方法完成正向设计过程.试验结果表明,基于形式化方法的设计流程能够有效帮助制定详细设计规范并在后期提高验证效率,进而缩减研制周期.     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

基于磁盘隐藏PE文件搜索的Bootkit检测方法

Bootkit通过将加载时间点提前到引导阶段,能够对其操作系统下的恶意行为进行隐藏以绕过多数安全软件。为此,对Bootkit的动态行为隐藏机制进行形式化建模,扩展协同隐藏机制以揭示Bootkit高隐蔽性,并且利用大部分Bootkit在磁盘上隐藏恶意PE文件的特点,设计并实现一种PE文件匹配算法。实验结果表明,该算法在磁盘隐蔽扇区中匹配特定的模式串以寻找潜在的恶意PE文件,在针对Bootkit样本的检测中取得了较好效果。     

基于新活动演算的SysML活动图形式化描述

针对Sys ML(Systems Modeling Language)活动图自身缺乏精确语义描述的不足,提出使用新活动演算来表示Sys ML活动图形式化语义的方法。通过分析Sys ML活动图的基本图符及其特点,对活动演算进行重新设计,增加了概率因子,并且在新活动演算中针对性地定义相应语法和操作语义。利用改进后的新活动演算实现了对Sys ML活动图的形式化描述,最后通过实例证明了所提出方法的有效性和实用性。     

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.     

安全攸关软件系统建模与验证专题前言

随着计算机技术应用的日益普及和不断深入,软件系统的规模和复杂性急剧增大,软件在越来越多的系统中成为主要的使能部件.在航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关的应用领域,软件系统失效将导致灾难性的后果,保障软件系统的质量成为迫切的需求和挑战.建模、分析与验证是保障软件系统质量的重要环节和手段.本专题收录的14篇论文反映了近年来我国学者在安全攸关软件系统建模与验证领域的