一种基于契约的安全分析方法的研究与实现

摘要

本文针对C/C++程序安全漏洞，提出并实现了一种基于契约的安全分析方法。该方法采用自下而上分析遍历程序中的函数体，将跨过程分析转变为过程内分析；提供安全规则描述方法，使得用户可以扩展安全规则；通过为变量和函数附加契约以记录其前置和后置条件，并在程序分析的过程中按照规则更新契约，使得在程序分析时自动进行安全检查。该方法具有代价小，灵活性强的特点，可以用来检查程序中指针非法引用、函数调用时实参或全局变量的状态不合法、内存泄漏及其他资源泄漏等安全漏洞。

目录

文摘

英文文摘

声明

第一章绪论

1.1研究背景

1.2课题解决方案

1.3本文主要工作

第二章自下而上分析方法中的契约

2.1自下而上分析

2.2变量契约与函数契约

2.3契约信息

第三章基于契约的安全分析方法的设计

3.1安全判定规则

3.2契约更新规则

3.3基于契约的安全分析算法

第四章基于契约的安全分析方法的实现

4.1程序框架

4.2配置文件格式定义模块

4.2.1配置文件格式定义

4.2.2系统默认契约信息

4.3契约信息模块

4.3.1契约信息的定义

4.3.2契约信息的提取

4.4前后置条件的状态保存模块

4.4.1状态条件表达式

4.4.2构建状态条件语法树

4.4.3消除非运算符节点

4.4.4转化为析取范式语法树

4.4.5提取状态二重集合

4.4.6优化状态二重集合

4.4.7方法的优化

4.4.8方法的整合

4.4.9实例

4.5契约结构定义模块

4.5.1变量契约的数据结构

4.5.2函数契约的数据结构

4.6安全判定的实现

4.6.1变量契约的安全判定

4.6.2变量失效前的安全判定

4.6.3函数调用时的安全判定

4.7契约更新的实现

4.7.1变量契约更新

4.7.2函数调用时的契约更新

4.7.3函数返回时的契约更新

第五章安全实例分析

结束语

致谢

参考文献

作者在读期间研究成果

附录