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