Checking JVMO - JVM

In this section we extend the defensive machine to handle also constraints for object-oriented language features. The extension adds the checking counterpart to the extension of the trustful execVMC to the trustful execVMO: new rules are added for checking each of the object-oriented instructions executed by execVMO. Therefore we de_ne the defensive JVMO as an instantiation of the defensive SchemeC . defensiveVMO = defensiveSchemeC (checkO; trustfulVMO)

For checking JVMO instructions, the compatibility notion must be re_ned, to take the inheritance hierarchy into account, and it must be guaranteed that only _elds of initialized instances may be accessed and only methods of initialized instances may be called. The defensive JVMO guarantees the following safety properties, in addition to the ones of the JVMC:

  1. The type of every target of an object access or of a method call is compatible with the required type.
  2. The argument of any InstanceOf or Checkcast operation is compatible with Object.

With respect to object creation and initialization the defensive JVM guarantees the following security properties:

  1. A newly created object is regarded as un-initialized. An object becomes fully initialized when the constructor of class Object is invoked. The invocation of another constructor makes an object partially initialized.
  2. Constructors are invoked on un-initialized or partially initialized objects only. If an object is un-initialized, then the invoked constructor is in the class of the object. If an object is partially initialized, then the invoked constructor is in the same class as the invoking constructor or in the direct superclass.
  3. When a constructor returns, it has invoked a constructor either in the same class or in the superclass.
  4. Field accesses are performed on fully initialized objects only.
  5. Instance methods are invoked on fully initialized objects only.
  6. References to not fully initialized objects are neither stored in class _elds, nor in instance _elds, nor in array elements. References to not fully initialized objects cannot be passed as arguments to methods and are not returned by methods.
  7. References to not fully initialized objects, however, can be moved from the operand stack to local registers and vice versa. They can also be compared with other references using the operator `=='. The Checkcast and Instanceof instructions are applied to fully initialized objects only.

What does it mean that an object is fully initialized? It means that there is a sequence of constructor calls for the object, starting with a constructor of the class of the object, such that each constructor in the sequence, except for the constructor of class Object, calls either another constructor of the same class or a constructor of its direct superclass before the instance members of the object are accessed. Fully initialized, however, does not mean that all constructor calls in the sequence do terminate normally. In a deviate program, it may happen that a constructor stores the value of this in a global variable and throws an exception afterwards. The exception can be caught and later the object can be used from the global class variable in its insecure state. Nevertheless, the object is regarded as fully initialized because all constructors of the type hierarchy have been called.

The JLS does not allow direct or indirect recursive constructor invocations (see [18, x8.6.5]), because cycles through explicit constructor invocations can easily be detected in Java source code. On the bytecode level, however, such cycles are not so obvious, because an argument expression of a constructor can contain a subexpression which creates a new instance of the same class and hence uses the same constructor. Therefore recursive constructor calls are allowed in bytecode programs.

Types. The above listed constraints require the introduction of new type descriptors. Since the new types are later also used in the bytecode veri_er, we call them

verify types.

The primitive verify types are identical with the corresponding word types. The descriptor Null represents its only value null and is compatible with any reference types. Reference types are class types, interface types, array types and Null. Initialized instances of a class c are denoted simply by the name itself. The type descriptor (c; pc)new is the type of an un-initialized object created at code index pc. Partially initialized objects are of type InInit. The types (c; pc)new and InInit are not considered as reference types. The type descriptor unusable is added in order to have a topmost element in the set of verify types. Every value can be of type unusable. The compatibility relation is de_ned on verify types _, _ as follows:

De_nition . For verify types _ and _ the relation _ v _ is true, i_ one of the following conditions is true:

_ = _ , or _ and _ are reference types and _ _ _ , or _ = unusable.

Since the types (c; pc)new and InInit are not reference types, they are compatible with themselves and unusable only.

The Load; Store and Return instructions are allowed to move class references and null. The instructions Load and Store are even allowed to move uninitialized objects, the Return instruction not. Therefore the notion of compatibility between veri_er types and move types is extended as follows. Let c be any reference type:

The de_nition of the predicate isHigh is re_ned to include also the type unusable. Hence a valid type sequence is not allowed to begin with the type unusable. isHigh(t) = (t = highLong _ t = highDouble _ t = unusable)

State. We have to distinguish un-initialized object, partially initialized objects and initialized objects. Therefore we introduce a new type InitState: data InitState = New(Pc) j InInit j Complete

We keep track of the initialization status of a reference in the dynamic function initState: initState:Ref ! InitState

A newly created un-initialized object of class c with reference r has initialization state New(pc), where pc is the code index of the instruction

New. If an initializer method declared in class c is called on r , the value of initState(r) is updated to InInit. When the initialization method of class Object is called, the partially initialized object r gets fully initialized and we update initState(r) to Complete (see Figure below).
References in the stack and in the registers are tagged with reference.

The universe WordType is extended by reference. data WordType = : : :

j reference

The heap contains the type information about references. Thus we have to extend our de_nition for type on words:

Checking JVMO instructions

Checking JVMO instructions

Rules. The execVMO rules are lifted for GetField, PutField, InvokeSpecial and InvokeVirtual onto the new state representation. Fig. above extends the check function of JVMC for these instructions. The conditions are similar to the ones for the class counterparts in the object-based language, additionally the type of the target reference must be an initialized subtype of the instruction parameter. The instructions InstanceOf and Checkcast both check whether the top of the stack denotes an initialized reference type. The instruction New(c) requires that there is still space on the type operand stack for the type (c; pc)new of a newly created un-initialized object of class c. When execVMO executes an instruction New(c) and creates a new reference r , then the initialization state of r has to be set in the following way: initState(r ) := New(pc) It remains to explain the conditions for calling and for returning from instance initialization methods. To initialize objects an <init> method has to be called. The target object must be un-initialized. The actual argument types must be compatible with the formal parameters.

If the target object is typed by (c; pc)new (the initialization method is called the _rst time for the target object), then the called method must be declared in the class c. Otherwise|the target object is typed by InInit|the machine executes initialization code. Then, the called method must either be declared in the same class or in the immediate super class. This is captured by the predicate initCompatible that is speci_ed as follows:

Pushing a new JVMO frame

Pushing a new JVMO frame

Whenever an initialization method is called, the dynamic function initState will be updated. This updating is performed in the switchVM , namely as follows. An object becomes initialized, when the initialization method of the root of the inheritance tree is called. Figure above re_nes the de_nition of pushing the type frame on the type stack. If an Object=<init> frame is pushed, initState is updated to Complete. If a c=<init> frame is pushed with c 6= Object, then the function initState is updated to InInit. Note that this update changes the initState of the reference|from New(pc), assigned to it when the reference has been created|only at the _rst constructor call.

Each <init> method should invoke another <init> method of the same class or of its direct superclass. Therefore, we assume that an <init> method keeps its target object in register 0. We forbid that it uses the instruction Store( ; 0) to store a di_erent value in register 0. Hence, at the end, when an <init> method returns and register 0 has a type di_erent from InInit, we know that it has called another <init> method. Therefore the check for the Return instruction is re_ned in checkO by the following condition:


All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd DMCA.com Protection Status

JVM Topics