基于约束分析与模型检测的代码安全漏洞检测方法研究

被引：6

作者：

王雷

陈归

金茂忠

机构：

[1] 北京航空航天大学计算机学院

来源：

计算机研究与发展 | 2011年 / 48卷 / 09期

关键词：

约束分析; 模型检测; 安全漏洞; 程序切片; 静态分析;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

与传统的程序分析相比,模型检测具有较高的检测精度,但无法将其直接应用于缓冲区溢出、代码注入等安全漏洞的检测.为解决此问题,提出了基于约束分析与模型检测相结合的安全漏洞自动检测方法.首先,通过约束分析跟踪代码中缓冲区的信息,在涉及缓冲区操作的危险点生成相应的属性传递和属性约束语句,并将安全漏洞检测问题转化为模型检测方法可接受的可达性检测问题.然后,采用模型检测方法对安全漏洞的可达性进行判断.同时采用程序切片技术,以减少状态空间.对6个开源软件的检测结果表明,基于该方法实现的CodeAuditor原型系统发现了18个新漏洞,误报率为23%.对minicom的切片实验显示,检测性能有较大提高.

引用

页码：1659 / 1666

页数：8

共 3 条

[1] 结合搜索空间划分和抽象进行LTL模型检测 [J].

蒲飞 ;

张文辉 .

中国科学(E辑:信息科学), 2007, (12) :1504-1520

[2]

The software model checker B last[J] . Dirk Beyer,Thomas A. Henzinger,Ranjit Jhala,Rupak Majumdar.International Journal on Software Tools for Technology Transfer . 2007 (5)

[3]

CCured: type-safe retrofitting of legacy software[J] . George C. Necula,Jeremy Condit,Matthew Harren,Scott McPeak,Westley Weimer.ACM Transactions on Programming Languages and Systems (TOPLAS) . 2005 (3)

← 1 →