摘要
为了增强对程序缓冲区溢出漏洞的检测,提出一种利用CCured和BLAST对C程序进行分析的检测方法。首先利用CCured对C语言源程序进行运行时检测的代码插桩;然后用BLAST提供的自定义安全属性语言对这些插桩代码进行相关约束描述;最后让BLAST根据约束描述文件对代码插桩后的程序进行模型检测,就可以尽可能地找出C语言程序中潜在的缓冲区溢出漏洞。
To enhance the buffer overflow detection for programs,this paper put forward a testing method based the analysis for C programs using CCured and BLAST.Firstly,the method used CCured to insert runtime detections into C program,and then described the constraints of the detections with the customized security-attribute language provided by BLAST.At last,according to the descriptions,BLAST could do model checking on the programs to find out the potential buffer overflow vulnerabilities in the programs as far as possible.
出处
《计算机应用研究》
CSCD
北大核心
2012年第2期617-620,共4页
Application Research of Computers
基金
国家自然科学基金可信软件重大研究计划资助项目(90818018
91018009)
关键词
CCured
BLAST
模型检测
缓冲区溢出
安全属性
CCured
BLAST（Barkeley lazy abstraction software verification tool）
model checking
buffer overflow
security attributes
