The defensive virtual machine

In this chapter we lift the trustfully executing machine of Part II to a defensive machine which checks each instruction before its execution to satisfy certain constraints about types, resource bounds, etc., guaranteeing correct execution in such a way that if the defensive VM executes bytecode successfully, then also the trustful VM does so with the same semantical effect. Our goal here is to prepare the description of the bytecode verifier, to be given in the next chapters, by a transparent definition of the verification functionality, namely in terms of run-time checks of the safe executability of single instructions. We formulate these checking conditions in terms of the types of values instead of values themselves so that they can be adapted in the next two chapters to link-time verifiable properties.