安全C语言程序验证器中验证条件生成器的扩展设计与实现

发布时间：2024-02-28 00:26

　　交通、电力、军事等关键领域对软件的可靠性和安全性要求越来越高,因为其严重关乎国民的人身和财产安全。C语言在上述基础领域软件的开发中有广泛的应用。C语言灵活高效的特性允许程序员做相当底层的操作,但也导致C程序容易出现非法指针解引用、内存泄漏、缓冲区溢出等缺陷。形式化验证是一种可以严格保证程序可靠性的方法。本课题组正在研发一个安全C语言验证器,其功能是对携有程序标注的安全C语言程序进行演绎推理,验证程序是否满足预期规范。安全C语言验证器中验证条件生成器的作用是支持安全C语言和规范语言SCSL的语法,实现每条语句的演算规则,并根据演算规则遍历源程序进行演算,同时产生程序点的断言和合理有效的验证条件。本文的工作是对安全C语言验证器中的验证条件生成器进行扩展。本文的主要工作和贡献如下:第一、参与规范语言SCSL中逻辑变量、幽灵代码、字符串类型、带命名行为协议和多函数协议的设计,提高了规范语言的表达能力,同时独立设计和实现了对应的演算规则。第二、基于Hoare逻辑设计和实现跳转语句goto、continue和break、选择语句switch以及函数调用语句的演算规则,使得验证器可以支持更多C的语法...

【文章页数】：85 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第1章 绪论
    1.1 研究背景
        1.1.1 软件安全问题
        1.1.2 形式化验证
        1.1.3 研究现状
    1.2 本文概述
        1.2.1 研究工作
        1.2.2 主要贡献
        1.2.3 章节安排
第2章 Safe-C验证器
    2.1 Safe-C与程序标注
    2.2 Hoare逻辑
    2.3 验证器的框架与验证流程
    2.4 验证条件生成器的架构
    2.5 单个函数的验证过程
    2.6 本章小结
第3章 SCSL的扩展设计以及对应的演算规则
    3.1 逻辑变量
    3.2 幽灵代码
    3.3 字符串
        3.3.1 逻辑字符串
        3.3.2 字符串类型的操作与内置函数
        3.3.3 字符串的演算策略
        3.3.4 字符串操作语句的演算规则
    3.4 对函数协议的扩展
        3.4.1 简单函数协议
        3.4.2 带命名行为的函数协议
        3.4.3 多协议
    3.5 本章小结
第4章 语句的演算规则与事务的处理
    4.1 部分语句的演算规则
        4.1.1 goto语句和label语句
        4.1.2 continue语句
        4.1.3 break语句
        4.1.4 switch语句
    4.2 函数调用语句的演算规则
        4.2.1 无逻辑变量时的演算过程
        4.2.2 有逻辑变量时的演算过程
    4.3 赋值语句前事务的处理
        4.3.1 赋值语句前对量化断言的展开
        4.3.2 赋值语句前对谓词的展开
    4.4 本章小结
第5章 栈区内存模型
    5.1 Hoare逻辑赋值规则与别名
    5.2 栈区内存模型
    5.3 验证点处断言和内存表的构造
        5.3.1 函数入口处断言与内存表的构造
        5.3.2 循环入口处断言与内存表的构造
    5.4 取地址和解引用操作
    5.5 别名判断算法
    5.6 栈区赋值语句演算规则
        5.6.1 栈区变量赋值
        5.6.2 指针关系运算
    5.7 本章小结
第6章 验证实例与测试分析
    6.1 查找最大值和最小值函数的验证
    6.2 字符串拷贝函数的验证
    6.3 快速排序函数的验证
    6.4 测试结果分析
    6.5 本章小结
第7章 总结与展望
    7.1 总结和相关工作对比
    7.2 不足和进一步工作展望
参考文献
致谢
在读期间发表的学术论文与取得的其他研究成果



本文编号：3913193