IntRepair: Informed Repairing of Integer Overflows

TL;DR

IntRepair is an automated static symbolic execution-based tool that detects and repairs integer overflows in C programs, demonstrating high effectiveness and efficiency on large real-world and synthesized codebases.

Contribution

The paper introduces IntRepair, a novel static symbolic execution technique for automatic detection and repair of integer overflows in C source code.

Findings

Successfully repaired over 2,000 real-world programs

Minimal code size increase (~1%) after repair

Repairs are over 10 times more efficient than manual fixes

Abstract

Integer overflows have threatened software applications for decades. Thus, in this paper, we propose a novel technique to provide automatic repairs of integer overflows in C source code. Our technique, based on static symbolic execution, fuses detection, repair generation and validation. This technique is implemented in a prototype named IntRepair. We applied IntRepair to 2,052C programs (approx. 1 million lines of code) contained in SAMATE's Juliet test suite and 50 synthesized programs that range up to 20KLOC. Our experimental results show that IntRepair is able to effectively detect integer overflows and successfully repair them, while only increasing the source code (LOC) and binary (Kb) size by around 1%, respectively. Further, we present the results of a user study with 30 participants which shows that IntRepair repairs are more than 10x efficient as compared to manually generated code repairs