Skip to main content
SpringerLink
Log in

A Java Bytecode Formalisation

  • Conference paper
  • First Online:
Verified Software. Theories, Tools, and Experiments (VSTTE 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11294))

  • 613 Accesses

Abstract

This paper presents the first Coq formalisation of the full Java bytecode instruction set and its semantics. The set of instructions is organised in a hierarchy depending on how the instructions deal with the runtime structures of the Java Virtual Machine such as threads, stacks, heap etc. The hierarchical nature of Coq modules neatly reinforces this view and facilitates the understanding of the Java bytecode semantics. This approach makes it possible to both conduct verification of properties for programs and to prove metatheoretical results for the language. Based upon our formalisation experience, the deficiencies of the current informal bytecode language specification are discussed.

This work was partially supported by the Polish NCN grant no 2013/11/B/ST6/01381.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Available at http://cojaq.mimuw.edu.pl. Intermediate report appeared in [10].

  2. 2.

    This does not include native method calls.

  3. 3.

    The integer arithmetic was taken, in its major part, from Bicolano [27] by David Pichardie. The specification of floats was taken from the Coq contribution IEEE754 by Patrick Loiseleur.

References

  1. Atkey, R.: CoqJVM: an executable specification of the Java virtual machine using dependent types. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 18–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68103-8_2

    Chapter  MATH  Google Scholar 

  2. Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_4

    Chapter  Google Scholar 

  3. Bertelsen, P.: Dynamic semantics of Java bytecode. Future Gener. Comput. Syst. 16(7), 841–850 (2000)

    Article  Google Scholar 

  4. Bertot, Y.: Formalizing a JVML verifier for initialization in a theorem prover. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 14–24. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_3

    Chapter  Google Scholar 

  5. Chrza̧szcz, J.: Modules in Coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 130–146. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24849-1_9

    Chapter  Google Scholar 

  6. Chrząszcz, J., Czarnik, P., Schubert, A.: A dozen instructions make Java bytecode. ENTCS 264(4), 19–34 (2011)

    Google Scholar 

  7. Coglio, A., Goldberg, A., Qian, Z.: Toward a provably-correct implementation of the JVM bytecode verifier. In: Proceedings DARPA Information Survivability Conference and Exposition, 2000. DISCEX 2000, vol. 2, pp. 403–410. IEEE Computer Society (2000)

    Google Scholar 

  8. Coglio, A.: Improving the official specification of Java bytecode verification. Concurr. Comput.: Pract. Exp. 15(2), 155–179 (2003). http://dblp.uni-trier.de/db/journals/concurrency/concurrency15.html#Coglio03

    Article  Google Scholar 

  9. Coq development team: the Coq proof assistant reference manual V8.4. Technical Report 255, INRIA, France, March 2012. http://coq.inria.fr/distrib/V8.4/refman/

  10. Czarnik, P., Chrząszcz, J., Schubert, A.: CoJaq: a hierarchical view on the Java bytecode formalised in Coq. In: Swacha, J. (ed.) Advances in Software Development, pp. 147–157. Polish Information Processing Society (2013)

    Google Scholar 

  11. Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 97–113. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17164-2_8

    Chapter  Google Scholar 

  12. Farzan, A., Chen, F., Meseguer, J., Roşu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_46

    Chapter  Google Scholar 

  13. Freund, S.N., Mitchell, J.C.: The type system for object initialization in the Java bytecode language. ACM Trans. Program. Lang. Syst. 21(6), 1196–1250 (1999)

    Article  Google Scholar 

  14. Freund, S.N., Mitchell, J.C.: A type system for the Java bytecode language and verifier. J. Autom. Reason. 30(3–4), 271–321 (2003). https://doi.org/10.1023/A:1025011624925

    Article  MATH  Google Scholar 

  15. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification. The Java Series, 3rd edn. Addison Wesley, Boston (2005)

    MATH  Google Scholar 

  16. Hagiya, M., Tozawa, A.: On a new method for dataflow analysis of Java virtual machine subroutines. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 17–32. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_2

    Chapter  Google Scholar 

  17. Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Comput. Surv. 33(4), 517–558 (2001)

    Article  Google Scholar 

  18. Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45314-8_21

    Chapter  Google Scholar 

  19. Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006)

    Article  Google Scholar 

  20. Leroy, X.: Bytecode verification on Java smart cards. Softw. Pract. Exper. 32(4), 319–340 (2002)

    Article  Google Scholar 

  21. Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley Professional, Boston (1999). Specification available at https://docs.oracle.com/javase/specs/jvms/se6/html/VMSpecTOC.doc.html

  22. Lochbihler, A.: A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler. Ph.D. thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, July 2012

    Google Scholar 

  23. Milner, R., Harper, R., MacQueen, D., Tofte, M.: The Definition of Standard ML - Revised. The MIT Press, Cambridge (1997)

    Book  Google Scholar 

  24. MOBIUS Consortium: Deliverable 3.1: bytecode specification language and program logic (2006). http://mobius.inria.fr

  25. Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras and Logic of Engineering Software, pp. 227–290. IOS Press, Amsterdam (2003)

    Google Scholar 

  26. O’Callahan, R.: A simple, comprehensive type system for Java bytecode subroutines. In: Proceedings of POPL1999, pp. 70–78. ACM (1999)

    Google Scholar 

  27. Pichardie, D.: Bicolano - Byte Code Language in Coq (2006). http://mobius.inria.fr/bicolano. Summary appears in [24]

  28. Posegga, J., Vogt, H.: Byte code verification for Java smart cards based on model checking. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 175–190. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055863

    Chapter  Google Scholar 

  29. 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). https://doi.org/10.1007/3-540-49059-0_7

    Chapter  Google Scholar 

  30. Qian, Z.: A formal specification of Java\(\cal{M}\) 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). https://doi.org/10.1007/3-540-48737-9_8

    Chapter  Google Scholar 

  31. Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report TR #00-03d, Iowa State University, March 2000

    Google Scholar 

  32. Rose, E.: Lightweight bytecode verification. J. Autom. Reason. 31, 303–334 (2003)

    Article  Google Scholar 

  33. Soubiran, E.: Développement modulaire de théories et gestion de l’espace de nom pour l’assistant de preuve Coq. Ph.D. thesis, Ecole Polytechnique (2010)

    Google Scholar 

  34. Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001). https://doi.org/10.1007/978-3-642-59495-3

    Book  MATH  Google Scholar 

  35. Stata, R., Abadi, M.: A type system for Java bytecode subroutines. ACM Trans. Program. Lang. Syst. 21(1), 90–137 (1999)

    Article  Google Scholar 

  36. Yelland, P.M.: A compositional account of the Java virtual machine. In: Proceedings of POPL1999, pp. 57–69. ACM (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Warsaw, ul. S. Banacha 2, 02–097, Warsaw, Poland

    Patryk Czarnik, Jacek Chrząszcz & Aleksy Schubert

Authors
  1. Patryk Czarnik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacek Chrząszcz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Aleksy Schubert
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aleksy Schubert .

Editor information

Editors and Affiliations

  1. Yale University, New Haven, CT, USA

    Ruzica Piskac

  2. Uppsala University, Uppsala, Sweden

    Philipp Rümmer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Czarnik, P., Chrząszcz, J., Schubert, A. (2018). A Java Bytecode Formalisation. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science(), vol 11294. Springer, Cham. https://doi.org/10.1007/978-3-030-03592-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03592-1_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03591-4

  • Online ISBN: 978-3-030-03592-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation