Paper Info
Title
A portable Virtual Machine target for Proof-Carrying Code
Abstract
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.
Year
DOI
Venue
2005
10.1145/858570.858573
Sci. Comput. Program.
Keywords
Field
DocType
code consumer,proof-carrying code,required proof,efficient just-in-time compilation,virtual machine,certified code,safety verification,code producer,target machine,portable virtual machine target,just-in-time compilation,just in time compiler,work in progress
Unreachable code,Threaded code,Computer science,Source code,Redundant code,Code generation,Real-time computing,Proof-carrying code,Tracing just-in-time compilation,Dead code
Journal
Volume
Issue
ISBN
57
3
1-58113-655-2
Citations 
PageRank 
References 
4
0.45
5
Authors
6
Name
Order
Citations
PageRank
Michael Franz1144499.50
Deepak Chandra215912.08
Andreas Gal325115.91
Vivek Haldar41209.84
Fermín Reig5141.77
Ning Wang611912.03