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

发布时间：2021-10-17 00:34

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

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：85 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第一章 绪论
    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.3.2.1 Expat介绍
            4.3.2.2 使用Expat编写XML解析器提取契约信息
    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.1.1 顺序结构中变量契约的更新
            4.7.1.2 分支结构中变量契约的更新
        4.7.2 函数调用时的契约更新
        4.7.3 函数返回时的契约更新
第五章 安全实例分析
结束语
致谢
参考文献
作者在读期间研究成果
附录A 配置文件格式定义
附录B 系统默认契约信息
附录C 细化的安全分析算法
附录D 对程序P的安全分析过程



本文编号：3440784