It is impossible today to escape the drumbeat of successful, malicious attacks reported in the media and on the Internet. As software developers, ensuring the integrity of our code requires constant vigilance and discipline. The situation we find software in today is similar to the pressure physical currency has been under for decades, but with one important exception: with currency, governments continually innovate new technology to make counterfeiting more difficult for criminals. But with software, criminals continually innovate new means to assault our code.
Of all the attacks directed at source code, integer overflows are one of the most pernicious. These potential exploits can easily lurk in your software because the conditions for triggering them are rarely, if ever, exercised by conventional test suites. These vulnerabilities are prime targets for hackers looking for points of infiltration.
Generally speaking, an integer overflows occurs when an unchecked add, subtract or multiply operation that looks innocuous to a programmer is pushed to its limits by special inputs crafted by a malicious user. When executed successfully, the result of the integer overflow can be a compromised system or denial of service. Because of the high cost of integer overflow exploits, programmers must find a way to pinpoint these vulnerabilities and eliminate them prior to the release of your code.
The defensive solution to avoid these vulnerabilities in code is to perform a bounds check on every value that is user-modifiable before using it in an arithmetic operation. However, for most applications, this would be an onerous task, as a user-supplied value can propagate across multiple function call boundaries to program points where the source of a value in an arithmetic operation is unclear.
Static analysis-based tools are useful aids in checking programs for these vulnerabilities. However, given the nature of the problem, the static analysis tool should be able to track values accurately across true inter-procedural paths. Recently, SAT-based analyses have demonstrated the capacity to perform the analysis required to detect integer overflow vulnerabilities, and programmers need to ensure code is protected. The bit-accurate representation of data and control flow using SAT constraints, coupled with SAT solvers, ensure that the tools report potential vulnerabilities while maintaining a small rate of false alarms.