基于定理证明的软件脆弱性分析方法研究

项目名称： 基于定理证明的软件脆弱性分析方法研究

项目编号： No.61170070

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 曾庆凯

作者单位： 南京大学

项目金额： 55万元

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

中文关键词： 脆弱性分析；程序脆弱性语义；验证条件生成；启发式验证；脆弱性处理

英文摘要：

英文关键词： vulnerability analysis；vulnerability-related semantics；generating verification conditions；heuristically verifying conditions；handling vulnerabilities