SMT-constrained symbolic execution engine for integer overflow detection in C code

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.