Abstract
Saraswat’s type spoofing was one of the most long-lasting bugs in the JVM. Recently, its solution was proposed and implemented in JDK 1.2. The correctness of this new feature, however, is non-trivial and required the formal soundness proof. Actually, during our work on it, two flaws inside the new JVM implementation were found. This paper briefly reports our work and results.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
A. Tozawa and M.Hagiya, New Formalization of the JVM, in preparation. Draft. available from http://nicosia.is.s.u-tokyo.ac.jp/members/miles/papers/cl-99.ps
T. Lindholm and F. Yellin, The Java Virtual Machine Specification, The Java Series, Addison-Wesley Longman, 1996. http://j.
V. Saraswat, Java is not type-safe, 1997. http://www.research.att.com/.
Sheng Liang, Gilad Bracha,Dynamic Class Loading in the Java Virtual Machine, OOPSLA’98, proc, pp. 36–43, 1998.
M. Hagiya and A. Tozawa, On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, SAS’98, Proc, LNCS 1503, Springer-Verlag, pp. 17–32, 1998. ftp://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/pro98/jvm-pro.ps.
R.Stata and M.Abadi, A Type System for Java Bytecode Subroutines, POPL’98, proc, pp. 149–160, 1998.
D.Dean, The Security of Static Typing with Dynamic Linking, 4th Conference on Computer and Communications Security, ACM, proc, 1997.
A. Goldberg, A specification of Java Loading and Bytecode Verification, 1998 http://www..
T. Jensen, D. Le Metayer and T. Thorn, Security and Dynamic Class Loading in Java: A Formalisation, Proceedings of IEEE International Conference on Computer Languages, pp. 4–15, 1998.
S.Freund and J.C.Mitchell, A Type System for Object Initialization in the Java Bytecode Language, ACM Symp. OOPSLA’98, Proceedings, pp. 310–327, 1998.
Z. Qian, A Formal Specification of Java Virtual Machine Instruction, 1997 http://www.infomatik.uni-bremen..
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tozawa, A., Hagiya, M. (1999). Careful Analysis of Type Spoofing. In: Cap, C.H. (eds) JIT’99. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-60247-4_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-60247-4_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66464-2
Online ISBN: 978-3-642-60247-4
eBook Packages: Springer Book Archive