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.
Descriptors:
Subject Categories:
- Computer Programming and Software