DocumentCode
690980
Title
SMT Solvers for Integer Overflows
Author
Qixue Xiao ; Yu Chen ; Hui Huang ; Lanhan Qi
Author_Institution
Dept. of Comput. Sci. & Technol., Tsinghua Univ., Beijing, China
fYear
2013
fDate
21-23 Sept. 2013
Firstpage
106
Lastpage
113
Abstract
SMT solver which is an automated program analysis technique is increasingly used by Vulnerability discovering platforms, especially in the integer security problems checking. An integer vulnerability discovering platform is mostly decided by the SMT solver. We have analyzed integer security problems and several SMT solvers, such as Boolector, Z3, STP and so on. We evaluated the ability of the SMT solvers in integer overflows checking from the view of vulnerability discovering. We also developed a set of APIs to check the integer overflows based on STP.
Keywords
computability; program diagnostics; security of data; API; SMT solvers; STP; automated program analysis technique; integer overflows; integer security problems checking; satisfiability modulo theories problem; vulnerability discovering platform; Cognition; Computer science; Educational institutions; Engines; Security; Software; Vectors; SMT solver; integer overflow; vulnerability;
fLanguage
English
Publisher
ieee
Conference_Titel
Instrumentation, Measurement, Computer, Communication and Control (IMCCC), 2013 Third International Conference on
Conference_Location
Shenyang
Type
conf
DOI
10.1109/IMCCC.2013.30
Filename
6840419
Link To Document