资料下载
×
基于模型检验的软件安全静态分析研究
消耗积分:5 |
格式:rar |
大小:128 |
2009-08-12
王飞云
分享资料个
软件安全静态分析是检测软件安全漏洞的一种手段。本文在总结现有的软件安全静
态分析方法的基础上，将在硬件设计领域得到成功应用的模型检验方法引入到软件产品的检验中，给出了一种基于自动机理论的检测软件安全的模型检验方法，阐述了其原理和工作流程，并用实例进行了验证说明。
随着计算机系统广泛应用，系统安全性越来越得到重视。软件安全漏洞是现代计算机
系统的毒瘤，多数恶意攻击都源自软件产品各种各样的漏洞。由于安全漏洞具有相当的隐蔽性，如何检测软件中可能存在的安全漏洞已成为信息安全关注的焦点。目前对于软件漏洞检测的研究有静态分析和动态检测两个分支，其中静态分析是主要的研究方向。静态分析通过对源代码的扫描和分析来检测漏洞，不需要改动源代码；动态检测则通过在程序执行期间对内存和堆栈的监测来检测漏洞，需要添加并重新编译源代码，增加了系统开销[1]。
模型检验是一种重要的自动化验证方法，它最早由 Clarke 和Emerson 提出[2]，主要通
过显式状态搜索或隐式不动点计算来验证系统的有穷状态和命题性质。模型检验在硬件设计领域的应用已经比较成熟，在软件安全静态分析上的应用也有研究人员进行了一些有意义的探索，如基于进程演算的模型检验方法[3]、基于程序时序逻辑的模型检验方法[4]等等。
软件安全静态分析的难点在于如何定义程序的安全属性以及如何制定对源代码的约束
条件。为了能够更好的描述程序的安全属性并运用某种形式化的方法对其进行验证，本文基于自动机的相关理论，通过将软件的源代码和安全属性分别建模为相应的自动机模型，探讨了一种检测软件安全的模型检验方法。
态分析方法的基础上，将在硬件设计领域得到成功应用的模型检验方法引入到软件产品的检验中，给出了一种基于自动机理论的检测软件安全的模型检验方法，阐述了其原理和工作流程，并用实例进行了验证说明。
随着计算机系统广泛应用，系统安全性越来越得到重视。软件安全漏洞是现代计算机
系统的毒瘤，多数恶意攻击都源自软件产品各种各样的漏洞。由于安全漏洞具有相当的隐蔽性，如何检测软件中可能存在的安全漏洞已成为信息安全关注的焦点。目前对于软件漏洞检测的研究有静态分析和动态检测两个分支，其中静态分析是主要的研究方向。静态分析通过对源代码的扫描和分析来检测漏洞，不需要改动源代码；动态检测则通过在程序执行期间对内存和堆栈的监测来检测漏洞，需要添加并重新编译源代码，增加了系统开销[1]。
模型检验是一种重要的自动化验证方法，它最早由 Clarke 和Emerson 提出[2]，主要通
过显式状态搜索或隐式不动点计算来验证系统的有穷状态和命题性质。模型检验在硬件设计领域的应用已经比较成熟，在软件安全静态分析上的应用也有研究人员进行了一些有意义的探索，如基于进程演算的模型检验方法[3]、基于程序时序逻辑的模型检验方法[4]等等。
软件安全静态分析的难点在于如何定义程序的安全属性以及如何制定对源代码的约束
条件。为了能够更好的描述程序的安全属性并运用某种形式化的方法对其进行验证，本文基于自动机的相关理论，通过将软件的源代码和安全属性分别建模为相应的自动机模型，探讨了一种检测软件安全的模型检验方法。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
