Checking JVME - JVM

This section adds the checking counterpart to the extension of the trustful execVMO to the trustful execVME, namely by checking each of the error handling instructions.

Checking JVME instructions

Checking JVME instructions

The defensive JVME assures the following security properties:

  1. Athrow is only applied on throwable objects.
  2. Program counters denote always valid addresses.

These aspect can be guaranteed if we keep track of the use of references and program counters in the store.

Types. The instructions Jsr and Ret push program counters on the stack and load program counters from local variables, respectively. We add the new variant retAddr to our type system.

In the JVM only the Store operation is allowed to move return addresses from the stack into a register. Therefore, we have to extend the corresponding check de_nition for Store.

Rules. The extension of the check function for JVME instructions is given in Figure above. The Athrow instruction requires that the reference on top of the operand stack is an instance of type Throwable. The Jsr instruction pushes retAddr on the type operand stack, provided enough space is left on the stack. The Ret instruction checks whether a retAddr is stored in the accessed location.

Jsr and Ret require to lift the execVME. The Jsr(s) instruction pushes the value (pc +1; retAddr(s)) on the operand stack indicating that pc +1 is a return address for subroutines.

The Ret(x) instruction only takes the _rst component of the register x as its next program counter.

The defensive JVME does not allow computed gotos: only Jsr generates return addresses and pushes them on the stack, only Store can move a return address into a register. The condition on Ret guarantees that only program generated return addresses can be used.

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

JVM Topics