Accession Number:

ADA528648

Title:

COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification

Descriptive Note:

Final rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Personal Author(s):

Report Date:

2010-08-01

Pagination or Media Count:

35.0

Abstract:

Buffer overflows continue to be the source of a vast majority of software vulnerabilities. Solutions based on runtime checks incur performance overhead, and are inappropriate for safety-critical and mission-critical systems requiring static -- that is, prior to deployment -- guarantees. Thus, finding overflows statically and effectively remains an important challenge. This report presents COVERT, an automated framework aimed at finding buffer overflows in C programs using state-of-the-art software verification tools and techniques. Broadly, COVERT works in two phases INSTRUMENTATION and ANALYSIS. The INSTRUMENTATION phase is the core phase of COVERT. During INSTRUMENTATION, the target C program is instrumented such that buffer overflows are transformed to assertion violations. In the ANALYSIS phase, a static software verification tool is used to check for assertion violations in the instrumented code, and to generate error reports. COVERT was implemented and then evaluated on a set of benchmarks derived from real programs. For the ANALYSIS phase, experiments were conducted with three software verification tools -- BLAST, COPPER, and PANA. Results indicate that the COVERT framework is effective at reducing the number of false warnings, while remaining scalable.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE