ABSTRACT

We are investigating how clients can use computer resources without having to trust (meaning assume) that those resources operate correctly. For example: Can we outsource computation to servers if the servers are not guaranteed to return the right answer? Can we build a distributed storage system that works even if _all_ of the machines misbehave?  Can we build a network if we cannot trust that the routers will forward properly? These are critical questions in high-assurance regimes.

Our funded research over the last few years has established, over several inquiries, that these questions have affirmative answers. This talk will cover several of these inquiries.

First, I will describe a system for _verified computation_: one machine specifies a computation to another one and then, without executing the computation, checks that the other machine carried it out correctly. It has long been known that (1) probabilistically checkable proofs (PCPs) offer highly principled and powerful solutions in theory; and (2) these solutions are wildly impractical (trillions of CPU-years or more to verify simple computations). Yet, we have challenged (2). We have done new theoretical work to improve performance by over 20 orders of magnitude and to verify arbitrary computations expressed in a high-level language. We have a parallel GPU-based implementation of the system and a compiler to go from computations in a high-level language to executables that implement the protocol entities. The resulting system is not quite ready for the big leagues, but it is close, and it suggests that in the near future, PCPs could be a real tool for building secure systems. Since PCPs offer unconditional (and hence extremely principled  and strong) guarantees, this is a very exciting development.

Second, I will describe a cloud storage system that tolerates buggy or malicious behavior by any number of clients or servers, yet it provides guarantees to correct clients. Put differently, this system assumes radically less than any prior system about the correctness of participating hosts. 

Third, and time permitting, I will describe a new networking primitive, called a Path Verification Mechanism (PVM). The purpose of a PVM is to enforce the network policies of the entities along a communication path. For instance, users may want to choose providers whom they trust to be

discreet, or a receiver may want traffic destined to it to travel through an intrusion detection service; the PVM enforces these considerations even if the forwarders in the network misbehave.