M.Eng. Thesis: Proof-Carrying Data

Thesis supervisors: Prof. Ronald L. Rivest, Prof. Eran Tromer.

Bibliographic information: My M.Eng. thesis at MIT; it was finished on May 21st, 2010. (BibTeX)

This thesis was awarded the Charles and Jennifer Johnson Thesis Award for Outstanding CS M.Eng. Thesis.

Abstract

The security of systems can often be expressed as ensuring that some property is maintained at every step of a distributed computation conducted by untrusted parties. Special cases include integrity of programs running on untrusted platforms, various forms of confidentiality and side-channel resilience, and domain-specific invariants.

We propose a new approach, proof-carrying data (PCD), which sidesteps the threat of faults and leakage by reasoning about properties of a computation’s output data, regardless of the process that produced it. In PCD, the system designer prescribes the desired properties of a computation’s outputs. Corresponding proofs are attached to every message flowing through the system, and are mutually verified by the system’s components. Each such proof attests that the message’s data and all of its history comply with the prescribed properties.

We construct a general protocol compiler that generates, propagates, and verifies such proofs of compliance, while preserving the dynamics and efficiency of the original computation. Our main technical tool is the cryptographic construction of short non-interactive arguments (computationally-sound proofs) for statements whose truth depends on "hearsay evidence": previous arguments about other statements. To this end, we attain a particularly strong proof-of-knowledge property.

We realize the above, under standard cryptographic assumptions, in a model where the prover has black- box access to some simple functionality --- essentially, a signature card.

• The M.Eng. thesis itself, in PDF or PostScript.
  ERRATA: The full proof of Theorem 4.3.1 in Appedix A contains a bug (see Footnote 3 on page 62) that is fixed in this revision, in PDF or PostScript.
• Proof-carrying-data project website.
• Webpage for the ICS'10 conference paper and talk.

Table of Contents

	1 Introduction
		1.1 Motivation
		1.2 Goals
		1.3 Our approach
		1.4 Model and trust
		1.5 Contributions of this thesis
		1.6 Previous approaches to security design
	2 Preliminaries
		2.1 Basic notation
			2.1.1 Strings, relations, and functions
			2.1.2 Distributions
			2.1.3 Computational models
			2.1.4 Feasible and infeasible computation
		2.2 Basic notions
			2.2.1 Computational indistinguishability
			2.2.2 Black-box subroutines and oracles
		2.3 Basic cryptographic primitives
			2.3.1 One-way functions
			2.3.2 Pseudo-random generators
			2.3.3 Pseudo-random functions
			2.3.4 Collision-resistant hashing schemes
			2.3.5 Signature schemes
	3 Related Work
		3.1 Proof systems
		3.2 Probabilistically-checkable proofs
			3.2.1 Alternative models of PCP
		3.3 Interactive proofs
			3.3.1 Zero knowledge
			3.3.2 Proof of knowledge
			3.3.3 Round efficiency
			3.3.4 Communication efficiency
			3.3.5 Verifier efficiency
		3.4 Secure multi-party computation
	4 An Argument System for Hearsay
		4.1 Difficulties and our solution
		4.2 Definition of APHA systems
			4.2.1 Structure of APHA systems
			4.2.2 Properties of APHA systems (intuitive)
			4.2.3 Properties of APHA systems (formal)
		4.3 Construction of an APHA system
		4.4 Correctness of the APHA construction
		4.5 Realizability of an assisted prover
	5 Proof-Carrying Data Systems
		5.1 Compliance of computation
		5.2 Definition of PCD systems
			5.2.1 Structure of PCD systems
			5.2.2 Properties of PCD systems (intuitive)
			5.2.3 Properties of PCD systems (formal)
			5.2.4 More on recursive time and PCD prover's complexity
		5.3 Construction of a PCD system
		5.4 Correctness of the PCD construction
	6 Applications and Design Patterns
	7 Conclusions and Open Problems
	A Full Proof of Security for APHA Systems
		A.1 A probability lemma
		A.2 Universal arguments with adaptive provers
		A.3 Achieving non-interaction through a SIR oracle
		A.4 Forcing a prover to query the witness
	B Full Proof of Security for PCD Systems
		B.1 Review of goals
		B.2 Details of proof
	Statement of Originality
	Bibliography