Paper 2013/513

Enforcing Language Semantics Using Proof-Carrying Data

Stephen Chong, 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.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Preprint. MINOR revision.
Keywords
computationally-sound proofsprogramming language security
Contact author(s)
tromer @ cs tau ac il
History
2014-01-14: revised
2013-08-21: received
See all versions
Short URL
https://ia.cr/2013/513
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2013/513,
      author = {Stephen Chong and Eran Tromer and Jeffrey A.  Vaughan},
      title = {Enforcing Language Semantics Using Proof-Carrying Data},
      howpublished = {Cryptology ePrint Archive, Paper 2013/513},
      year = {2013},
      note = {\url{https://eprint.iacr.org/2013/513}},
      url = {https://eprint.iacr.org/2013/513}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.