【摘要】 Java虚拟机支持一种功能很强的动态加载类的机制,它具有惰性加载、类型安全连接、用户自定义加载策略、以及动态名字空间等特性。但是,在Java的早期实现(JDK1.0和1.1)中,这种机制包含了一种称为类型欺骗的严重设计错误。尽管JDK1.2通过引入一种类加载约束策略修正了这个错误,但是由动态加载引起的其它形式的类型欺骗仍然存在于JDK1.2和1.3中。本文详细讨论了与动态类加载相关的类型欺骗问题,提出了一个严格定义Java虚拟机操作语义和静态语义的形式化模型。其中,操作语义描述了类加载约束策略、字段及方法解析算法等类加载的主要特性;静态语义采用类型规修正了JDK1.2和1.3中的类型欺骗。更多还原

【Abstract】 The Java Virtual Machine(JVM)supports a novel and powerful class loading mechanism which incorporates all of the following features: lazy loading, type-safety linkage, user-definable class loading policy and multiple names- paces. However, that class loading methanism contained a seerious type-spoofing bug in earlier implementations (JDK 1.0 and 1.1), which leads to type safety violations. Although JDK 1.2 introduces a class loading constraint scheme to fix the bug, subtle type spoofing related to class loaders still exists in JDK 1.2 and 1.3. We develop a formal model to specity the operational semantics and static semantics of the Java virtual machine, rigorously. In the model, the opera- tional semantics describes the main features of class loading such as class loading constraints scheme, field and method resolutions etc. The static semantics uses typing rules to fix the type-spoofing bug in JDK 1.2 and 1.3.更多还原