Checking JVMC - JVM

In this section we re_ne the defensiveSchemeI to the defensiveSchemeC which incorporates the switching machine, and then instantiate this scheme with the new checking function checkC to the defensive JVMC:

defensiveVMC = defensiveSchemeC (checkC ; trustfulVMC ) Since JVMC introduces class _elds and class methods, the defensive JVMC adds a check constraint for each of the new instructions to guarantee the following security properties:

  1. The type of every value stored in a class _eld is compatible with its declared type.
  2. The actual arguments to each class method invocation are compatible with the corresponding formal parameters.
  3. The type of every returned result is compatible with the declared result type.

Environment. Every method has its own maximum operand stack size so that we re_ne maxOpd by an additional method parameter. For this reason maxOpd appears in the class _le component of method declarations.

Rules. Figure below extends the defensiveSchemeI by the switching submachine and by checking constraints on class _elds and methods. A GetStatic instruction can be executed provided the operand stack has su_cient space to push the stored value. The PutStatic instruction requires the popped value to be

Checking JVMC instructions

Checking JVMC instructions

compatible with the _eld type. The InvokeStatic instruction requires that the actual argument types are compatible to the types of the formal parameters of the method. If the method returns a result, enough space must be left to push the result onto the operand stack. Executing a Return instruction requires that the actual type on top of the stack is compatible with the result type of the method and this type must be compatible with the move type as speci_ed by the instruction parameter. In case of a Return without return value, the constraint is satis_ed. (The condition will be sharpened later by the clause endinit for returns from instance initialization methods.)

Of course, the run-time dependent length of the method call invocation stack is and cannot be checked for overow.

[ ] vmv void = True


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

JVM Topics