● 摘要
软件系统的安全性对一些关键部门，比如核心政府机构、银行等组织，有十分严格的要求。要保证系统和信息的安全，避免遭受恶意入侵，一个重要的问题是相关的程序必须经过严格的验证，特别是C语言程序中经常存在影响系统安全性的严重漏洞，利用工具有效地检测并消除出这些漏洞，可以大大提高系统的安全性。在代码安全漏洞静态检查方法中，传统工具多采用模式匹配、类型验证等算法，检查结果的误报率较高。模型检测工具虽然降低了误报率，但是在应用于缓冲区溢出安全漏洞的检查时，无法提取出漏洞模型，从而不能对该类错误进行检查。 本文提出了基于编译技术与模型检测相结合的缓冲区溢出漏洞检查方法。利用从GCC的抽象语法树中获得的信息，归纳出代码中可能出现安全漏洞的几种模式，完成对安全漏洞的建模，再结合模型检测工具BLAST，完成对该类漏洞的自动检查。该方法解决了模型检测工具BLAST不能应用于缓冲区溢出等安全漏洞检查的问题，将对代码漏洞的检测转化为对程序某个位置可达性的判定问题。本文使用这一方法设计并实现了一个可以精确检测C程序中缓冲区溢出漏洞的工具CodeAuditor。本文使用该工具对若干实际应用软件系统代码进行了测验。结果表明，使用该方法可以较精确地检测并定位出代码中的缓冲区溢出漏洞。