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

Robert F. Stärk, Joachim Schmid, Egon Börger3540420886, 9783540420880

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.

---

Table of contents :
Introduction……Page 10
The goals of the book……Page 11
The contents of the book……Page 12
Decomposing Java and the JVM……Page 16
Sources and literature……Page 20
ASMs in a nutshell……Page 24
Mathematical definition of ASMs……Page 27
Notational conventions……Page 36
Part I. Java……Page 38
Static semantics of JavaI……Page 42
Transition rules for JavaI……Page 48
Static semantics of JavaC……Page 56
Transition rules for JavaC……Page 72
Static semantics of JavaO……Page 80
Transition rules for JavaO……Page 89
Static semantics of JavaE……Page 96
Transition rules for JavaE……Page 98
The concurrent extension JavaT of JavaE……Page 104
Static semantics of JavaT……Page 105
Transition rules for JavaT……Page 107
Thread invariants……Page 115
Structural properties of Java runs……Page 120
Unreachable statements……Page 126
Rules of definite assignment……Page 130
Java is type safe……Page 135
Part II. Compilation of Java: The Trustful JVM……Page 144
Dynamic semantics of the JVMI……Page 148
Compilation of JavaI……Page 151
Dynamic semantics of the JVMC……Page 156
Compilation of JavaC……Page 162
Dynamic semantics of the JVMO……Page 164
Compilation of JavaO……Page 166
Dynamic semantics of the JVME……Page 168
Compilation of JavaE……Page 172
Executing the JVMN……Page 174
The correctness statement……Page 176
The correctness proof……Page 187
Part III. Bytecode Verification: The Secure JVM……Page 214
The defensive virtual machine……Page 218
Checking JVMI……Page 219
Checking JVMC……Page 222
Checking JVMO……Page 223
Checking JVME……Page 228
Checking JVMN……Page 230
Checks are monotonic……Page 231
Bytecode type assignments……Page 232
Problems of bytecode verification……Page 233
Successors of bytecode instructions……Page 240
Type assignments without subroutine call stacks……Page 245
Soundness of bytecode type assignments……Page 251
Certifying compilation……Page 261
Principal bytecode type assignments……Page 282
Verifying JVMI……Page 284
Verifying JVMC……Page 288
Verifying JVME……Page 292
Verifying JVMN……Page 295
Initiating and defining loaders……Page 298
Loading classes……Page 299
Dynamic semantics of the JVMD……Page 300
Overview……Page 314
Java……Page 315
Compiler……Page 321
Java Virtual Machine……Page 323
Rules……Page 332
Arrays……Page 340
Trustful execution……Page 344
Defensive execution……Page 352
Diligent execution……Page 353
Check functions……Page 356
Successor functions……Page 357
Constraints……Page 358
Arrays……Page 360
Abstract versus real instructions……Page 364
Compilation functions……Page 370
maxOpd……Page 372
Arrays……Page 373
References……Page 374
List of Figures……Page 376
List of Tables……Page 380
Index……Page 382