nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

A Java Bytecode Formalisation

verfasst von : Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert

Erschienen in: Verified Software. Theories, Tools, and Experiments

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel TWAM: A Certifying Abstract Machine for Logic Programs

Nächstes Kapitel Formalising Executable Specifications of Low-Level Systems

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

This does not include native method calls.

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.

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_2CrossRefMATH

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_4CrossRef

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

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_3CrossRef

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_9CrossRef

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

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)

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#Coglio03CrossRef

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)

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_8CrossRef

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_46CrossRef

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)CrossRef

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:1025011624925CrossRefMATH

15.

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

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_2CrossRef

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)CrossRef

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_21CrossRef

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)CrossRef

20.

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

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

23.

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

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)

26.

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

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/BFb0055863CrossRef

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_7CrossRef

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_8CrossRef

31.

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

32.

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

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)

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-3CrossRefMATH

35.

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

36.

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

Titel: A Java Bytecode Formalisation
verfasst von: Patryk Czarnik
Jacek Chrząszcz
Aleksy Schubert
Verlag: Springer International Publishing
Buch: Verified Software. Theories, Tools, and Experiments
Print ISBN: 978-3-030-03591-4

Electronic ISBN: 978-3-030-03592-1

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-03592-1_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"