题目：代码安全漏洞静态检测工具的研究和实现

系统和信息的安全性在一些关键部门（比如核心政府机构、银行等）中，有着十分重要的意义。要保证系统和信息的安全，避免遭受恶意入侵，一个重要的问题是同系统和信息相关的软件程序必须经过严格的验证。特别是在C语言的程序中，经常存在影响系统安全性的严重漏洞。利用工具有效地检测并消除这一漏洞，可以大大提高系统的安全性。针对现有工具在代码安全漏洞检测上的不足，本文提出了一种利用模型检测技术对C语言代码中潜在的安全漏洞进行精确检测的方法。该方法首先利用控制流无关的属性分析技术和代码插装技术将安全漏洞检测问题转化为程序某个位置可达性的判定问题，再使用模型检测工具对可达性进行验证，验证为可达的路径就是存在安全漏洞的路径。使用这一方法，本文建立了一个可以精确检测C程序中缓冲区溢出漏洞的原型系统框架，该框架由前端和后端两部分组成，前端进行控制流无关的属性分析和代码插装，后端使用模型检测工具对可达性进行验证。此外，本文完成了该框架下的后端系统和部分前端系统的实现并结合缓冲区溢出漏洞的特点对该原型系统进行了两个级别的优化。使用该原型系统，本文对若干实际的软件系统代码进行了漏洞检测。结果表明，使用该方法的原型系统可以较为精确地检测并定位出代码中的漏洞。