Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

White Paper

Precise Buffer Overflow Detection via Model Checking

  • December 2005
  • By Sagar Chaki , Scott Hissam
  • In this paper, the authors present an automated overflow detection technique based on model checking and iterative refinement.
  • Publisher: Software Engineering Institute
  • 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).

  • Download