一种基于SAT的C程序缓冲区溢出漏洞检测技术

摘要：

本文给出一种基于SAT的C语言缓冲区溢出检测方法。该方法利用源代码变换技术,在程序源码中加入缓冲区属性刻画语句,使用断言刻画缓冲区溢出属性,然后借助SAT工具对断言进行检查。该方法以程序源代码作为输入,能够自动检测程序中包含的缓冲区溢出漏洞。

关键词： 缓冲区溢出 布尔可满足性 模型检验 源代码变换 信息安全

作者: 陈石坤 李舟军 邢建英

作者单位: 国防科技大学计算机学院 北京航空航天大学计算机学院

会议类型: 国内会议

会议名称: 第二届信息安全漏洞分析与风险评估大会

会议地点: 北京

会议语种:中文

页码: 268-277

在线出版日期: 2009-12-01（万方平台首次上网日期，不代表论文的发表时间）