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. Unfortunately, previous approaches to using PCD required tailoring a specialized predicate for each application, using an inconvenient formalism and with little methodological support.
We connect these two threads by introducing a novel, PCD-based approach to enforcing language semantics in distributed computations. We show how to construct an object-oriented language runtime that ensures that objects received from potentially untrusted parties are well-traced with respect to a set of class definitions. Programmers can then soundly reason about program behavior, despite values received from untrusted parties, without needing to be aware of the underlying cryptographic techniques.
Category / Keywords: applications / computationally-sound proofs, programming language security Date: received 17 Aug 2013, last revised 13 Jan 2014 Contact author: tromer at cs tau ac il Available format(s): PDF | BibTeX Citation Version: 20140114:001018 (All versions of this report) Short URL: ia.cr/2013/513 Discussion forum: Show discussion | Start new discussion