基于模型检测的软件安全分析研究

作     者：郭臣 

作者单位：北京交通大学 

学位级别：硕士

导师姓名：刘吉强

授予年度：2009年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：软件安全 模型检测 MOPS 有限状态自动机 安全属性 

摘      要：目前计算机系统和网络的安全性越来越受到软件质量和安全性的影响,并且软件安全性问题有越来越严重的趋势。软件安全的研究在世界范围逐渐受到重视,但目前并没有较成熟和实用的方法。模型检测是一种形式化验证技术,该技术在时序电路设计和通信协议设计的验证领域得到了广泛应用。但将模型检测技术应用于软件的验证和安全性分析正处于研究阶段。模型检测技术能够高效、自动化并且完全地对软件进行安全性分析,模型检测技术在软件的安全性分析方面有着良好的发展前景。本文分析了软件安全问题越来越严重的原因以及软件漏洞与软件安全性之间的联系。软件发展的互连性、可扩展性和复杂性趋势对软件安全问题产生了重大影响。而随着软件漏洞的增加,软件的安全性问题也必将增加。本文介绍了模型检测的基本概念、发展情况。针对模型检测的流程,介绍了模型检测过程中三个重要的步骤——系统建模、属性建模和模型检测算法——中所应用的技术。针对软件模型检测的特点,介绍了一些解决状态空间爆炸问题的技术和方法。分析了MOPS的形式化方法,针对MOPS的不足给出了改进设想。给出了一个设计安全属性FSA模型的一般性方法,按照这种方法,通过安全属性的提出,FSA状态的确定,以及FSA状态转移规则的确定,设计并实现了两个安全属性的FSA模型。在本文的最后将安全属性模型应用于实际的程序系统中,成功的发现了软件中存在的安全隐患,并对目标程序进行了安全性分析。