一个经过证明的类型化汇编语言的类型检查器

• 作者: 华保健 李兆鹏 郭宇 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 类型系统 汇编语言 类型检查 软件安全
• 年，卷（期）: 2008,（7）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 1230-1236
• 页数: 7页
• 分类号: TP301
• 字数: 9453字
• 语种: 中文

摘要

编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全, 内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术系	83	854	16.0	26.0
2	华保健	中国科学技术大学计算机科学与技术系	17	116	6.0	10.0
3	李兆鹏	中国科学技术大学计算机科学与技术系	17	99	7.0	9.0
4	郭宇	中国科学技术大学计算机科学与技术系	12	38	3.0	6.0