A type system for Java bytecode subroutines
A type system for Java bytecode subroutines
复制标题
Java 字节码子例程的类型系统
DOI：
10.1145/314602.314606
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Abadi
中科院分区：
文献类型：
--
作者：
Raymie Stata;M. Abadi
Java通常被编译成中间语言JVML，由Java虚拟机解释。因为移动JVML代码并不总是受信任的，所以字节码验证器强制实施静态约束以防止各种动态错误。考虑到字节码验证器对于安全的重要性，它目前的描述是不充分的。本文建议使用类型规则来描述字节码验证器，因为它们比散文更精确，比代码更清晰，而且比两者都更容易推理。JVML有一个子例程结构，用于编译Java的Try-Finally语句。子例程是字节码验证器复杂性的主要来源，因为它们不是明显的后进/先出，而且它们需要一种多态。重点放在子例程上，我们分离出一个有趣的JVML子集。我们给出了这个子集的类型规则，并证明了它们的正确性。我们的类型系统为字节码验证和Sun字节码验证器的一个微妙部分的合理重构奠定了良好的基础。
Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode verifier for security, its current descriptions are inadequate. This article proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either. JVML has a subroutine construct which is used for the compilation of Java's try-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and because they require a kind of polymorphism. Focusing on subroutines, we isolate an interesting, small subset of JVML. We give typing rules for this subset and prove their correctness. Our type system constitutes a sound basis for bytecode verification and a rational reconstruction of a delicate part of Sun's bytecode verifier.