TY - GEN

T1 - Authenticated data structures, generically

AU - Miller, Andrew

AU - Hicks, Michael

AU - Katz, Jonathan

AU - Shi, Elaine

PY - 2014/2/11

Y1 - 2014/2/11

N2 - 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 operation's 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 λ• (lambda-auth), with which one can program authenticated operations over any data structure defined by standard type constructors, including recursive types, sums, and products. The programmer writes the data structure largely as usual and it is compiled to code to be run by the prover and verifier. Using a formalization of λ• we prove that all well-typed λ• programs result in code that is secure under the standard cryptographic assumption of collision-resistant hash functions. We have implemented λ• 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.

AB - 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 operation's 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 λ• (lambda-auth), with which one can program authenticated operations over any data structure defined by standard type constructors, including recursive types, sums, and products. The programmer writes the data structure largely as usual and it is compiled to code to be run by the prover and verifier. Using a formalization of λ• we prove that all well-typed λ• programs result in code that is secure under the standard cryptographic assumption of collision-resistant hash functions. We have implemented λ• 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.

KW - authenticated data structures

KW - cryptography

KW - programming languages

KW - security

UR - http://www.scopus.com/inward/record.url?scp=84893481888&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84893481888&partnerID=8YFLogxK

U2 - 10.1145/2535838.2535851

DO - 10.1145/2535838.2535851

M3 - Conference contribution

AN - SCOPUS:84893481888

SN - 9781450325448

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 411

EP - 423

BT - POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

T2 - 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014

Y2 - 22 January 2014 through 24 January 2014

ER -