Justin's Poster at FCRC

Justin Thaler, a student I'm advising (or, quite arguably, the other way around), will be at the poster session for STOC, ready to talk about a bunch of his currently-under-submission work on streaming interactive proofs, including the most recent, Practical Verified Computation with Streaming Interactive Proofs (with me and Graham Cormode).  Justin has been working for some time on streaming problems with the following motivation:  you're gathering a big data set that you're going to store, and compute on, on the cloud.  How do you trust that the cloud is going to give you the right answer?  A natural theorists' answer is via an interactive proof, and here the natural limitation is to a streaming verifier:  a verifier that sees all the data initially, forwarding it to the cloud, but can't store it all due to limited memory, including later when the prover (the cloud) wants to prove that it's done the computation correctly.

We didn't initiate these models, to be sure.  There's now been a chain of work, including the "annotations" paper by Chakrabarti, Cormode, and McGregor, which was a primary motivator.  For Justin's other theoretical work, see the arxiv version of his ESA paper (with me and Cormode, journal version under submission) and this paper of his with Cormode and Yi (under submission).

Some time ago I challenged Justin to figure out if this work on streaming verifiers was "practical" for real-world cloud settings, and if not, why not.  The outcome (so far) is the Practical Verified Computation with Streaming Interactive Proofs paper.  We're not the only ones to have noticed that perhaps interactive proofs are ready for deployment in these kinds of real-world systems.  Apparently, there was a recent HotOS paper, Toward Practical and Unconditional Verification of Remote Computations, on the same theme, by real-live honest-to-goodness systems people.  I'll avoid (biased) comparisons, and leave that to others.

But I can highlight some of what Justin's done.  He's considered and implemented both special-purpose "building-block" functions, like self-joins (or F_2 computations), and a fully general approach for arbitrary computations based on the "Muggles" protocol (interactive proofs with polynomial time provers).  He's considered and implemented both non-interactive protocols, where the prover sends a single message that includes both the answer and the verification, and interactive protocols, where the prover and verifier have a multi-round conversation to verify the result. Along the way he's had to come up with several "engineering" improvements (with some strong theoretical foundations) to make things practical, including a clever use of FFTs for the non-interactive protocols that seems new, and adopting the approach of linearizing polynomials from previous work on interactive proofs to improve efficiency to these protocols.  

Our experience, I think, shows that with some significant engineering, interactive proof systems in the streaming verifier setting are ready for real systems.  So if you get a chance stop by and ask Justin more about the work.  He's eager to talk about it!