Verifying JVMC - JVM

We apply the verifySchemeI to all methods of a given class or interface and instantiate the resulting diligentScheme with the trustfulVMC and with the successor and check functions succC , checkC .

In JVMC a class or interface must be successfully veri_ed before it is initialized. The veri_er has to verify every method of a class. If each method invocation and return can be guaranteed to be type correct, the veri_er can check each method individually. The type correctness of method invocation is taken care of by starting the veri_cation of the method with the types of its formal parameters; the type correctness of returning from a method is veri_ed by checking for return instructions the top of the operand type frame against the return type of the method. In this way the diligentVMC can be obtained from the diligentVMI by applying the bytecode veri_cation to all methods of the class to be veri_ed.

State. In order to make our model close to an executable model, instead of checking all methods in parallel we choose a not furthermore speci_ed but _xed order for method veri_cation. This requires the following extension of the state of diligentVMI . A new dynamic function verifyClass contains the class to be veri_ed. The dynamic function verifyMeths holds all methods of the class to be veri_ed.

Veri_cation starts with the _rst method of verifyMeths, abbreviated as methv . We leave the particular ordering of verifyMeths unspeci_ed, as well as the corresponding functions top, drop, null which are used to walk through verifyMeths in an attempt to exhaust it. Veri_cation succeeds, if all instructions of all methods are veri_ed. Rules. We de_ne a scheme for the diligent JVMC which iterates a re_nement of the veri_er of the diligent JVMI. As long as a class is not veri_ed (and the veri_cation did not fail) the veri_cation process proceeds. After the class has been veri_ed, the VM continues with the trustful code execution.

The top level guard isChecked tests whether there is still some instruction in some method of the class to verify.

The verifySchemeC is the verifySchemeI extended by resetting the veri_er, once a method of the class has been successfully veri_ed, for the veri_cation of the next method to verify, and by updating the veri_cation status of the class to Linked once all its methods have been veri_ed successfully.

Whenever a method is veri_ed, the veri_er drops it from the still to be veri_ed methods in verifyMeths and resets its dynamic functions to their initial state for the next method to be veri_ed using the following initVerify rule. This rule formalizes the assumptions made for the initial veri_er state in diligentVMI .

The type correctness of method invocation is guaranteed by using the argument types of the method as initial assignments for the type registers, described by a static function formals, to be re_ned for instance methods and constructors: formals(c=m) = if isStatic(c=m) then makeRegs(argTypes(c=m))

We have to extend the switchVMC of the trustfulVM in order to support verifying of classes before class initialization. When the trustful VM switches to the initialization of a class which has not yet been linked, the diligent VM triggers a submachine to link this class. For this purpose the universe ClassState is extended.

data ClassState = : : : j Referenced

A class can be in one of the states Referenced, Linked, Initialized or Unusable. We assume in this chapter that at the beginning all classes are referenced.

Linking a class or interface c involves linking (i.e., verifying and preparing) c, its direct superclass and its direct superinterfaces. If the superclass of c and all its direct superinterfaces are already linked or if c is Object, the veri_cation of c is started. Otherwise the linking submachine is triggered for one of the still to be linked superinterfaces or the superclass of c|unless a class circularity error is detected. Due to the _niteness of the class inheritance, the recursive calls of the submachine linkClass terminate. If any of the superclasses or superinterfaces of c is c itself, then the class hierarchy is cyclic and the VM stops with an error.

There is a preparatory test for starting the veri_cation, namely checking the format of the class _le and the static constraints for the method bodies.

Preparing the class involves creating its static _elds and initializing those
_elds to their standard values.

In the diligent VM, only after a class has been successfully veri_ed and prepared for initialization, it is initialized by executing its <clinit> method.


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

JVM Topics