[Prev][Next][Index][Thread]

New book on Bytecode verification for Java/JVM

R. Staerk, J. Schmid, E. Boerger

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

Springer-Verlag, June 2001. 381 pp. 
CD-ROM. Hardcover. ISBN 3-540-42088-6

Abstract: 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 AsmGofer executable models and additional lecturing material can be
downloaded from

  http://www.inf.ethz.ch/~jbook/

System requirements: Windows 95, 98, 2000, NT, ME or Linux on 200MHz
Intel (or Intel compatible) CPU, or Solaris on Sun-Sparc 20, Sun Ultra.

To order the book:

  http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42088-6
  http://www.amazon.de/exec/obidos/ASIN/3540420886/

Table of contents:

1.   Introduction
1.1  The goals of the book
1.2  The contents of the book
1.3  Decomposing Java and the JVM
1.4  Sources and literature

2.   Abstract State Machines
2.1  ASMs in a nutshell
2.2  Mathematical definition of ASMs
2.3  Notational conventions

Part I. Java 

3.   The imperative core Java-I of Java
3.1  Static semantics of Java-I
3.2  Transition rules for Java-I

4.   The procedural extension Java-C of Java-I
4.1  Static semantics of Java-C
4.2  Transition rules for Java-C

5.   The object-oriented extension Java-O of Java-C
5.1  Static semantics of Java-O
5.2  Transition rules for Java-O

6.   The exception-handling extension Java-E of Java-O
6.1  Static semantics of Java-E
6.2  Transition rules for Java-E

7.   The concurrent extension Java-T of Java-E
7.1  Static semantics of Java-T
7.2  Transition rules for Java-T
7.3  Thread invariants

8.   Java is type safe
8.1  Structural properties of Java runs
8.2  Unreachable statements
8.3  Rules of definite assignment
8.4  Java is type safe

Part II. Compilation of Java: The Trustful JVM

9.   The JVM-I submachine
9.1  Dynamic semantics of the JVM-I
9.2  Compilation of Java-I

10.  The procedural extension JVM-C of JVM-I
10.1 Dynamic semantics of the JVM-C
10.2 Compilation of Java-C

11.  The object-oriented extension JVM-O of JVM-C
11.1 Dynamic semantics of the JVM-O
11.2 Compilation of Java-O

12.  The exception-handling extension JVM-E of JVM-O
12.1 Dynamic semantics of the JVM-E
12.2 Compilation of Java-E

13.  Executing the JVM-N 

14.  Correctness of the compiler
14.1 The correctness statement
14.2 The correctness proof

Part III. Bytecode Verification: The Secure JVM

15.  The defensive virtual machine
15.1 Construction of the defensive JVM
15.2 Checking JVM-I
15.3 Checking JVM-C
15.4 Checking JVM-O
15.5 Checking JVM-E
15.6 Checking JVM N
15.7 Checks are monotonic

16.  Bytecode type assignments
16.1 Problems of bytecode verification
16.2 Successors of bytecode instructions
16.3 Type assignments without subroutine call stacks
16.4 Soundness of bytecode type assignments
16.5 Certifying compilation

17.  The diligent virtual machine
17.1 Principal bytecode type assignments
17.2 Verifying JVM-I
17.3 Verifying JVM-C
17.4 Verifying JVM-O
17.5 Verifying JVM-E
17.6 Verifying JVM-N

18.  The dynamic virtual machine
18.1 Initiating and defining loaders
18.2 Loading classes
18.3 Dynamic semantics of the JVM-D

Appendix 

A.   Executable Models
A.1  Overview
A.2  Java
A.3  Compiler
A.4  Java Virtual Machine

B.   Java
B.1  Rules 
B.2  Arrays

C.   JVM
C.1  Trustful execution
C.2  Defensive execution
C.3  Diligent execution
C.4  Check functions
C.5  Successor functions
C.6  Constraints
C.7  Arrays
C.8  Abstract versus real instructions

D.   Compiler
D.1  Compilation functions
D.2  maxOpd
D.3  Arrays 

References
List of Figures
List of Tables
Index

************************************************************************