一种基于模型检验的缓冲区溢出检测方法

计算机科学 ›› 2012, Vol. 39 ›› Issue (Z6): 31-34.

一种基于模型检验的缓冲区溢出检测方法

张媛，于冠龙，李仁见

(65042部队沈阳110001);(海军驻沈阳地区航空军事代表室沈阳110031);(国防科学技术大学计算机学院长沙410073)

出版日期:2018-11-16 发布日期:2018-11-16

Buffer Overflow Detection Method Based on Model Checking

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 缓冲区溢出已经成为程序漏洞的主要根源之一。目前存在的缓冲区溢出检测方法或多或少地都存在着不足，从而限制了这些方法的实际应用。深入研究了当前缓冲区溢出检测方法的优缺点，对程序中的缓冲区及其相关操作进行建模，设计了一种基于模型检验的缓冲区溢出检测方法，并开发了一个原型工具来对该方法进行初步验证。在剖析缓冲区溢出基本原理的基础上，对程序中的缓冲区及其相关操作建立了理论模型，设计了一种基于模型检验的缓冲区溢出检测方法。最后，实现了一个原型工具来对该方法进行初步验证。

关键词: 缓冲区溢出，模型检验，人工分析

Abstract: Buffer overflow has become one of the major sources of program flaws. All of the existing solutions for detec- ting buffer overflow have serious drawbacks that hinder their wider adoption by practitioners. In this paper, we re- searched those solutions,analyzed their advantages and disadvantages. We presented a model for buffers in the program related operations. At last we designed a buffer overflow detecting approach based on model checking. A prototype was also developed to verify this method.

Key words: Buffer overflow, Model checking, Artificial analysis

张媛，于冠龙，李仁见. 一种基于模型检验的缓冲区溢出检测方法[J]. 计算机科学, 2012, 39(Z6): 31-34. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed