Cryptology ePrint Archive: Report 2013/513

Enforcing Language Semantics Using Proof-Carrying Data

Stephen Chong and Eran Tromer and Jeffrey A. Vaughan

Abstract: Sound reasoning about the behavior of programs relies on program execution adhering to the language semantics. However, in a distributed computation, when a value is sent from one party to another, the receiver faces the question of whether the value is well-traced: could it have been produced by a computation that respects the language semantics? If not, then accepting the non-well-traced value may invalidate the receiver's reasoning, leading to bugs or vulnerabilities.

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)

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]