Precise Buffer Overflow Detection via Model Checking
• SEI Report
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).
Cite This SEI Report
Chaki, S., & Hissam, S. (2005, December 1). Precise Buffer Overflow Detection via Model Checking. Retrieved August 19, 2026, from https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/.
@techreport{chaki_2005,
author={Chaki, Sagar and Hissam, Scott},
title={Precise Buffer Overflow Detection via Model Checking},
month={Dec},
year={2005},
institution={Software Engineering Institute, Carnegie Mellon University},
url={https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/},
note={Accessed: 2026-Aug-19}
}
Chaki, Sagar, and Scott Hissam. "Precise Buffer Overflow Detection via Model Checking." Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, December 1, 2005. https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/.
S. Chaki, and S. Hissam, "Precise Buffer Overflow Detection via Model Checking," Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, 1-Dec-2005 [Online]. Available: https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/. [Accessed: 19-Aug-2026].
Chaki, Sagar, and Scott Hissam. "Precise Buffer Overflow Detection via Model Checking." Software Engineering Institute, Carnegie Mellon University, Software Engineering Institute, 1 Dec. 2005. https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/. Accessed 19 Aug. 2026.
Chaki, Sagar; & Hissam, Scott. Precise Buffer Overflow Detection via Model Checking. Software Engineering Institute. 2005. https://www.sei.cmu.edu/library/precise-buffer-overflow-detection-via-model-checking/