Accession Number:

ADA633384

Title:

Precise Buffer Overflow Detection via Model Checking

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Personal Author(s):

Report Date:

2005-12-01

Pagination or Media Count:

10.0

Abstract:

Buffer overflows are the source of a vast majority of vulnerabilities in todays software. Existing solution for detecting buffer overflow, either statically or dynamically, have serious drawbacks that hinder their wider adoption by practitioners. In this paper we present an automated overflow detection technique based on model checking and iterative refinement. We discuss advantages, and limitations, of our approach with respect to todays existing solutions. We also describe how our approach may be implemented on top of a model checking technology being developed at the Software Engineering Institute SEI.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE