Covert Buffer Overflow Detector

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.

Find Us Here

Find us on Youtube  Find us on LinkedIn  Find us on twitter  Find us on Facebook

Share This Page

Share on Facebook  Send to your Twitter page  Save to del.ico.us  Save to LinkedIn  Digg this  Stumble this page.  Add to Technorati favorites  Save this page on your Google Home Page 

For more information

Contact Us

info@sei.cmu.edu

412-268-5800

Help us improve

Visitor feedback helps us continually improve our site.

Please tell us what you
think with this short
(< 5 minute) survey.