Proof-Carrying Data (PCD) is a recently-introduced cryptographic mechanism that allows messages in a distributed computation to be accompanied by proof that the message, and the history leading to it, complies with a specified predicate. Using PCD, a verifier can be convinced that the predicate held throughout the distributed computation, even in the presence of malicious parties, and at a verification cost that is independent of the size of the computation producing the value. With a suitable choice of predicate, a program may use PCD to check that values received from the network are well-traced. Unfortunately, previous approaches to using PCD required tailoring a specialized predicate for each application, using an inconvenient formalism and with little methodological support.
This work introduces a novel, PCD-based approach to enforcing language semantics in a distributed computation. We show how to construct a runtime, for an object-oriented language, which ensures that objects received from potentially untrusted parties are well-traced with respect to any prescribed class definitions. This means programmers can analyze language-level properties of distributed programs in a trusted setting, and then use the runtime to generically enforce the same properties in the presence of malicious parties, without needing to be aware of the the underlying cryptographic techniques.Category / Keywords: applications / computationally-sound proofs, programming language security Date: received 17 Aug 2013 Contact author: tromer at cs tau ac il Available format(s): PDF | BibTeX Citation Version: 20130821:012023 (All versions of this report) Discussion forum: Show discussion | Start new discussion