基于SMT求解器的整数溢出检测研究

摘要：

SMT求解器作为程序自动分析的组件,被越来越多的应用在安全漏洞研究领域.本文通过对整数安全问题和SMT求解器的分析,深入研究使用SMT求解器判断整数安全漏洞的方法.本文对目前已有的13种不同求解器特征进行了分析和总结,并针对整数溢出安全问题,重点对几种常用的SMT求解器(如Boolector、Z3、STP)的检测思路进行深入剖析.在此基础上,本文针对不直接支持整数溢出检测的SMT求解器STP,设计开发了一套相关检测接口。

关键词： 计算机安全漏洞 整数溢出 可满足性模理论求解器 检测技术

作者: 肖奇学 王欢 张知皦 史元春 陈渝

作者单位: 清华大学 计算机科学技术系,北京100088 北京工业大学 计算机学院,北京100124

会议类型: 国内会议

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

会议地点: 长沙

会议语种:中文

页码: 313-324

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