TY - GEN
T1 - SMT-constrained symbolic execution engine for integer overflow detection in C code
AU - Muntean, Paul
AU - Rahman, Mustafizur
AU - Ibing, Andreas
AU - Eckert, Claudia
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/11/20
Y1 - 2015/11/20
N2 - Integer overflow errors in C programs are difficult to detect since the C language specification rules which govern how one can cast or promote integer types are not accompanied by any unambiguous set of formal rules. Thus, making it difficult for the programmer to understand and use the rules correctly causing vulnerabilities or costly errors. Although there are many static and dynamic tools used for integer overflow detection, the tools lack the capacity of efficiently filtering out false positives and false negatives. Better tools are needed to be constructed which are more precise in regard to bug detection and filtering out false positives. In this paper, we present an integer overflow checker which is based on precise modeling of C language semantics and symbolic function models. We developed our checker as an Eclipse plug-in and tested it on the open source C/C++ test case CWE-190 contained in the National Institute of Standards and Technology (NIST) Juliet test suite for C/C++. We ran our checker systematically on 2592 programs having in total 340 KLOC with a true positive rate of 95.49% for the contained C programs and with no false positives. We think our approach is effective to be applied in future to C++ programs as well, in order to detect other kinds of vulnerabilities related to integers.
AB - Integer overflow errors in C programs are difficult to detect since the C language specification rules which govern how one can cast or promote integer types are not accompanied by any unambiguous set of formal rules. Thus, making it difficult for the programmer to understand and use the rules correctly causing vulnerabilities or costly errors. Although there are many static and dynamic tools used for integer overflow detection, the tools lack the capacity of efficiently filtering out false positives and false negatives. Better tools are needed to be constructed which are more precise in regard to bug detection and filtering out false positives. In this paper, we present an integer overflow checker which is based on precise modeling of C language semantics and symbolic function models. We developed our checker as an Eclipse plug-in and tested it on the open source C/C++ test case CWE-190 contained in the National Institute of Standards and Technology (NIST) Juliet test suite for C/C++. We ran our checker systematically on 2592 programs having in total 340 KLOC with a true positive rate of 95.49% for the contained C programs and with no false positives. We think our approach is effective to be applied in future to C++ programs as well, in order to detect other kinds of vulnerabilities related to integers.
KW - context-sensitive analysis
KW - information security
KW - software vulnerability
UR - http://www.scopus.com/inward/record.url?scp=84962081974&partnerID=8YFLogxK
U2 - 10.1109/ISSA.2015.7335070
DO - 10.1109/ISSA.2015.7335070
M3 - Conference contribution
AN - SCOPUS:84962081974
T3 - 2015 Information Security for South Africa - Proceedings of the ISSA 2015 Conference
BT - 2015 Information Security for South Africa - Proceedings of the ISSA 2015 Conference
A2 - Eloff, Mariki M.
A2 - Flowerday, Steven
A2 - Venter, Hein S.
A2 - Loock, Marianne
A2 - Coetzee, Marijke
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - Annual Information Security for South Africa Conference, ISSA 2015
Y2 - 12 August 2015 through 13 August 2015
ER -