ISSN 1000-1239 CN 11-1777/TP

• 论文 • 上一篇    下一篇

一种汇编程序的形式验证框架

李兆鹏 陈意云 葛 琳 华保健   

  1. (中国科学技术大学计算机科学与技术系 合肥 230026) (中国科学技术大学苏州研究院软件安全实验室 苏州 215123) (zpli@mail.ustc.edu.cn)
  • 出版日期: 2008-05-15

A Formal Certifying Framework for Assembly Programs

Li Zhaopeng, Chen Yiyun, Ge Lin, and Hua Baojian   

  1. (Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230026) (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123)
  • Online: 2008-05-15

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

关键词: 软件安全, 出具证明编译器, 指针逻辑, 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.

Key words: Key wordssoftware safety, certifying compiler, pointer logic, Hoare logic, certified assembly program