| 一个经过证明的类型化汇编语言的类型检查器 |
| |
| 引用本文： | 郭宇,陈意云,华保健,李兆鹏. 一个经过证明的类型化汇编语言的类型检查器[J]. 小型微型计算机系统, 2008, 29(7) |
| |
| 作者姓名： | 郭宇 陈意云 华保健 李兆鹏 |
| |
| 作者单位： | 中国科学技术大学,计算机科学与技术系,安徽,合肥,230027 |
| |
| 摘 要： | 编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全, 内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性.
|
| 关 键 词： | 类型系统 汇编语言 类型检查 软件安全 类型化 汇编语言 检查器 Assembly Language 高级语言 方法 辅助工具 定理证明 相关 工作 文本 汇编程序 类型检查 类型性 检查程序 内存 安全属性 控制流 运行时 安全性 |
A Certified Type Checker for Typed Assembly Language |
| |
| GUO Yu,CHEN Yi-yun,HUA Bao-jian,LI Zhao-peng. A Certified Type Checker for Typed Assembly Language[J]. Mini-micro Systems, 2008, 29(7) |
| |
| Authors: | GUO Yu CHEN Yi-yun HUA Bao-jian LI Zhao-peng |
| |
| Affiliation: | GUO Yu,CHEN Yi-yun,HUA Bao-jian,LI Zhao-peng(Department of Computer Science , Technology,University of Science , Technology of China,Hefei 230027,China) |
| |
| Abstract: | Typed programming languages guarantee the type safety of programs at runtime,such as control-flow safety and memory safety.A type checker is needed to check whether programs are well-typed.Therefore,the safety of a typed programming language still greatly depends on the soundness of its type checker.This paper proposes a typed assembly language with a type checker which is used to check the type of the programs written in this assembly language.Moreover,the soundness of the type checker has been proved so t... |
| |
| Keywords: | type system assembly language type checking software safety |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
