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

Technical Note

Certifying the Absence of Buffer Overflows

  • September 2006
  • By Sagar Chaki , Scott Hissam
  • In this report, the authors present a technique for certifying the safety of buffer manipulations in C programs.
  • Software Assurance
  • Publisher: Software Engineering Institute
  • 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 like 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. This report also discusses the advantages and limitations of the approach with respect to today's 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.

  • Download

Cite This Report

SEI

Chaki, Sagar; & Hissam, Scott. Certifying the Absence of Buffer Overflows (CMU/SEI-2006-TN-030). Software Engineering Institute, Carnegie Mellon University, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7971

IEEE

Chaki. Sagar, and Hissam. Scott, "Certifying the Absence of Buffer Overflows," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2006-TN-030, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7971

APA

Chaki, Sagar., & Hissam, Scott. (2006). Certifying the Absence of Buffer Overflows (CMU/SEI-2006-TN-030). Retrieved December 20, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7971

CHI

Sagar Chaki, & Scott Hissam. Certifying the Absence of Buffer Overflows (CMU/SEI-2006-TN-030). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7971

MLA

Chaki, Sagar., & Hissam, Scott. 2006. Certifying the Absence of Buffer Overflows (Technical Report CMU/SEI-2006-TN-030). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7971