安全C语言的验证条件生成器的设计与实现

作     者：冯峰 

作者单位：中国科学技术大学 

学位级别：硕士

导师姓名：邵中;陈意云

授予年度：2016年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：程序验证 栈指针 静态区指针 路径别名 形式验证 Hoare逻辑 

摘      要：随着计算机应用的日益推广,我们对软件的可靠性和安全性的需求越来越高。这些需求体现在安全攸关的基础设施和系统上,包括核电、航空、航天、军事、金融等领域;也体现在人们日常生活中,如汽车、医疗、电子支付等领域。C语言作为主流的编程语言之一,在操作系统、嵌入式软件、编译器等领域都有广泛的应用。由于C语言具有指针、动态内存分配等特点,导致其与其他编程语言相比,容易出现非法指针解引用、内存泄漏等一系列安全漏洞。通过静态分析、动态分析、程序验证等方法检查C程序中的安全漏洞是目前学术界和工业界的热门研究方向。本实验室正在开发的一个基于演绎推理的程序验证工具：安全C语言验证工具,它是一个针对C语言程序的自动化形式验证工具,可以检查出程序中出现的内存错误,保障程序满足预期的规范。本文介绍的是安全C语言验证工具中的验证条件生成器的设计与实现,验证条件生成器的主要作用是：第一,基于各类语句的演算规则以及语句前条件进行产生语句后条件的演算;第二,在各个程序点,根据演算得到的断言产生必要的验证条件。本文主要贡献如下：第一,设计并实现安全C语言的断言演算基本流程框架。包括安全C语言中各类语句基于Hoare逻辑的断言演算规则,以及在使用演算规则前后需要对断言所做的处理;另外,验证条件生成器在程序的各个程序点产生必要的验证条件,包括一些必要的检查,如：类型不变式和数据不变式的检查、指针越界访问检查、非法指针解引用检查等等。第二,设计和实现了栈指针、静态区指针程序的形式验证方法：该方法定义指针的三元属性表示一个指针的状态。指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移。通过对Hoare逻辑的扩展,基于上述的基本演算流程和指针的三元属性表示法,设计了相应的栈指针、静态区指针相关断言演算规则和生成验证条件的方法。该方法可以解决栈指针和静态区指针相关的问题,例如：路径别名判断、指针越界访问检查、非法指针解引用检查等.对于堆指针相关断言的演算本文会给出了演算过程中需要调用的形状分析模块中比较重要的接口。目前通过本文所介绍的安全C语言验证条件生成器的实现,安全C语言验证工具已经成功地验证了部分教材上常用的经典算法。