安全协议验证模型的高效自动生成

为了能高效地利用模型检测技术对安全协议进行分析与验证,提高工作效率,提出了一种适用范围广,自动化程度及验证效率均较高的建模算法。开发了一个基于该建模算法"网络安全协议验证模型生成系统",该系统可高效地对安全协议进行分析与验证,系统在对攻击者建模时采用偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题。

基于SPIN的网络认证协议高效模型检测

为了有效地提高网络认证协议建模和验证的效率,基于模型检测方法提出一个通用的网络认证协议模型描述方法,结合模型检测工具SPIN可以方便地进行性质验证。通过一些模型的简化策略,不仅可以对不同协议进行高效建模,而且减小了模型的状态空间。与现有的文献相比,自动化程度较高,模型验证的效率较好。基于该方法,对PKM认证协议进行了模型检测,实验证明该模型分析验证方法的有效性,可用于其他网络认证协议的分析验证。

组合服务安全性检查方法研究

文章针对组合服务安全性检查方法未对服务进行分类处理的问题,将服务分为基本服务和扩展服务,基本服务采用进程元语言建模,借助线性时态逻辑表示基本服务的常规安全标准,通过SPIN模型检查基本服务符合常规安全标准的情况;扩展服务在开放工作流网络建模,借助FIONA模型检查服务、组合服务及其服务交互的安全性。通过智能家居药物管理系统的案例验证方法的正确性和效率性能,实验结果表明组合服务安全性检查方法是正确的和有效的。

ESpin:基于SPIN的Eclipse模型检测环境

信息化社会中人们对软件可信性的要求越来越高,传统的测试技术已经不能充分保证系统的安全性,基于模型的形式化验证技术成为解决此类问题的重要途径。SPIN作为典型的模型检测工具,在学术界和工业界都得到了广泛应用。在Eclipse平台上设计并实现了一个基于SPIN的易扩展的模型检测环境ESpin,通过一个优化了的代码分区算法和可迅速支持SPIN升级的文法分析器,构造了一个高效、易扩充的Promela编辑器。编辑器除了支持Promela的全部语法规则外,还提供了包括实时语法反馈、关键字高亮、大纲视图、代码折叠、代码提示、代码补全在内的多种功能,提高了复杂模型的建模效率。ESpin还为用户提供了多种运行模式和特有的向导、配置界面,简化了SPIN的操作过程。

UML模型检测方法的研究

统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法。首先对UML模型进行形式化描述,使用层次自动机来描述状态图,然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA,使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束,通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。