Abstract
Dynamic class loading is an important feature of the Java virtual machine. It is the underlying mechanism that supports installing software components at runtime. However, it is also complex. Improperly written class loaders could undermine the type safety of the Java virtual machine. Given the importance of security, the current description provided by the Java virtual machine is deficient. It is ambiguous, imprecise and hard to reason about. In this paper, we suggest a model for the Java virtual machine, which includes the main features of dynamic class loading and linking. We formalize the model and prove its soundness in the HOL system. The soundness theorem demonstrates that our model can preserve types indeed. Based on the model, we can analyze the behaviors of loading in the virtual machine.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barthe, G., Courtieu, P.: A formal correspondence between offensive and defensive javacard virtual machines. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 31–46. Springer, Heidelberg (2002)
Barthe, G., Dufay, G., Jakubiec, L., Sousa, S.M., Serpette, B.P.: A formal executable semantics of the javacard platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 302–319. Springer, Heidelberg (2001)
Barthe, G., Dufay, G., Jakubiec, L., Sousa, S.M., Serpette, B.P.: A formal correspondence between offensive and defensive javacard virtual machines. In A. Cortesi, editor, Proc. VMCAI’02. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 32–45. Springer, Heidelberg (2002)
Dean, D.: The security of static typing with dynamic linking. In: Fourth ACM Conference on Computer and Communication Security (1997)
Drossopoulou, S.: Towards an abstract model of java dynamic linking and verification. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 53–84. Springer, Heidelberg (2001)
Fong, P.W.L., Cameron, R.D.: Proof linking: Modular verification of mobile programs in the presence of lazy, dynamic linking. ACM Transactions on Software Engineering and Methodology 9(4), 379–409 (2000)
Jensen, T., Le Metayer, D., Thorn, T.: Security and dynamic loading in java: A formalisation. In: Proceedings of the 1998 IEEE International Conference on Computer Languages, Chicago, Illinois, May 1998, vol. 2618, pp. 4–15 (1998)
Klein, G.: Verified Java bytecode verification. PhD thesis, Technische Universitat Munchen (2003)
Klein, G., Strecker, M.: Verified bytecode verification and typecertifying compilation. Journal of Logic Programming (2002)
Klein, G., Wildmoser, M.: Verified bytecode subroutines. Journal of Automated Reasoning, Special Issue on Bytecode Verification (2003)
Liu, H., Moore, J.S.: Executable jvm model for analytical reasoning: a study. In: Proceedings of the 2003 workshop on Interpreters, Virtual Machines and Emulators, San Diego, California, pp. 15–23 (2003)
Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 347–363. Springer, Heidelberg (2001)
Nipkow, T., von Oheimb, D., Pusch, C.: μjava: Embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbruggen, R. (eds.) Foundations of Secure Computation, pp. 117–144. IOS Press, Amsterdam (2000)
Pusch, C.: Proving the soundness of a java bytecode verifier specification in isabelle/hol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 89–103. Springer, Heidelberg (1999)
Qian, Z.: A formal specification of java-TM virtual machine instructions for objects, methods and subroutines. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 271–311. Springer, Heidelberg (1999)
Qian, Z., Goldberg, A., Coglio, A.: A formal specification of javatm class loading. In: OOPSLA 2000 (November 2000)
Saraswat, V.: Java is not type-safe. Technical report, AT&T Rresearch (1997)
Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
Tozawa, A., Hagiya, M.: New fomalizaion of the JVM (1999), http://nicosia.is.s.u.-tokyo.ac.jp/members/milespapers/cl-99.ps
von Oheimb, D.: Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universitat Munchen (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zuo, Tj., Han, Jg., Chen, P. (2004). Formalizing Java Dynamic Loading in HOL. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive