VEP: a virtual machine for extended proof-carrying code

One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related methods is the difficulty in communicating the proofs which are inherently large. One way to alleviate this problem is to transmit, instead, a proof generator for the program in question in a generic extended PCC framework (EPCC). The EPCC needs to provide the execution of the proof generator at the consumer side in a secure manner. The ability to securely run arbitrary untrusted proof generator is a challenging problem. We explore the design of a small and safe virtual machine (VEP) which provides the EPCC with a robust security guarantee. The VEP is a minor TCB extension of less than 300 lines of code which works as a safe execution environment and brings about a practical solution to the common security and resource management issues. Categories and Subject Descriptors

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: Heidar Pirzadeh, Danny Dubé
• Keywords: CCS 2008, Generic Extended Pcc, Proof Generator, Security Privacy, Untrusted Proof Generator