Java and the Java Virtual Machine : Definition, Verification, Validation

by Stark, Robert F.; Borger, Egon; Shmid, Joachim

• ISBN13: 9783540420880
• ISBN10: 3540420886
• Format: Hardcover
• Copyright: 2001-08-01
• Publisher: Springer Verlag

Summary

This book provides a high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into language layers and machine components. It comes with a natural executable refinement (written in AsmGofer and provided on CD ROM) which can be used for testing code. The method developed for this purpose is based on Abstract State Machines (ASMs) and can be applied to other virtual machines and to other programming languages as well. The book is written for advanced students and for professionals and practitioners in research and development who need a complete and transparent definition and an executable model of the language and of the virtual machine underlying its intended implementation. The CD ROM contains the entire text of the book and numerous examples and exercises. "The Jbook gives the most comprehensive and consistent formal account of the combination of Java and the JVM." (Pieter Hartel and Luc Moreau in Formalizing the Safety of Java, the Java Virtual Machine and Java Card, ACM Computing Surveys, 33(4):517-558, 2001. Section 6.2, page 540.)

Table of Contents

Introduction	1	(14)
The goals of the book	2	(1)
The contents of the book	3	(4)
Decomposing Java and the JVM	7	(4)
Sources and literature	11	(4)
Abstract State Machines	15	(18)
ASMs in a nutshell	15	(3)
Mathematical definition of ASMs	18	(9)
Notational conventions	27	(6)
Part I. Java
The imperative core JavaI of Java	33	(14)
Static semantics of JavaI	33	(6)
Transition rules for JavaI	39	(8)
The procedural extension Javac of JavaI	47	(24)
Static semantics of Javac	47	(16)
Transition rules for Javac	63	(8)
The object-oriented extension Java of Javac	71	(16)
Static semantics of Java	71	(9)
Transition rules for Java	80	(7)
The exception-handling extension Java of Java	87	(8)
Static semantics of Java	87	(2)
Transition rules for Java	89	(6)
The concurrent extension JavaI of Java	95	(16)
Static semantics of Java	96	(2)
Transition rules for Java	98	(8)
Thread invariants	106	(5)
Java is type safe	111	(28)
Structural properties of Java runs	111	(6)
Unreachable statements	117	(4)
Rules of definite assignment	121	(5)
Java is type safe	126	(13)
Part II. Compilation of Java: The Trustful JVM
The JVMI submachine	139	(8)
Dynamic semantics of the JVMI	139	(3)
Compilation of JavaI	142	(5)
The procedural extension JVMc of JVMI	147	(8)
Dynamic semantics of the JVMc	147	(6)
Compilation of Javac	153	(2)
The object-oriented extension JVM of JVMc	155	(4)
Dynamic semantics of the JVM	155	(2)
Compilation of Java	157	(2)
The exception-handling extension JVM of JVM	159	(6)
Dynamic semantics of the JVM	159	(4)
Compilation of Java	163	(2)
Executing the JVMN	165	(2)
Correctness of the compiler	167	(42)
The correctness statement	167	(11)
The correctness proof	178	(31)
Part III. Bytecode Verification: The Secure JVM
The defensive virtual machine	209	(14)
Construction of the defensive JVM	210	(1)
Checking JVMI	210	(3)
Checking JVMc	213	(1)
Checking JVM	214	(5)
Checking JVM	219	(2)
Checking JVMN	221	(1)
Checks are monotonic	222	(1)
Bytecode type assignments	223	(50)
Problems of bytecode verification	224	(7)
Successors of bytecode instructions	231	(5)
Type assignments without subroutine call stacks	236	(6)
Soundness of bytecode type assignments	242	(10)
Certifying compilation	252	(21)
The diligent virtual machine	273	(16)
Principal bytecode type assignments	273	(2)
Verifying JVMI	275	(4)
Verifying JVMc	279	(4)
Verifying JVM	283	(1)
Verifying JVM	283	(3)
Verifying JVMN	286	(3)
The dynamic virtual machine	289	(76)
Initiating and defining loaders	289	(1)
Loading classes	290	(1)
Dynamic semantics of the JVMD	291	(14)
Appendix
A. Executable Models	305	(18)
A.1 Overview	305	(1)
A.2 Java	306	(6)
A.3 Compiler	312	(2)
A.4 Java Virtual Machine	314	(9)
B. Java	323	(12)
B.1 Rules	323	(8)
B.2 Arrays	331	(4)
C. JVM	335	(26)
C.1 Trustful execution	335	(8)
C.2 Defensive execution	343	(1)
C.3 Diligent execution	344	(3)
C.4 Check functions	347	(1)
C.5 Successor functions	348	(1)
C.6 Constraints	349	(2)
C.7 Arrays	351	(4)
C.8 Abstract versus real instructions	355	(6)
D. Compiler	361	(4)
D.1 Compilation functions	361	(2)
D.2 maxOpd	363	(1)
D.3 Arrays	364	(1)
References	365	(2)
List of Figures	367	(4)
List of Tables	371	(2)
Index	373