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}
}