| 一种汇编程序的形式验证框架 |
| |
| 引用本文： | 李兆鹏,陈意云,葛琳,华保健.一种汇编程序的形式验证框架[J].计算机研究与发展,2008,45(5):825-833. |
| |
| 作者姓名： | 李兆鹏 陈意云 葛琳 华保健 |
| |
| 作者单位： | 中国科学技术大学苏州研究院软件安全实验室,苏州,215123;中国科学技术大学计算机科学与技术系,合肥,230026 |
| |
| 基金项目： | 国家自然科学基金
,
Intel中国研究中心资助项目 |
| |
| 摘 要： | 在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.
|
| 关 键 词： | 软件安全 出具证明编译器 指针逻辑 Hoare逻辑 携带证明的汇编程序 |
| 修稿时间： | 2007年2月5日 |
A Formal Certifying Framework for Assembly Programs |
| |
| Li Zhaopeng,Chen Yiyun,Ge Lin,Hua Baojian.A Formal Certifying Framework for Assembly Programs[J].Journal of Computer Research and Development,2008,45(5):825-833. |
| |
| Authors: | Li Zhaopeng Chen Yiyun Ge Lin Hua Baojian |
| |
| Affiliation: | Li Zhaopeng,Chen Yiyun,Ge Lin,, Hua Baojian(Department of Computer Science , Technology,University of Science , Technology of China,Hefei 230026)(Software Security Laboratory,Suzhou Institute for Advanced Study,Suzhou 215123) |
| |
| 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... |
| |
| Keywords: | software safety certifying compiler pointer logic Hoare logic certified assembly program |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
