Paper 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.