C程序精确形状分析中的规范语言设计

摘要

随着计算机技术的快速发展，计算机软件的规模越来越大，软件调试和维护越来越困难，其成本也越来越高，软件的安全形势变得越来越重要。特别是在安全攸关领域（例如，航空航天、高铁、核电、医疗等领域），人们对高可信软件的需求越来越大。在这些领域，C语言仍是最普遍使用的编程语言。而C程序中的空指针脱引用、内存泄漏、缓冲区溢出等诸多内存安全问题在软件开发中依然突出。
　　提高软件质量的方法有很多种，如软件测试、程序分析和程序验证等;在众多方法中，相对有效而又经济的方法是程序静态分析。针对C程序中内存安全问题，作者所在实验室的课题组开发了一个静态分析工具，该工具采用了符号执行的静态分析技术，并加入了形状分析，为了降低静态分析的误报率和漏报率，以及提高分析的效率，设计了表达能力较为丰富的规范语言来描述程序状态和函数行为。
　　在该静态分析工具的实现中，设计了描述函数行为的规范语言，包括描述程序状态的基本断言，描述内存状态的谓词以及描述单链表、双链表、二叉树的形状谓词。该工具基于编译框架LLVM和符号执行分析工具KLEE，以函数为单位分析并构造函数行为规范，该过程中需要用断言描述程序状态并按需抽象成形状谓词。为此，针对断言设计了一系列的规范化和抽象化规则。
　　本文的贡献主要有三方面:第一，设计并实现了描述函数行为的规范语言，包括描述程序状态的基本断言，描述内存的谓词以及描述单链表、双链表、二叉树的形状谓词。通过规范语言来记录已分析函数的行为，可以避免重复分析，提高分析的效率。通过使用描述内存的谓词和形状谓词，该工具可以检测内存泄漏、空指针脱引用等内存安全问题以及进行形状分析。第二，设计并实现了一系列的规则来规范和抽象断言，将程序状态抽象成形状谓词，用于形状分析。第三，利用已有的规范语言为C语言标准库函数构造函数行为规范。许多程序中会频繁调用C的库函数，为这些常用的库函数手动构造行为规范可以提高分析的精度和效率。
　　本文工作的意义在于针对C程序内存安全问题，提出了一套规范语言;并针对形状分析，提出了一系列的抽象化规则，用于精确分析单链表、双链表和二叉树等递归数据结构程序中的内存安全错误，为以后的研究和工具扩展奠定了基础。

目录

声明

摘要

第1章 绪论

1．1 研究背景

1．1．1 C程序的安全性

1．1．2 程序静态分析

1．1．3 规范语言

1．2 本文概述

1．2．1 研究工作

1．2．2 主要贡献

1．2．3 章节安排

第2章 ShapeChecker简介

2．1 ShapeChecker总体框架

2．2 编译框架LLVM

2．2．1 LLVM总体结构

2．2．2 LLVM IR简介

2．3 符号执行

2．3．1 符号执行算法

2．3．2 符号执行面临的问题

2．4 本章小结

第3章 规范语言的设计

3．1 ACSL简介

3．2 IRSL规范语言

3．2．1 断言语言

3．2．2 形状谓词

3．2．3 函数规范

3．3 函数行为规范的构建

3．3．1 程序状态

3．3．2 行为规范的构建过程

3．4 支持的C标准库函数

3．4．1 malloc()函数行为规范

3．4．2 free()函数行为规范

3．4．3 strcat()函数行为规范

3．5 本章小结

第4章 规范化和抽象化

4．1 规范化

4．2 抽象化

4．2．1 单链表表段的抽象规则

4．2．2 双链表表段的抽象规则

4．2．3 二叉树的抽象规则

4．2．4 数组谓词的抽象

4．3 本章小结

第5章 实例分析

5．1 一维数组程序示例

5．1．1 函数行为规范

5．1．2 抽象化和规范化操作

5．2 单链表的程序示例

5．2．1 函数行为规范

5．2．2 抽象化操作

5．2．3 规范化操作

5．2．4 错误检测

5．3 双链表的程序示例

5．3．1 函数行为规范

5．3．2 抽象化操作

5．3．3 规范化操作

5．4 调用C库函数的程序示例

5．5 本章小结

第6章 实现及实验结果

6．1 实现工作

6．2 实验结果

6．3 本章小结

第7章 结束语

7．1 论文工作总结

7．2 进一步研究方向

参考文献

致谢

在读期间发表的学术论文与取得的研究成果