论文摘要
今天软件在我们的生活中已经无处不在,它对人们的影响越来越大,虽然有时会觉察不到它的存在。在许多领域如航空航天、金融、医疗、汽车电子等,软件的可信性具有十分重要的意义。随着软件工程技术的不断发展,软件的规模不断扩大,复杂度越来越高,应用场景更加广泛,运行环境网络化、动态化,形态更加多样化。这些因素导致保证软件的可信性变得十分困难。寻找更加有效的方法提高软件的可信性一直是学术界和工业界关注的重点。软件的可信性可以在软件开发周期的各个阶段及各种制品上进行保证。基于代码的可信性保障方法是一个有效的重要方法,因为代码直接反映了软件的运行行为。在这种方法中,传统的测试方法无法保证软件完全的可信性,而程序验证方法由于完备性和可靠性,越来越受到重视。在系统软件中,存在大量的C代码。而对类似C这样包含指针操作、变量引用、堆操作的程序的验证一直是程序验证面临的挑战。本文主要研究针对类C语言的基于类型系统的静态程序验证方法,基本思想是通过确保程序具有合法的类型来保证其可信性。已有的验证方法要么难以使用,要么验证的性质有限。提出的方法将类型系统和基于霍尔逻辑的程序验证进行有机的结合,可以在不增加编程复杂度的情况下实现对程序较为深刻性质的验证,从而提高程序验证的易用性和有效性。为了对较低级的类C语言给出精确的安全形式化语义,我们首先提出了一个安全的类型化内存模型。这个内存模型既支持较低级的内存操作,又具备一定的抽象性,方便程序验证等其它需要屏蔽细节的应用。内存模型可以描述访问控制同时类型化特征保证了内存操作的严格安全性,即读取的数据具有合法的类型状态。给出了内存模型完整的抽象性质,同时实现了一个具体的内存模型。为了实现对类C语言的验证,我们设计了一种扩展的类型系统,它是建立在精化类型、子类型、动态类型等高级类型系统的基础上,因而可以对指针变量及操作进行精确的刻画,对堆中数据结构的性质进行隐式描述。类型系统具有开放性的特点,易于扩展。给出了类型系统的形式化描述,在类型化内存模型的基础上形式化的定义了源语言的操作语义,利用操作语义证明了类型系统的安全性。为了提高类型检测的自动化程度和精度,我们利用高效的自动定理证明器如可满足性模理论求解器来实现类型检测。首先将含扩展类型的待验证代码转换成普通代码,使用传统的类型检测算法进行检测。如果检测通过,则将待验证代码转换成中间验证语言Boogie代码。这个转换过程是对源代码的动态和静态语义进行编码的过程,从而保证了用于程序验证的信息不会丢失。这种方式的类型检测算法只需要设计一个语法指导的转换算法,不需要设计特定的复杂类型检测算法,具有通用性好、易于扩展、自动化程度高的特点。