基于逻辑的程序验证方法在高可信软件开发上的应用

【作者】 项森；

【导师】 陈意云；

【作者基本信息】 中国科学技术大学 ， 计算机软件与理论， 2006， 博士

【摘要】 随着软件规模的越来越大，软件的安全越来越引起软件开发人员的关注，而现有的编程语言以及软件开发方法所能提供的安全保证是脆弱和不可靠的，例如通过标准的软件工程方法和大量的测试减少软件漏洞的发生，但是即使经过高强度测试的软件，也不能保证它没有漏洞，另外一方面，对一个漏洞的修复也往往会引起新的漏洞。可以说，现有的软件工程方法对软件安全的提高已经越来越微弱。而基于语言的程序验证方法能为软件安全提供可靠的保证。 基于语言的程序验证方法通过对程序设计语言添加静态的类型以及规范结构，使得用这种语言写出的良形式程序是安全的。现有的关于认证代码技术以及类型系统方面的研究已经能够验证低级语言和高级语言程序的多种安全属性。例如，当前的大部分程序设计语言都有一个类型系统，它一般用于检查程序的一些简单语义错误，可靠的类型系统可以以较低的代价保证程序的一些基本安全属性。安全的高级语言和通用中间层语言的类型系统的研究已经对安全计算做了有意义的贡献，但是用这些语言写就的安全程序还需经过多步的未经编译和优化才能在最终的硬件上运行，这使得最终运行的代码是未经验证的。基于这个原因，很多工作转向研究低级代码的验证，特别是研究从类型化高级语言代码产生可验证低级代码的认证编译器。但是由于类型的弱表达能力，使得类型系统只能保证代码一些最基本的安全属性，对用户指明的一些安全属性，比如算法正确性，信息流安全等基本不能触及。也正由于这个原因，对于现实的底层软件如启动引导程序，操作系统内核，用户态运行时函数库等，都没有相应的经过验证版本发布出来，而这些底层软件的安全性对整个计算系统的安全性来说是至关重要的。但是，类型系统对栈式函数调用的模块化验证有比较好的支持。另一方面，Hoare逻辑具有很强的表达能力，因为相对于类型的弱表达能力，逻辑谓词能够表达更丰富的程序属性，但是Hoare逻辑对栈式函数调用的支持比较弱。基于此，本文的研究目标是以逻辑谓词代替类型作为规范标注程序，结合类型系统和Hoare逻辑两方面的优点，设计可以模块化地构造程序满足规范的证明的框架，并使用它进行安全代码的开发。 本文提出一个基于逻辑的使用汇编语言的高可信软件开发方法，并运用此方法开发出经过严格安全验证的运行时库和操作系统组件。此方法源于Hoare逻辑的程序推理以及耶鲁大学的认证汇编编程(CAP)，它首先需要定义一个推理需要的目标机器和一组静态推理规则，并且证明推理规则的可靠性(安全性)。本文的贡献有如下几个方面： ·设计并使用Coq实现一个现实的x86平台上的认证汇编语言RCAL86，并证明更多还原

【Abstract】 Today, most softwares are of large scale, so the programmers have paid much more attention to their safety. But until now, the safety guarantee provided by existing programming language and software engineering technology is weak and unreliable. For instance, in the production of software, standard engineering method and intensive testings are used to decrease bugs. However, it can’t be guaranteed that there are no bugs after intensive testings, in fact, new bugs will be introduced when the old bugs are fixed. It can be asserted that existing software engineering techniques can’t improve the software safety and security essentially. On the other hand, language based approach of program verification can provide guarantee for software safety.Language based approach of program verification makes the programs of this language safe through adding language components of types (logic predicates), which are called program specifications universally, and typing rules (reasoning rules), which should be definitely proved to be sound. Existing research on certified code and type system has contributed much on the guarantee of a variety of program (high-level or low-level) safety properties, such as the simple type system of modern programming language, which can be utilized to check some simple semantics errors and guarantee fundamental safety properties with little cost. Although research on type system of high-level and intermediate language have contribute to computation safety significantly, the ultimate codes executed in machine are binaries, which are originated from certified programs and not certified themselves. For this reason, many researchers begin explore the approaches of low-level program verification and certifying compiler which preserves the program specification from high-level to low-level. Compared with logic predicates, types are less expressive, so type system can’t deal with complex safety requirements, such as program correctness, information flow security. Thus, although type system is widely used, until now, no certified version of boot loader, operation system kernel, and runtime library are released, whose safety are critical for the safety of whole computation system. In the other hand, Hoare logic has enough expressiveness since logic predicates can express more information than types. However, the support of stack-based function call is weak in Hoare logic. For these reasons, the goal of this research is substituting logic predicates for types as program specification so that type system更多还原