Cryptology ePrint Archive: Report 2013/513

Enforcing Language Semantics Using Proof-Carrying Data

Stephen Chong and Eran Tromer and Jeffrey A. Vaughan

Abstract: The soundness of language-level reasoning about 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*, i.e., could it have produced by a computation that respects the language semantics? Otherwise, accepting the value may lead 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. 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


[ Cryptology ePrint archive ]