中文摘要：

为了增强对程序缓冲区溢出漏洞的检测,提出一种利用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.