基于LLVM的静态程序有界模型检测

发布时间：2023-06-13 19:43

　　科技发展日新月异,计算机的应用越来越普及,使得程序随处可见,其应用场景十分广泛,小到手机应用、智能家电控制系统和门禁系统等,大到交通控制系统、高铁列车控制系统和卫星通信系统等。人们的安全意识也逐步提高,对于程序的安全性和可靠性的要求也越来越高。如何保障程序的安全性和提高可靠性一直以来是软件技术发展与应用的核心问题之一。本文主要从静态程序验证领域对程序源代码进行分析。其工作流程首先通过底层虚拟机(Low Level Virtual Machine,LLVM)将源代码转换成与语言无关的中间表示,并对中间表示进行优化和提升,转化成静态单赋值形式;其次使用有界模型检测技术实现程序有限次数的循环展开;然后通过语义分析将中间表示转化成等价的基于SMT-lib2规范的公式;最后调用可满足性模理论(Satisfiability Modulo Theories,SMT)求解器验证解析后的公式集合的正确性。本文的主要贡献有三个方面:首先实现了基于LLVM的中间表示的基本块状态迁移系统的有界模型检测方法,避免了对源代码的直接验证,通过有界模型检测实现循环展开,通过语义分析实现数据流编码,通过构造迁移关系实现...

【文章页数】：64 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
第1章 引言
    1.1 研究背景和意义
    1.2 研究现状
    1.3 主要工作
    1.4 论文结构
    1.5 本章小结
第2章 相关技术
    2.1 形式验证
    2.2 有界模型检测
    2.3 LLVM
        2.3.1 中间表示
        2.3.2 指令集
        2.3.3 静态单赋值形式
    2.4 控制流分析
        2.4.1 控制流图
        2.4.2 支配关系
        2.4.3 后支配关系
        2.4.4 控制依赖关系
    2.5 SMT求解器
    2.6 本章小结
第3章 基于状态迁移的程序验证方法
    3.1 生成中间表示
    3.2 有限次循环展开
        3.2.1 循环展开预处理
        3.2.2 循环展开
    3.3 迁移系统构造
        3.3.1 基本块
        3.3.2 基本块迁移关系构造
        3.3.3 指令构造
    3.4 测试用例生成公式
    3.5 实验分析
    3.6 本章小结
第4章 基于状态迁移的程序验证方法改进
    4.1 迁移系统构造
        4.1.1 基本块表示
        4.1.2 指令分析
    4.2 测试用例生成公式
    4.3 实验分析
    4.4 本章小结
第5章 基于控制依赖关系的程序验证方法
    5.1 拓扑排序
    5.2 控制依赖关系
    5.3 迁移系统构造
        5.3.1 控制流表示
        5.3.2 指令分析
    5.4 测试用例生成公式
    5.5 实验分析
    5.6 本章小结
第6章 总结与展望
    6.1 本文主要成果
    6.2 本文的创新点
    6.3 本文的不足
    6.4 将来的工作
参考文献
致谢



本文编号：3833174