Off-device pre-verification and runtime verification with stack maps

For class files with version numbers ≤ 48 verification must be performed using the alternative verification approach that was defined in this specification since CLDC 1.0.

Verification by Byte Code Typechecker is described below and in the CLDC Byte Code Typechecker Specification (pdf).

Verification by Byte Code Typechecker is deprecated in CLDC 8 and is a candidate to be removed in the next release.

In CLDC 8 the verification by Byte Code Typechecker is optional and may be removed in the next release; if not supported class file versions ≤ 48 are not supported.

The verification approach described in this subsection is significantly smaller and more efficient in resource-constrained devices than the existing Java SE verifier for class file versions ≤ 48. The typical implementation of the verifier requires about ten kilobytes of Intel x86 binary code and less than 100 bytes of dynamic RAM at runtime for typical class files. The verifier performs only a linear scan of the bytecode, without the need of a costly iterative dataflow algorithm.

The CLDC Byte Code Typechecker class file verifier operates in two phases:

1. First, class files have to be run through a preverifier tool in order to remove certain bytecodes and augment the class files with additional StackMap attributes to speed up runtime verification. The preverification phase is typically performed on the development workstation that the application developer uses for writing and compiling the applications.
2. At runtime, the runtime verifier component of the virtual machine uses the additional StackMap attributes generated by the preverifier to perform the actual class file verification efficiently.

The execution of bytecodes in a class file can start only when the class file has successfully passed the runtime verifier.

Runtime class file verification guarantees type safety. Classes that pass the runtime verifier cannot, for example, violate the type system of the Java Virtual Machine or corrupt the memory. Unlike approaches based on code signing, such a guarantee does not rely on the verification attribute to be authentic or trusted. A missing, incorrect or corrupted verification attribute causes the class to be rejected by the runtime verifier.

The CLDC Byte Code Typechecker verifier requires certain methods in class files, that have some non-local branches or exceptions, to contain a special StackMap attribute. The preverifier tool inserts this attribute into normal class files. A transformed class file is still a valid Java class file, with additional StackMap attributes that allow verification to be carried out efficiently at runtime. These attributes are automatically ignored by the class file verifier used in Java Standard Edition, so the solution is fully upward compatible with the Java Virtual Machine of Java Standard Edition. Preprocessed class files containing the extra attributes are approximately 5 to 15 percent larger than the original, unmodified class files.

Additionally, the CLDC Byte Code Typechecker verifier requires that all the subroutines in the bytecodes of class files are inlined. In Java class files, subroutines are special bytecode sequences that contain the bytecodes jsr, jsr_w, ret, or wide ret. The inlining process removes all the jsr, jsr_w, ret, and wide ret bytecodes from all the methods in class files, replacing these instructions with semantically equivalent bytecode. The inlining process makes runtime verification significantly easier and faster.

Verification process

Below is a more detailed description of the two-phase verification process (further details are provided in the CLDC Byte Code Typechecker Specification (pdf)):

Phase 1: Preverification (off-device)

The preverification tool provided with the CLDC Byte Code Typechecker verifier performs the following operations:

• Inline all subroutines and remove all the jsr, jsr_w, ret and wide ret bytecode instructions from the class file. Each method containing these instructions is replaced with semantically equivalent bytecode not containing the jsr, jsr_w, ret, and wide ret bytecodes.
• Add StackMap attributes into class files to facilitate runtime verification. The format and the semantics of the StackMap attribute is defined in the CLDC Byte Code Typechecker Specification (pdf).

In addition, the preverification tool will perform other non-semantical code transformations in order to guarantee that, if passed a valid Java class or interface as defined by the JVMS8, the resulting code will pass in-device verification, provided that the run-time type hierarchy is identical to the type hierarchy that was present during preverification. If passed an invalid Java class or interface, the preverification tool will not produce a class or interface that can pass in-device verification.

Phase 2: In-device verification

The in-device verification algorithm consists of the following steps:

• First, the verifier allocates enough memory for storing the types of all local variables and operand stack items of a given method. The memory size is determined by the maximum number of local variables and maximum stack depth specified in the Code attribute. This memory area is used to store the derived types as the verifier makes a linear pass through the bytecode. This is the only piece of memory the verifier allocates.
• Second, the verifier initializes the derived types to be the type of the this pointer for instance methods, argument types, and an empty operand stack.
• Third, the verifier linearly iterates through each instruction. For each instruction, the following happens:
• If the previous instruction is either unconditional jump (e.g., goto), return (e.g., ireturn), athrow, tableswitch, or lookupswitch, or the current instruction is at the starting byte code offset of an exception handler, there is no direct control flow from the previous instruction. The verifier ignores the current derived types and sets the derived types according to the stack map entry recorded for the current instruction. If the current instruction does not have a stack map entry the verifier reports an error.
• If the previous instruction is not unconditional jump (e.g., goto), return (e.g., ireturn), athrow, tableswitch, or lookupswitch, there is direct control flow from the previous instruction. The verifier checks if there is a stack map entry recorded for the current instruction. If there is, the verifier attempts to match the derived types with the recorded stack map entry. If the recorded types are of the same or a more general type than the derived types, the derived types are set to be the recorded types. Otherwise, the verifier reports an error.
• If the current instruction is in the scope of an exception handler (try block), the derived types are matched against the stack map entry that corresponds to the starting bytecode offset of the exception handler. The verifier reports an error if there is not a stack map entry that corresponds to the starting bytecode offset of the exception handler.
• The verifier then attempts to match the derived types with what is expected by the instruction. The iadd instruction, for example, expects the top two operand stack items to be integers. The derived types are then modified according to what the instruction does. The iadd instruction, for example, pops two integers off the operand stack and pushes an integer result onto the operand stack.
• Finally the verifier attempts to match the derived types with any stack map entries recorded for any successor instructions that do not directly follow the current instruction.
• Finally, the verifier makes sure that the last instruction in the method is a unconditional jump (e.g., goto), return (e.g., ireturn), athrow, tableswitch, or lookupswitch. Otherwise it reports a verification error: the control flow falls through the end of the method.

In addition to the steps discussed above, the in-device verifier must perform an additional check: the verifier must distinguish newly allocated objects from those on which a constructor has been invoked. It must make sure that constructors are invoked exactly once on an object allocated by a new instruction at a given bytecode offset, that the only legal operation on newly allocated objects is to invoke its constructor, and that there are no newly allocated objects in local variables or on the operand stack when a backward branch may be taken.

Stack map attribute definition

The CLDC Byte Code Typechecker runtime verifier requires the Java class files to contain special attributes. Because these attributes describe the types of local variables and operand stack items, all of which reside on the interpreter stack, the attribute is known as a "stack map."

Each StackMap attribute consists of multiple entries, with each entry recording the types of local variables and operand stack items at a given bytecode offset.

The StackMap attribute is a sub-attribute of the Code attribute. See chapter §4.7.3 of the JVMS for a detailed description of the Code attribute and how the stack map attribute fits in as part of the Code attribute.

Refer to the CLDC Byte Code Typechecker Specification (pdf) for the formal definition of the StackMap attribute.