基于UML行为模型的软件漏洞检测形式方法研究

摘要

随着计算机应用的不断发展,人们对软件的高可靠性要求越来越高。形式化方法是基于数学和逻辑语言的精确性规格、验证,保证软件高可靠性的重要方法。模型检测是一种形式化的验证技术,对该理论的研究和应用成为国内外近几年的热点问题。在计算机硬件、安全协议验证等领域,模型检测技术已经取得了丰硕的成果。
　　 为了实现软件的高可靠性,首先要对影响软件可靠性的软件漏洞进行学习和研究。论文不仅介绍了软件漏洞的分类而且对几种具体的漏洞进行了分析和定义。时序逻辑语言是模型检测的基础,为了掌握模型检测技术,对线性时序逻辑语言LTL进行了详细的描述,使用LTL对分析得到的漏洞定义进行了描述,从而得到了LTL公式。并且详细地介绍了模型检测工具SPIN。通过对SET购买过程协议使用SPIN进行验证,更深入的了解了该模型检测工具的建模语言promela以及属性定义语言LTL。
　　 模型检测技术应用在软件漏洞检测领域主要包括对需求分析和设计阶段的软件模型进行模型检测和对目标代码的模型检测。本课题选择了对软件开发初期阶段的设计模型进行形式化验证,可以及早的规避软件逻辑漏洞和安全漏洞,大大减少软件开发成本,缩短软件开发周期。并且对软件设计模型的形式化验证基于UML行为模型。UML建模是目前软件开发中最主要的可视化建模方法,而模型检测等形式化方法在建模过程中存在可视化困难,因此,将两种方法结合进行软件漏洞的检测,可以有效地减少形式化建模方面的难题。
　　 本课题主要研究在软件开发初期,对UML行为模型进行模型检测。首先,对UML行为模型转换为扩展层次自动机EHA模型的转换规则进行了描述,结合ATM工作流程的状态图模型,对该转换过程进行了实现。其次,给出了部分活动图的模型元素对应的EHA模型转换为promela模型的描述框架。同时,结合哲学家就餐问题的活动图模型的SPIN模型检测过程进行了详述,给出了死锁问题的验证结果。