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

摘要

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.