Precise Buffer Overflow Detection via Model Checking

Abstract

Buffer overflows are the source of a vast majority of vulnerabilities in today's 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 today's 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).

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2005
Accession Number
ADA633384

Entities

People

  • Sagar Chaki
  • Scott A. Hissam

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Cyber
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Assembly
  • Computer Programming
  • Computer Programs
  • Computers
  • Construction
  • Debugging
  • Detection
  • Detectors
  • Engineering
  • False Alarms
  • Intrusion Detection
  • Language
  • Programming Languages
  • Reliability
  • Software Development
  • Vulnerability
  • Warning Systems

Fields of Study

  • Computer science
  • Engineering

Readers

  • Parallel and Distributed Computing.
  • Software Engineering.
  • Systems Analysis and Design