An authenticated data structure (ADS) is a data structure whose
operations can be carried out by an untrusted *prover*, the
results of which a *verifier* can efficiently check as
authentic. This is done by having the prover produce a
compact proof that the verifier can check along with each query result.
ADSs thus support outsourcing data maintenance and processing tasks
to untrusted servers without loss of integrity. Past work on ADSs
has focused on particular data structures (or limited
classes of data structures), one at a time, often with support only
for particular operations. This
paper presents a generic method, using a simple extension
to a ML-like functional programming language we call lambdaAuth
with
which one can program authenticated operations over any data
structure constructed from standard type constructors, including
recursive types, sums, and products. The programmer writes the data
structure largely as usual; it can then be compiled to code
to be run by the prover and verifier. Using a formalization of
lambdaAuth
we prove that all well-typed lambdaAuth programs result in code that is
secure under the standard cryptographic assumption of
collision-resistant hash functions. We have implemented
our approach as an extension to the OCaml compiler, and have used it
to produce authenticated versions of many interesting data
structures including binary search trees, red-black trees, skip
lists, and more. Performance experiments show that our approach is
efficient, giving up little compared to the hand-optimized data
structures developed previously.

[ .pdf ] [ full version (pdf) ] [ slides ] [ code ]

@INPROCEEDINGS{miller14gpads, AUTHOR = {Andrew Miller and Michael Hicks and Jonathan Katz and Elaine Shi}, TITLE = {Authenticated Data Structures, Generically}, BOOKTITLE = {Proceedings of the {ACM} Conference on Principles of Programming Languages (POPL)}, MONTH = JAN, YEAR = 2014, NOTE = {To appear} }