【作者】 李兆鹏；

【导师】 陈意云；

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

【摘要】 随着计算机科学的飞速发展和计算机在全球日益普及,计算机软件越来越广泛的应用于各个行业。国家和社会的关键领域对软件的依赖程度日益增长,使得关键软件的高可信性质显得越来越重要,其中安全性是关注的重点。提高软件安全性的目标是:所有的程序错误在程序运行前被发现或者在程序运行时被温和地捕获,以保证程序不会导致不可预测的系统行为。而软件安全性研究主要是探索如何建立一个管理安全性的健全的科学和技术基础,其中软件满足安全策略的程序性质证明方法是研究的热点之一。近十年来,程序性质证明研究领域有了很大的发展。许多学者提出了不同的思路,这些思路主要采用基于类型的或基于逻辑的方法,来证明高级语言程序或低级语言程序的性质。程序性质证明采用类型方法和逻辑方法相结合方式可以兼得两种方法的长处。因此,本文作者所在的项目组(以下简称本项目组)选择采用一个简单的类型系统结合一个自动的逻辑推理系统的方法来证明程序满足安全策略。对那些有高安全要求的关键软件,程序设计及安全性证明可以在一种新的编程和编译框架下进行。在这个框架下,本项目组选择类C语言PointerC(带有动态存储分配)作为源语言,实现了一个出具证明编译器的原型;并且实现了类型安全和内存安全等基本安全策略。该出具证明的编译器在把源程序和规范翻译成汇编程序和等效规范的同时,将源程序满足规范的证明翻译成汇编代码满足等效规范的证明。在汇编语言一级由证明检查器利用代码所携带的证明进行代码满足规范的检验。汇编语言上的验证可以将编译器、验证条件生成器、定理证明器等排除出TCB,以尽量缩小系统的TCB。因而整个编译框架最终依赖于汇编程序形式验证框架,来保证产生的汇编程序满足汇编语言一级等效的安全规范。本文介绍作者在汇编级程序验证框架方面的研究。而在众多计算机程序中,指针程序的安全性质最为复杂,因此汇编指针程序安全性质的验证是本文的重点。本文的工作主要基于Hoare逻辑、携带证明代码(Proof-Carrying Code)和验证汇编编程(Certified Assembly Programming)等研究,采用类型和逻辑相结合的研究方法。本文首先介绍了基于程序性质证明的软件安全的相关研究和指针程序性质证明等方面的研究,然后介绍了本项目组提出的一个使用指针逻辑的安全软件丌发和验证框架。基于该框架下,本文着重介绍汇编程序一级的验证框架的设计和实现。本文提出了汇编级指针逻辑来对汇编指针程序安全性质的进行验证。本文还实现了一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。本文的主要特色和贡献为:●设计了一种基于x86机器模型、Hoare逻辑风格的形式证明框架,丰富了出具证明编译器的目标级基础研究。●设计了一种用于汇编指针程序安全性证明的指针逻辑,解决了Hoare逻辑处理别名面临的困难,使得拓展后的指针逻辑成为汇编程序性质证明的一种新工具。●证明了汇编语言指针逻辑的可靠性。并已在证明辅助工具Coq中完成。●实现了一个汇编级验证原型系统。本文使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。本工作的意义在于给出一种汇编指针程序验证的新思路,并设计实现了一个可用的原型系统,丰富了程序性质证明的研究和应用。更多还原

【Abstract】 With the rapid development of computer science and technology,computer software is more and more widely used in various industries.The dependence of computer software using in the key areas of the state and society is growing.So high-assurance software is more and more valued,and among its properties,safety and security are most important.The objective to improve software safety is:all program errors in the programs were discovered before the program is executed,or were captured moderately.Thus it ensures that programs would not result in unpredictable system behaviors.The research goal of software safety is to build a wholesome scientific and technological infrastructure for the management of software safety.And the verification method for software to meet its safety policies is one of the hot researches.In the past decade,great progress has been made in the area of program verification.Proof-Carrying Code brings two grand challenges to the research field of programming languages.By analysis of the current research situation,combining both type-based and logic-based approaches is a better way.We have designed a high-assurance software development infrastructure.In this infrastructure programs are certified to meet their safety policies using a simple type system and a logic system.In this infrastructure,source-level and assembly-level program verification could be done simultaneously,and a certifying compiler produces assembly-level safety proofs automatically from the source-level specifications and safety proofs.In terms of our infrastructure to design and verification of safety programs,and the pointer logic proof system,this dissertation presents the research work in assembly-level program verification.Among various computer programs,the programs containing pointers are more complex to reason about.So the research on verification of assembly pointer programs is an emphasis.The work in this dissertation is inspired by Hoare Logic,PCC(Proof-Carrying Code)and CAP (Certified Assembly Programming)etc.,and adopts an approach of combining both types and logics.This dissertation firstly introduces our research background on software safety and verification of pointer programs.Then a high-assurance software development infrastructure is presented.Under this infrastructure,the design and implementation of the assembly verification framework will be introduced.The main characteristics and contributions of this dissertation are:●A design of formal verification framework(Function-based Certifying Assembly Programming,FCAP)based on a x86 target machine.It is based on Intel x86 target machine.●A design of the assembly pointer logic(APL)for reasoning the safety of the assembly pointer programs.It has resolved difficulties to deal with the aliases using Hoare logic.It assures that there will be no null-pointer dereferences and no memory leak after the program is passed the verification.●Proof of the soundness of the assembly pointer logic is finished in the proof assistant Coq.●Implementation of a prototype system of the assembly-level verification framework.And using this prototype system,some non-trivial pointer programs of operations on the lists and binary trees have been verified.This dissertation was supported by Chinese Natural Science Foundation under Grant No.60673126 and Intel China Research Center(Beijing).更多还原