Automated Verification of Integer Overflow

TL;DR

This paper introduces an automated method for verifying integer overflow in software, providing a new specification mechanism and a prototype tool that successfully identified 43 bugs in existing verified programs.

Contribution

It presents a novel specification mechanism for integer overflow and an automated verification procedure, along with a prototype tool tested on real-world code.

Findings

Identified 43 integer overflow bugs in verified programs

Developed a prototype overflow checker tool

Validated the approach on a 14k LOC benchmark

Abstract

Integer overflow accounts for one of the major source of bugs in software. Verification systems typically assume a well defined underlying semantics for various integer operations and do not explicitly check for integer overflow in programs. In this paper we present a specification mechanism for expressing integer overflow. We develop an automated procedure for integer overflow checking during program verification. We have implemented a prototype integer overflow checker and tested it on a benchmark consisting of already verified programs (over 14k LOC). We have found 43 bugs in these programs due to integer overflow.