中文摘要：

根据软件脆弱性分析的需求和技术发展，课题拟研究脆弱性程序语义、以及验证条件生成和启发式验证等方法，从而形成基于定理证明的脆弱性分析框架，以支持对包含复杂数据结构和数据类型的大型软件系统进行脆弱性分析。与模型检测分析方法单纯依赖脆弱性模型不同，本方法通过研究软件脆弱性形成原理，在脆弱性的程序语义、验证条件和验证证明等方面，不仅考虑脆弱性模型特征，而且引入软件的安全策略因素，使之既能检测脆弱性模型所表达的脆弱性，又能根据安全策略表达的约束检测未建模的脆弱性。通过研究、利用脆弱性的原理和特征，启发脆弱性验证过程的判定过程，结合语义推导、验证条件生成和反例生成等自动化技术，大幅度提高脆弱性分析过程的自动化程度。研究分析推理的优化方法，进一步改善分析验证过程。课题研究将在软件安全性分析工具和安全软件的设计开发等方面发挥积极的促进作用，并为软件脆弱性的分类和建模等研究提供参考和依据。

结论摘要：

本课题目标是研究基于定理证明的软件脆弱性分析方法，以提高软件的安全性。课题研究了脆弱性程序语义、验证条件生成、启发式验证和优化方法，重点在程序脆弱性语义、验证属性生成、脆弱性检测、启发式验证优化和脆弱性处理等方面开展了研究。研究了程序脆弱性语义，包括整数漏洞的建模、良性整数溢出的语义、并发线程的脆弱性描述、变量间的信息流分析等；研究了验证属性的提取方法，提出了程序循环不变式的改进生成方法；研究了各种脆弱性检测方法，包括检测IO2BO的动态跟踪技术、基于数据流分析的整数符号错误检测方法、基于信息流的整数漏洞验证方法、Web注入型脆弱性检测改进方法等；研究了启发式验证和优化方法，包括基于脆弱性知识的静态分析指导漏洞检测方法、基于脆弱性知识的检测输入评价方法、基于混合执行的漏洞检测方法、LTL属性分解方法等；探讨了各种脆弱性利用和处理方法，包括基于循环的代码复用攻击、基于硬件的代码复用攻击检测、脆弱性环境下内存保护、内核监控以及数据沙箱等方法。课题研究中，发表论文27篇，申请发明专利12项、获得授权3项，开发了多个具有较好应用前景的软件脆弱性检测和安全保护工具。