首页 | 本学科首页   官方微博 | 高级检索  
     

一个经过证明的类型化汇编语言的类型检查器
引用本文:郭宇,陈意云,华保健,李兆鹏.一个经过证明的类型化汇编语言的类型检查器[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 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号