【摘要】 在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.更多还原

【Abstract】 Proof-carrying code brings two grand challenges to the research field of programming languages.One is to study the technology of certifying compilation.The other is to seek more expressive program logics or type systems to specify or reason about the properties of high-level or low-level programs.And safety is an important issue among the properties of high-assurance software.The verification method for software to meet its safety policies is one of the hot researches.In terms of the framework to design and verification of safety programs,and the pointer logic proof system,this paper introduces the research on the formal description of target machine,the formal certifying framework for assembly programs and property proof of assembly pointer programs.The main characteristics of the design and implementation are as follows:first,the design of the certifying framework is based on program verification method of Hoare style;second,program property related with pointers is proved using a pointer logic which is similar to the counterpart in the level of source language;and finally,a simple type system is designed to fulfill type checking on pointers.Moreover,this work has been formalized in the proof assistant Coq and all code is available on the website of the authors’ laboratory.更多还原