Covert is a tool for finding buffer overflows in C programs. It is based on a combination of software model checking and static analysis. Covert can be used both from the command line and via an Eclipse-based graphical user interface. Both Linux and Windows platforms are supported.
Covert transforms buffer overflow problems into assertion violations and then uses a C analysis engine to find possible violations of these assertions. When a buffer overflow is detected, Covert also emits a program trace that exhibits the error. The transformation of buffer overflows into assertion violations is achieved via an extension of the CIL tool.
Unlike buffer overflow detection tools which employ static analysis, Covert uses software model checking based on predicate abstraction and iterative counterexample-driven refinement. Currently, Covert relies on the Copper model checker as its C backend analysis engine. Covert aims to emit few false warnings, while scaling to programs of realistic complexity. This report describes some of the technical details behind Covert.
Covert focuses primarily on buffer overflows caused by string manipulation routines, and is not suitable for finding arbitrary buffer overflows. At present, it is able to detect overflows caused by most common, but not all, string manipulation routines.