work on Java bytecode verification

The following paper on Java bytecode verification is available from URL:

        A Type System for Java Bytecode Subroutines

            Raymie Stata and Martin Abadi

  Java is typically compiled into an intermediate language, JVML, 
  that is interpreted by the Java Virtual Machine. Because mobile 
  JVML code is not always trusted, a bytecode verifier enforces static 
  constraints that prevent various dynamic errors. Given the importance 
  of the bytecode verifier for security, its current descriptions 
  are inadequate. This paper proposes using typing rules to describe 
  the bytecode verifier because they are more precise than prose, 
  clearer than code, and easier to reason about than either. 

  JVML has a subroutine construct used for the compilation of Java's 
  try-finally statement. Subroutines are a major source of complexity 
  for the bytecode verifier because they are not obviously last-in/first-out 
  and because they require a kind of polymorphism. Focusing on subroutines, 
  we isolate an interesting, small subset of JVML. We give typing 
  rules for this subset and prove their correctness. Our type system 
  constitutes a sound basis for bytecode verification and a rational 
  reconstruction of a delicate part of Sun's bytecode verifier. 

  (This paper will be presented at POPL98.) 

Some related results are described below; a paper on these results is
in preparation.

           A Type System for Object Initialization 
        	in the Java Bytecode Language
               Stephen Freund and John Mitchell

  The Java language enables the creation of portable programs which 
  can be transmitted over a network and run safely on any computer.  
  To support this paradigm, Java compilers typically translate a 
  Java program into an intermediate language which can be interpreted 
  by any Java Virtual Machine. This intermediate language is a typed, 
  machine-independent bytecode language, and it is the foundation 
  for many of Java's features, including portability across platforms, 
  dynamic type resolution, and run-time type safety. Despite the 
  bytecode language's important role in the success of Java, there 
  is no precise definition of its type system. We have developed
  a sound type system for a small set of ten bytecode instructions 
  which are sufficient to study the type rules associated with object 
  creation and initialization. Our type system is based on a system 
  previously developed by Stata and Abadi to describe Java bytecode 

  We begin by developing a model of the Java Virtual Machine's bytecode 
  interpreter using the standard framework of structured operational 
  semantics. We then formulate syntax-directed type rules for the 
  bytecodes in our language. We show our type system is sound by 
  proving that any well-typed program will not produce a run-time 
  type error.  

  In addition, we integrate the earlier work of Stata and Abadi to 
  develop a sound type system encompassing both bytecode subroutines 
  and object initialization. We have used the soundness proof for 
  this system to understand the relationship between uninitialized 
  objects and subroutines. This analysis has led to the discovery 
  of a previously unpublished bug in Sun's implementation of the 
  bytecode verifier that allows a program to use an object before 
  it has been initialized. 

  This work is part of an effort to specify a type system for the 
  whole bytecode language. Once this system has been developed, we 
  can formally specify type safety for a compiled Java program and 
  precisely describe the security guarantees which can be made by 
  the verifier. In addition, this study may lead to more expressive, 
  but simpler, typed intermediate languages in the future. 

  Thanks to Martin Abadi and Raymie Stata (DEC SRC) for their assistance 
  on this project. 

Martin Abadi, Stephen Freund, John Mitchell, and Raymie Stata