Abstract：
SMT求解器作为程序自动分析的组件,被越来越多的应用在安全漏洞研究领域.本文通过对整数安全问题和SMT求解器的分析,深入研究使用SMT求解器判断整数安全漏洞的方法.本文对目前已有的13种不同求解器特征进行了分析和总结,并针对整数溢出安全问题,重点对几种常用的SMT求解器(如Boolector、Z3、STP)的检测思路进行深入剖析.在此基础上,本文针对不直接支持整数溢出检测的SMT求解器STP,设计开发了一套相关检测接口。
Keyword：
Reprint Author's Address：
Email：
Source ：
Year： 2014
Page： 313-324
Language： Chinese
Cited Count：
WoS CC Cited Count： 0
SCOPUS Cited Count：
ESI Highly Cited Papers on the List： 0 Unfold All
WanFang Cited Count： 1
Chinese Cited Count：
30 Days PV： 0
