Raymie Stata
ABSTRACT
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 paper 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 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.
- Coh97.Richard M. Cohen. Defensive Java Virtual Machine version 0.5 alpha release. Web pages at http://w~, cli. com/~ May 13, 1997.Google Scholar
- DE97.Sophia Drossopoulou and Susan Eisenbach. Java is type safe---probably. In Proceedings of ECOOP'gT, pages 389-418, June 1997.Google ScholarCross Ref
- LY96.Tim LindhoIm and Frank Yellin. The java Virtual Machine Spec~jicatior~ Addison-Wesley~ 1996. - Google ScholarDigital Library
- Mor95.Grog Morrisett. Compiling with Types. PhD the. sis, Carnegie Mellon University, December 1995.Google Scholar
- MTC+96.G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, 1996.Google Scholar
- Qia97.Zhenyu Qian. A formal specification of Java(tin) Virtual Machine instructions (draft). Web page at http://~w.informatik.uni-bremen . de/-qian/abs-f sjvm. html, 1997.Google Scholar
- Sar97.Vijay Saraswat. The Java bytecode verification problem. Web page at htep:/}w~w.research . art. com/-vj/main.html, 1997.Google Scholar
- SMB97.Emin G~in Sizex, Scan McDirmid, and Brian Bershad. Kimerm A Java system security architecture. Web pages at htzp://kiraera, es . washington, edu/~ 1997.Google Scholar
- Sym97.I)on Syme. Proving Java type soundness, Technical Report 427, University of Cambridge Computer Laboratory, June t{}97.Google Scholar
- TIC97.ACM SIGPLAN Workshop on Types in Compilation (TIC97). June 1997.Google Scholar
- Yel97.Frank Yellin. Private communication. March 1997.Google Scholar
Index Terms
- A type system for Java bytecode subroutines
Recommendations
A simple, comprehensive type system for Java bytecode subroutines
POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesA type system with proven soundness is a prerequisite for the safe and efficient execution of Java bytecode programs. So far, efforts to construct such a type system have followed a "forward dataflow" approach, in the spirit of the original Java Virtual ...
A type system for Java bytecode subroutines
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 ...
A type system for object initialization in the Java bytecode language
In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then executed by the Java Virtual Machine. Since bytecode may be written by hand, or ...
Comments