Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis

We describe a methodology and a tool for performing scalable bit-precise static analysis. The tool combines the scalable static analysis engine PREfix and the bit-precise efficient SMT solver Z3. Since 1999, PREfix has been used at Microsoft to analyze C/C++ production code. It relies on an efficient custom constraint solver, but addresses bit-level semantics only partially. On the other hand, the Satisfiability Modulo Theories solver Z3, developed at Microsoft Research, supports precise machine-level semantics for integer arithmetic operations.

The integration of PREfix with Z3 allows uncovering software bugs that could not previously be identified. Of particular importance are integer overflows. These typically arise when the programmer wrongly assumes mathematical integer semantics, and they are notorious causes of buffer overflow vulnerabilities in C/C++ programs.

We performed an experimental evaluation of our integration by running the modified version of PREfix on a large legacy code base for the next version of a Microsoft product. The experiments resulted in a number of bugs filed and fixed related to integer overflows. We also describe how we developed useful filters for avoiding false positives based on the comprehensive evaluation.