Authenticated Data Structures (Generically)

This blog post is the first in my series on secure computation and will be presented in two parts. It briefly introduces some work my collaborators and I published this year, which illustrates a pleasant application of programming languages ideas to cryptographic computation.

In particular, we develop a general-purpose technique for programming authenticated data structures (ADSs) (an idea that this post will introduce). Our approach is implemented as a small extension to a general-purpose programming language. With this extension, we can establish security by typing: any type-correct program (which is a data structure implementation) implemented in our language will be secure. Thus we perform the proof once and for all, for all possible data structures, rather than having to prove security for each variation. Our approach exploits the compositional nature at the core of formal PL semantics and type systems to factor out the tedious part (the data structure logic) to focus on the security-relevant part (the use of cryptographic primitives). The proof ends up being pleasingly straightforward. The idea of security by typing is a powerful one that shows up frequently in PL-inspired work on security.

The remainder of this post — part 1 — introduces the idea of ADSs and why we want general-purpose support for them. The PL ideas show up in part 2, which will introduce our approach for building ADSs.

What is an authenticated data structure?

An authenticated data structure is a data structure whose operations can be carried out by Bob, the results of which Alice can efficiently check as authentic. This is done by having Bob produce a compact proof that Alice can check along with each query result.

ADS interaction between trusted client (verifier) and untrusted server (prover)

ADSs support outsourcing data maintenance and processing tasks to untrusted servers without loss of integrity, where the server plays the role of Bob, the prover, and the client plays the role of Alice, the verifier. Such scenarios are particularly compelling with the rise of “the cloud.”

Merkle Hash Trees

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. The original work on the topic, by Ralph Merkle in 1989, was for a particular data structure that has come to be known as a “Merkle hash tree”, or “Merkle tree” for short.

A Merkle tree essentially implements a map from natural numbers to values using a complete binary tree, where the values are stored at the leaves of the tree. The bit representation of the index encodes the path through the tree: a 0 indicates “go left” and a 1 indicates “go right”. Thus if the size of the domain is N, then the size of the tree is 2N – 1 and lookups take time O(log N).

The thing that makes this data structure interesting is the use of cryptographic hashes to form the basis of the proof communicated from server to client. Each leaf node is coupled with a cryptographic hash of the associated value, which we refer to as the digest. Each internal node contains a digest that is the hash of the concatenation of the digests of its two children. Thus the use of hashes is recursive.

When looking up a value in the tree, the server accumulates digests associated with the path taken to reach the value (I’m being vague about the details, to keep things simple). These constitute the proof, which in general has size proportional to the running time of the operations on the tree (e.g., O(log N) for lookups).

The use of hashes makes it possible to ensure that each step of an operation on the tree is carried out properly; if not, the verifier can discover an inconsistency with high probability.

Status Quo: Designing New ADSs from Scratch

Since Merkle’s seminal paper, cryptographers have identified other scenarios in which an authenticated data structure would be useful, but a Merkle tree in particular wouldn’t be the best choice. For example, an authenticated version of a cloud-based file system, like Dropbox, would prefer a data structure like a b-tree for managing stored blocks. The increasingly popular Bitcoin electronic currency uses an authenticated data structure for keeping track of the ledger of transactions. Researchers have also developed authenticated red-black trees, authenticated skip lists, and other variations, too.

The problem with this state of affairs is that to design a system that uses an authenticated data structure requires expertise in cryptography. This is because each new data structure requires the designer to construct, from scratch, a proof that the data structure is both correct and secure. By the former property we mean that when both the prover and the verifier act as they should, the answer that is produced is the same as in the “ideal” version of the data structure, as might be implemented on a single host. By the latter property we mean that if the prover (or some other intermediate party) attempts to subvert the protocol so as to lie about the answer, the verifier will discover the subterfuge with high probability. (Note that these properties are sometimes given different names in the crypto literature.)

At their root, the correctness proofs rely on the fact that ADSs are augmentations of their non-authenticated versions, so there is a close correspondence between the execution of the ADS and the ideal operations when all goes well. The security proofs rely on the one-way nature of the cryptographic hashes that are integrated into the data structure. To elaborate: in knowing what a lookup or other operation is supposed to be doing when producing its proof, the verifier can confirm that each step of the operation is producing evidence consistent with what it knows about the data structure, as determined by the hash that it retains. To lie about a result and not get caught ultimately boils down, by an inductive argument, to finding a hash collision. Since hash collisions are computationally difficult to find, then so is lying about the final result.

The problem is that these key ideas are embedded within an argument involving the details of the various operations themselves. The proofs are made more laborious by the fact that the data structure and operations on it are often specified semi-formally, as a combination of English prose with some math notation and pseudocode. As such, it’s not necessarily obvious how to generalize the argument to arbitrary data definitions and operations on them, since there is no formal language used for either. Worse yet, there’s no way to reuse the a proof, so even small customizations of existing ADSs would require additional work to prove they are secure. Ideally, the key argument involving the use of hashes could be made independent of  the rest of the details of the operation, so that customizations do not require the proof to be redone.

Programming Languages for General-purpose ADSs

Fortunately, ideas from the programming languages research community can help remedy this state of affairs. PL researchers have spent decades developing mathematics for specifying the semantics of programming languages in a compositional manner.

The comunity has also developed methods for proving properties about whole classes of programs by typing. A classic example is the property “well typed programs don’t go wrong” (a phrase due to Robin Milner). This property states that if a program is accepted by a type system (it is “well typed”), then a certain class of errors that would cause it to fail (e.g., treating a string as if it were a function, by trying to call it), are not possible. As such, a programmer does not have to provide a separate proof for each program she writes that it will not go wrong; rather, the programmer simply ensures the program is well typed, and the desired property follows directly.

We can apply these techniques to the problem of defining general-purpose ADSs. In particular, we can define a small language feature that captures the key ideas of ADSs discussed above: the use of hashes within the data structure, and the systematic construction (and consumption) of proofs based on the execution of an operation, as defined by normal features of the language. By defining the semantics and type system carefully, we can prove that “well typed programs are secure and correct.” As such, programmers can design new ADSs simply by writing them down in the language and establishing they are well typed. This is significantly easier than proving correctness and security all over again.

The next blog post will describe how we did exactly this in our POPL’14 paper.