Accession Number:

ADA456867

Title:

Certifying the Absence of Buffer Overflows

Descriptive Note:

Final rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Personal Author(s):

Report Date:

2006-09-01

Pagination or Media Count:

39.0

Abstract:

Despite increased awareness and efforts to reduce buffer overflows, they continue to be the cause of most software vulnerabilities. In large part, these problems are due to the widespread use of unsafe library routines among programmers. For reasons of efficiency, such routines will continue to be used, even during the development of mission-critical and safety-critical software systems. Effective certification techniques are needed to ascertain whether unsafe routines are used in a safe manner. This report presents a technique for certifying the safety of buffer manipulations in C programs. The approach is based on two key ideas 1 using a certifying model checker to automatically verify that a buffer manipulation is safe, and 2 validating the resulting invariant and proving it with a decision procedure based on Boolean satisfiability. The report also discusses the advantages and limitations of the approach with respect to todays existing solutions for buffer-overflow detection. Experimental results are presented that position the technique favorably against other static overflow-detection tools and indicate that the procedure can complement and augment these tools from a purely verification perspective.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE