search menu icon-carat-right cmu-wordmark

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

Technical Report
In this report, the authors present COVERT, an automated framework for finding buffer overflows in C programs using software verification tools and techniques.
Publisher

Software Engineering Institute

CMU/SEI Report Number
CMU/SEI-2010-TR-029
DOI (Digital Object Identifier)
10.1184/R1/6572828.v1

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 it 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.

Cite This Technical Report

Chaki, S., & Gurfinkel, A. (2010, August 1). COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification. (Technical Report CMU/SEI-2010-TR-029). Retrieved February 22, 2024, from https://doi.org/10.1184/R1/6572828.v1.

@techreport{chaki_2010,
author={Chaki, Sagar and Gurfinkel, Arie},
title={COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification},
month={Aug},
year={2010},
number={CMU/SEI-2010-TR-029},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6572828.v1},
note={Accessed: 2024-Feb-22}
}

Chaki, Sagar, and Arie Gurfinkel. "COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification." (CMU/SEI-2010-TR-029). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, August 1, 2010. https://doi.org/10.1184/R1/6572828.v1.

S. Chaki, and A. Gurfinkel, "COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Report CMU/SEI-2010-TR-029, 1-Aug-2010 [Online]. Available: https://doi.org/10.1184/R1/6572828.v1. [Accessed: 22-Feb-2024].

Chaki, Sagar, and Arie Gurfinkel. "COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification." (Technical Report CMU/SEI-2010-TR-029). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Aug. 2010. https://doi.org/10.1184/R1/6572828.v1. Accessed 22 Feb. 2024.

Chaki, Sagar; & Gurfinkel, Arie. COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification. CMU/SEI-2010-TR-029. Software Engineering Institute. 2010. https://doi.org/10.1184/R1/6572828.v1