有界模型检查可执行文件的安全属性  

Bounded Model Checking Security Properties of Executables

作　　者：唐卓椿[1] 吴刚[1] 帅建梅[1] 孔德光[1] 

机构地区：[1]中国科学技术大学信息科学技术学院自动化系,安徽合肥230027

出　　处：《小型微型计算机系统》2008年第9期1674-1678,共5页Journal of Chinese Computer Systems

基　　金：安徽省优秀青年科技基金项目(04042046)资助;国家"八六三"高技术研究发展计划基金项目(2006AA01Z449)资助

摘　　要：引入模型检查方法对可执行文件进行脆弱性分析.对可执行文件形式化建模,采用有界模型检查技术验证可执行文件的安全属性,并在X86体系结构上开发了一个用于可执行文件的模型检查器.实验以内存泄漏和栈溢出漏洞为例,将其属性描述为线性时序逻辑公式,在可执行文件的状态迁移系统模型中验证公式是否能满足,实验结果表明对可执行文件的有界模型检查是一种有效的静态分析方法.Introduce model checking method to vulnerability analysis of exeeutables. This paper formally modeled binary executables, then adapted model checking technology to verify security properties of exeeutables, and developed a useful model checker. Memory leak and stack buffer overflow vulnerability as example properties, were abstracted to temporal logic formula, and then model checker verified whether the properties are satisfiable. The checking result as expected are sound and prove that bounded model checking is an effective static analysis method.

关 键 词：软件脆弱性 静态分析 有界模型检查 反汇编 线性时序逻辑 

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