基于模型检验的软件安全静态分析研究  

Research On Model Checking Based Software Security Static Analysis

作　　者：黄锦[1] 陈晓苏[1] 肖道举[1] 刘辉宇[1] 

机构地区：[1]华中科技大学计算机学院,湖北430074

出　　处：《微计算机信息》2007年第30期86-87,49,共3页Control & Automation

基　　金：国家863计划项目;项目号(2003AA712022)

摘　　要：软件安全静态分析是检测软件安全漏洞的一种手段。本文在总结现有的软件安全静态分析方法的基础上,将在硬件设计领域得到成功应用的模型检验方法引入到软件产品的检验中,给出了一种基于自动机理论的检测软件安全的模型检验方法,阐述了其原理和工作流程,并用实例进行了验证说明。Software security static analysis is an important way of software vulnerability checking. This paper summarizes the current static analysis methods and then imports the model checking method which has been successfully used in hardware design. Describes an automata theory based model checking method for software vulnerability checking. Then explains its principles and working flow, and at last validates it by using example.

关 键 词：静态分析 模型检验 漏洞挖掘 软件安全 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]