Virtual Machines (VMs) and Proof-Carrying Code (PCC) are two
techniques that have been used independently to provide safety for
(mobile) code. Existing virtual machines, such as the Java VM, have
several drawbacks: First, the effort required for safety
verification is considerable. Second and more subtly, the need to
provide such verification by the code consumer inhibits the amount
of optimization that can be performed by the code producer. This in
turn makes just-in-time compilation surprisingly expensive.
Proof-Carrying Code, on the other hand, has its own set of
limitations, among which are the sizes of the proofs and the fact
that the certified code is no longer machine-independent. In this
paper, we describe work in progress on combining these approaches.
Our hybrid safe-code solution uses a virtual machine that has been
designed specifically to support proof-carrying code, while
simultaneously providing efficient just-in-time compilation and
target-machine independence. In particular, our approach reduces the
complexity of the required proofs, resulting in fewer proof
obligations that need to be discharged at the target machine.
