模型检验技术在软件漏洞自动挖掘中的应用  

Application of model checking technology to automatically vulnerabilities finding in software

作　　者：刘晖[1] 张翀斌[2] 张晓敏[3] 

机构地区：[1]华中科技大学计算机科学与技术学院,湖北武汉430074 [2]中国信息安全产品测评认证中心,北京100089 [3]山东大学信息科学与工程学院,山东济南250100

出　　处：《华中科技大学学报（自然科学版）》2008年第2期70-73,共4页Journal of Huazhong University of Science and Technology(Natural Science Edition)

摘　　要：将在工业设计领域应用很成功的模型检验技术引入到信息技术软件产品的安全漏洞挖掘中,提出了针对源码的漏洞挖掘系统原型,以开放源代码的操作系统Linux为例,建立了特权释放和文件创建的安全属性模型,并举例加以验证.研究结果表明:该方法是一种自动化挖掘软件安全漏洞并证明漏洞存在性的形式化方法,对挖掘已经确认机理类型的漏洞非常有效.Model checking technology used widely in industrial designs was introduced into probable vulnerabilities finding in software. A system prototype is proposed to find vulnerabilities in source codes. Taking open-source operating system Linux as an example, a security property model was built for dropping privilege and creating files in this system, and this model was verified by various exampies. The results show that the proposed method is a formal means that could prove the existence of vulnerabilities and automatically discover security vulnerabilities in software.

关 键 词：软件 漏洞挖掘 模型检验 时序安全属性 有穷状态自动机 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]