一种用于Java程序验证编译的标签类型.pdfVIP

1000-9825/2005/16(03)0346 © 2005 Journal of Software 软 件 学 报 Vol.16, No.3 一种用于Java 程序验证编译的标签类型 + 陈 晖, 陈意云, 茹祥民 ( 中国科学技术大学 计算机科学系,安徽 合肥 230027) A Tag Type for Certifying Compilation of Java Program + CHEN Hui, CHEN Yi-Yun , RU Xiang-Min (Department of Computer Science, University of Science and Technology of China, Hefei 230027 , China) + Corresponding author: Phn: +86-551-3607043, E-mail: yiyun@ Received 2004-09-01; Accepted 2004-11-03 Chen H, Chen YY, Ru XM. A tag type for certifying compilation of Java program. Journal of Software, 2005,16(3):346- 354. DOI: 10.1360/jos160346 Abstract: In the area of language-based security, programs written in typed high -level languages need to be translated into those written in typed low-level languages. This work is not trivial when type dispatch constructs are involved and implemented with tag mechanism. This paper proposes a new type that can deal with a special type dispatch construct occurring in the interface invokation of Java. A low-level language with this type is able to efficiently implement the interface invokation. This implementation approach is adopted in a Just-In-Time compiler with a typed low-level language as a certifying language. Key words : type-preserving compilation; type dispatch; tag mechanism 摘 要: 在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行 类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继 承接口的 Java 程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言 能够有效地实现 Java 程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语 言的Java 字节码即时编译器中. 关键词: 类型保持编译;类型调度;标签机制 中图法分类号: TP301 文献标识码: A 经典的计算机安全原则和受信任计算基础(trusted computer base,简称 TCB)尽可能小的原则,要求软件系 统的TCB 尽可能地小而简单[1].TCB 是系统中这样的代码或机制:我们未能证明它们是安全的,而又不得不基于 它们是安全的假设来证明系统是安全的.显然,系统的 TCB 越大,则存在安全漏洞的可能性就越大.在过去的 10 Supported by the