| 安全语言PointerC的设计及形式证明 |
| |
| 引用本文： | 华保健,陈意云,李兆鹏,王志芳,葛琳.安全语言PointerC的设计及形式证明[J].计算机学报,2008,31(4):556-564. |
| |
| 作者姓名： | 华保健 陈意云 李兆鹏 王志芳 葛琳 |
| |
| 作者单位： | 1. 中国科学技术大学计算机科学技术系,合肥,230026
2. 中国科学技术大学苏州研究院软件安全实验室,江苏,苏州,215123 |
| |
| 基金项目： | 国家自然科学基金(60673126)，Intel中国研究中心资助~~ |
| |
| 摘 要： | 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的.
|
| 关 键 词： | 软件安全 语言设计 类型系统 Hoare逻辑 指针逻辑 |
| 修稿时间： | 2007年11月26 |
Design and Proof of a Safe Programming Language PointerC |
| |
| HUA Bao-Jian,CHEN Yi-Yun,LI Zhao-Peng,WANG Zhi-Fang,GE Lin.Design and Proof of a Safe Programming Language PointerC[J].Chinese Journal of Computers,2008,31(4):556-564. |
| |
| Authors: | HUA Bao-Jian CHEN Yi-Yun LI Zhao-Peng WANG Zhi-Fang GE Lin |
| |
| Abstract: | |
| |
| Keywords: | software safety language design type systems Hoare logic pointer logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
