Java and the Java Virtual Machine 1

The origin of this book goes back to the Dagstuhl seminar on Logic for System Engineering, organized during the first week of March 1997 by S. Jiihnichen, J. Loeckx, and M. Wirsing. During that seminar, after Egon Borger's talk on How to Use Abstract State Machines in Software Engineering, Wolfram Schulte, at the time a research assistant at the University of Ulm, Germany, questioned whether ASMs provide anything special as a scientifically well­ founded and rigorous yet simple and industrially viable framework for high­ level design and analysis of complex systems, and for natural refinements of models to executable code. Wolfram Schulte argued, referring to his work with K. Achatz on A Formal Object-Oriented Method Inspired by Fusion and Object-Z [1], that with current techniques of functional programming and of axiomatic specification, one can achieve the same result. An intensive and long debate arose from this discussion. At the end of the week, it led Egon Borger to propose a collaboration on a real-life specification project of Wolfram Schulte's choice, as a comparative field test of purely functional­ declarative methods and of their enhancement within an integrated abstract state-based operational (ASM) approach. After some hesitation, in May 1997 Wolfram Schulte accepted the offer and chose as the theme a high-level specification of Java and of the Java Virtual Machine. Introduction......Page 9 The goals of the book......Page 10 The contents of the book......Page 11 Decomposing Java and the JVM......Page 15 Sources and literature......Page 19 ASMs in a nutshell......Page 23 Mathematical definition of ASMs......Page 26 Notational conventions......Page 35 Part I. Java......Page 37 Static semantics of JavaI......Page 41 Transition rules for JavaI......Page 47 Static semantics of JavaC......Page 55 Transition rules for JavaC......Page 71 Static semantics of JavaO......Page 79 Transition rules for JavaO......Page 88 Static semantics of JavaE......Page 95 Transition rules for JavaE......Page 97 The concurrent extension JavaT of JavaE......Page 103 Static semantics of JavaT......Page 104 Transition rules for JavaT......Page 106 Thread invariants......Page 114 Structural properties of Java runs......Page 119 Unreachable statements......Page 125 Rules of definite assignment......Page 129 Java is type safe......Page 134 Part II. Compilation of Java: The Trustful JVM......Page 143 Dynamic semantics of the JVMI......Page 147 Compilation of JavaI......Page 150 Dynamic semantics of the JVMC......Page 155 Compilation of JavaC......Page 161 Dynamic semantics of the JVMO......Page 163 Compilation of JavaO......Page 165 Dynamic semantics of the JVME......Page 167 Compilation of JavaE......Page 171 Executing the JVMN......Page 173 The correctness statement......Page 175 The correctness proof......Page 186 Part III. Bytecode Verification: The Secure JVM......Page 213 The defensive virtual machine......Page 217 Checking JVMI......Page 218 Checking JVMC......Page 221 Checking JVMO......Page 222 Checking JVME......Page 227 Checking JVMN......Page 229 Checks are monotonic......Page 230 Bytecode type assignments......Page 231 Problems of bytecode verification......Page 232 Successors of bytecode instructions......Page 239 Type assignments without subroutine call stacks......Page 244 Soundness of bytecode type assignments......Page 250 Certifying compilation......Page 260 Principal bytecode type assignments......Page 281 Verifying JVMI......Page 283 Verifying JVMC......Page 287 Verifying JVME......Page 291 Verifying JVMN......Page 294 Initiating and defining loaders......Page 297 Loading classes......Page 298 Dynamic semantics of the JVMD......Page 299 Overview......Page 313 Java......Page 314 Compiler......Page 320 Java Virtual Machine......Page 322 Rules......Page 331 Arrays......Page 339 Trustful execution......Page 343 Defensive execution......Page 351 Diligent execution......Page 352 Check functions......Page 355 Successor functions......Page 356 Constraints......Page 357 Arrays......Page 359 Abstract versus real instructions......Page 363 Compilation functions......Page 369 maxOpd......Page 371 Arrays......Page 372 References......Page 373 List of Figures......Page 375 List of Tables......Page 379 Index......Page 381 Introduction 9 The goals of the book 10 The contents of the book 11 Decomposing Java and the JVM 15 Sources and literature 19 Abstract State Machines 23 ASMs in a nutshell 23 Mathematical definition of ASMs 26 Notational conventions 35 Part I. Java 37 The imperative core JavaI of Java 41 Static semantics of JavaI 41 Transition rules for JavaI 47 The procedural extension JavaC of JavaI 55 Static semantics of JavaC 55 Transition rules for JavaC 71 The object-oriented extension JavaO of JavaC 79 Static semantics of JavaO 79 Transition rules for JavaO 88 The exception-handling extension JavaE of JavaO 95 Static semantics of JavaE 95 Transition rules for JavaE 97 The concurrent extension JavaT of JavaE 103 Static semantics of JavaT 104 Transition rules for JavaT 106 Thread invariants 114 Java is type safe 119 Structural properties of Java runs 119 Unreachable statements 125 Rules of definite assignment 129 Java is type safe 134 Part II. Compilation of Java: The Trustful JVM 143 The JVMI submachine 147 Dynamic semantics of the JVMI 147 Compilation of JavaI 150 The procedural extension JVMC of JVMI 155 Dynamic semantics of the JVMC 155 Compilation of JavaC 161 The object-oriented extension JVMO of JVMC 163 Dynamic semantics of the JVMO 163 Compilation of JavaO 165 The exception-handling extension JVME of JVMO 167 Dynamic semantics of the JVME 167 Compilation of JavaE 171 Executing the JVMN 173 Correctness of the compiler 175 The correctness statement 175 The correctness proof 186 Part III. Bytecode Verification: The Secure JVM 213 The defensive virtual machine 217 Construction of the defensive JVM 218 Checking JVMI 218 Checking JVMC 221 Checking JVMO 222 Checking JVME 227 Checking JVMN 229 Checks are monotonic 230 Bytecode type assignments 231 Problems of bytecode verification 232 Successors of bytecode instructions 239 Type assignments without subroutine call stacks 244 Soundness of bytecode type assignments 250 Certifying compilation 260 The diligent virtual machine 281 Principal bytecode type assignments 281 Verifying JVMI 283 Verifying JVMC 287 Verifying JVMO 291 Verifying JVME 291 Verifying JVMN 294 The dynamic virtual machine 297 Initiating and defining loaders 297 Loading classes 298 Dynamic semantics of the JVMD 299 Appendix 313 Executable Models 313 Overview 313 Java 314 Compiler 320 Java Virtual Machine 322 Java 331 Rules 331 Arrays 339 JVM 343 Trustful execution 343 Defensive execution 351 Diligent execution 352 Check functions 355 Successor functions 356 Constraints 357 Arrays 359 Abstract versus real instructions 363 Compiler 369 Compilation functions 369 maxOpd 371 Arrays 372 References 373 List of Figures 375 List of Tables 379 Index 381 Java,Definition,Validation,Verification Java, JVM

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

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 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 for their work a complete and transparent definition and an executable model of the language and of the virtual machine underlying its intended implementation The notion of Abstract State Machines (ASMs), defined in [20], captures in mathematically rigorous yet transparent form some fundamental operational intuitions of computing, and the notation is familiar from programming practice and mathematical standards.