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

摘要：

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

关键词：软件安全、出具证明编译器、指针逻辑、Hoare逻辑、携带证明的汇编程序

所属期刊栏目：45

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目60473068,60673126;Intel中国研究中心资助项目

在线出版日期：2008-07-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：825-833