● 摘要
在代码安全漏洞静态检查方法中，传统工具多采用模式匹配、类型验证等算法，检查结果的误报率相当高。当今的形式化验证工具例如模型检测工具虽然降低了误报率，但是在应用于缓冲区溢出、注入缺陷这类安全漏洞的检查时，无法提取出漏洞模型，从而不能对该类错误进行检查。本文首先提出了基于编译技术与模型检测相结合的缓冲区溢出漏洞检查方法。利用从GCC的抽象语法树中获得的信息，归纳出代码中可能出现安全漏洞的几种模式，完成对安全漏洞的建模，再结合模型检测工具BLAST，完成对该类漏洞的自动检查。该方法解决了模型检测工具BLAST不能应用于缓冲区溢出等安全漏洞检查的问题，使检查结果的精确性与传统工具相比得到提高。接着，为了解决模型检测工具在检查大型系统时的状态空间爆炸问题，也同时根据安全漏洞的特点，本文提出了程序切片与模型检测相结合的代码安全漏洞检查方法，并实现了C代码切片工具与模型检测工具的集成，可以对C代码安全漏洞进行自动检查。最后，本文选取实际系统minicom与corehttp对系统进行验证，试验结果表明，程序切片与模型检测相结合，在提高模型检测效率方面具有显著作用，本文在代码安全漏洞静态检查领域的研究，达到了预期的效果。