This post is the second part of a post on using ideas from programming languages to assist the design of authenticated data structures (ADSs). I will describe a small programming language extension for building ADSs that I co-developed with Andrew Miller, Jonathan Katz, and Elaine Shi, called **LambdaAuth**. A paper on this language was presented at POPL’14 and the implementation is freely available.

As a word of warning, this post goes into some technical detail. The goal of doing so is to make, in detail, a general point: *programming language researchers’ focus on ways of programming *(often embodied as language features, patterns, transformations, or analyses), rather than particular programs, yields* broadly applicable results*, extending outside of the motivating examples or domain. In this case, **LambdaAuth** embodies a simple mechanism for programming *any* authenticated data structure, not just one particular kind.

If you get bogged down in the details, you can always jump to the Conclusions at the end, which elaborates on this main point.

**Authenticated Data Structures**

The original post introduced the idea of an ADS. To recap, briefly: An ADS supports outsourcing data management tasks. A server stores a data structure and performs operations on that data structure requested by a client. To assure the client these outsourced operations have been performed correctly (i.e., they are “authentic”), the server provides a proof along with the result. An ADS is *secure* if the server can successfully lie about the result only with negligible probability. It is *correct* if the result is the one you would get from using a “normal”, non-authenticated version of the data structure.

Security and correctness of an ADS written in our language **LambdaAuth** follows from type correctness, which is relatively easy for the programmer to ensure. Conversely, the previous state of the art required the programmer to produce security and correctness proofs for every ADS they developed. **LambdaAuth**‘s design helps to isolate the key elements involved in the security of the ADS so that they can be proven effective once and for all, rather than on a per-data structure basis.

**Example: Binary Search Tree**

Suppose the outsourced data structure we are interested in is a binary search tree (BST). Creating an authenticated BST in **LambdaAuth** is as easy as writing an ordinary BST in OCaml. The following code (adapted from examples/bintree.ml in our distribution) is an example of membership lookup, where the tree stores integers:

type tree = Leaf | Node of (tree * int * tree) authtype let rec (contains : int -> tree authtype -> bool) x t = match t with | Leaf -> false | Node a -> let (l,y,r) = unauth a in if x = y then true else if x < y then contains x l else contains x r

Ignoring the **authtype** type operator and the **unauth** keyword (imagine just erasing them from the code), this is a standard binary search tree. In short: trees are either a **Leaf** (which has no data associated with them) or a **Node** consisting of two sub-trees and an integer value. The *contains* function takes two arguments, an integer *x* and a tree *t* and returns whether *t* contains *x*. If the tree is a **Leaf** then it contains no values, much less *x*, so the answer is **false**. If the tree is a **Node**, then the function compares *x* against the value *y* stored at that node, returning **true** if they match, or else recursing to the left sub-tree if *x* < *y* and the right sub-tree otherwise.

**Client and Server Code**

The **LambdaAuth** compiler automatically generates executables for both the client and the server from this single piece of input code. For normal language constructs, compilation proceeds as normal, and both parties get the same code. The interesting part is the added syntax.

Data of type *‘a* **authtype** is represented at the server as a pair consisting of a value of (the server representation of) type *‘a*, and a cryptographic hash (e.g., using SHA1) of a shallow projection of that value, which is a serialized version of the representation of that value up to and including, but not beyond, any nested hashes. We will write * hash*(

*v*) to indicate taking the cryptographic hash of the serialized (i.e., flat byte) representation of

*v*. At the client,

*‘a*

**authtype**values are only the hash, and not the value. This is how ADSs are used for outsourced storage: The server’s view of the tree is the entire data structure (starting at the root, which is the tree and its hash), while the client’s view is just the root’s hash.

As an example, the following picture shows the client’s and server’s view of the same tree, which has type *tree* **authtype** (that is, it is a *tree* whose root is also authenticated). **Leaf** elements are depicted as ⊤, and **Node**s are depicted as the large ovals. The lower right of the figure shows how *h1*, *h2*, etc. are computed as the hashes of the shallow projections of corresponding tree elements.

Returning to the code: The **unauth** keyword is a function that takes a value of type *‘a* **authtype** and returns a value of type ‘a. At the server, a value of type *‘a* **authtype** has form *(h,v)* where *h* is the hash and *v* is the value. **unauth** will return *v* (which has type *‘a*), and at the same time it will add the shallow projection of *v*, call it **sp**(*v*), to the current *proof*, which will consist of a list of shallow projections. Importantly, recall that *h* = * hash*(

**sp**(

*v*)). The complete proof is sent to the client, along with the final answer.

To verify the authenticity of the server’s answer, the client runs its version of the code on its version of the data (e.g., starting with the root hash), consuming the server’s proof. Each time the client reaches an **unauth**, the provided argument will simply be a hash value *h*. At the client, the **unauth** function will pull the front element from the proof stream (call it *s*), compute its hash (call this *h’*), and confirm that *h = h’*, returning *s*, if so. Recall that *s* should be the shallow projection of the actual value in the tree, so it will have the “shape” assumed by the current computation. Importantly, the fact that the client’s hash *h* matches the hash *h’* of this shallow projection, means that this shallow projection is correct one, with high probability. The reason is that hash functions are “one way,” in the sense that it is very hard to find a value *v* such that, for a given *h*, * hash*(

*v*) =

*h*.

**Example Execution**

Returning to our example, the client could ask the server to compute (*contains* 4 (**unauth** *t*)); that is, whether the tree contains the integer 4. The answer will be **false**, producing the following proof stream:

The first element comes from the first call to **unauth**, which is applied to the initial tree. The shallow projection of the root’s value is added to the front of the proof stream (the leftmost value). Notice that the shallow projection includes the data in the root node, and the hashes of the subtrees, but not the values of the subtrees. The next element of the proof comes from a recursive call to *contains*, which is given the right subtree. The **unauth** call puts its shallow projection in the proof. The final element is just a **Leaf** which is due to the last recursive call; the shallow projection of a non-**authtype**-containing value is just the value itself.

The client will run its version of the code to consume this proof. On the first call (*contains* 4 (**unauth** *t*)), the *t* that is passed in is the root hash *h1*. The client will dequeue the first element of the proof and compute its hash. As shown in the first figure above, the hash of this element is *h1*, so hashes match and we can proceed computing with the shallow projection as the returned value. The recursive call will pass *h3* as the tree argument, and the subsequent **unauth** call will compute the hash of the second element of the proof. The hash is *h2*, as shown in the first figure, so once again the hashes match. The final call is to the leaf, so the element is not in the tree, and **false** is returned.

**Why does it work?**

Congratulations on making it this far! Now that you have seen a **LambdaAuth** example, let’s step back and reflect on why it works.

The key idea in **LambdaAuth** is that it can use a root of trust, the initial hash, to extend trust to data (the shallow projections) provided in the server’s proof, ultimately reproducing the entire computation. Doing so makes sense because hashes are recursive, covering all of the data below them, including the nested hashes, but not the data that those hashes themselves cover. The server’s proof begins with the data covered by the initial hash that the client trusts, i.e., the shallow projection of the root of the tree. In confirming that the hash is correct (by recomputing the hash from the data and comparing it to the client’s own hash), the client extends its trust to the given data, including the nested hashes. It can therefore compute with that data safely and use any nested hashes it reaches to confirm the trustworthiness of subsequent data it extracts from the proof.

**How do you prove it works?**

In traditional work on ADSs, the proof that the data structure is secure (i.e., that a malicious server can only successfully lie about its answer with very low probability) is done on a per-data structure basis. This is because the idea behind why ADSs work is embedded in the design of each ADS. Even though this idea is roughly the same for each data structure, the lack of explicitness makes it hard to reason about on its own.

By contrast, the key idea in **LambdaAuth** is made explicit as a language construct: the semantics of ‘a **authtype** data and the **unauth** construct. (Note that there is an **auth** construct too, for building authenticated data, but we elide that in this post. See the paper for details.) There is a clear connection between what the server does with **unauth** and what the client does: the server adds the shallow projection of the current value it is considering, while the client consumes that shallow projection and confirms that its hash matches the hash the client expects. We can formalize this connection compositionally without worrying about the other aspects of how the data structure works, since they are the same on both client and server. This design gives us the ability to perform reasoning that *works for all data structures* (which use **authtype**s), not just particular ones.

As such, we can prove the following theorem about all **LambdaAuth** programs: Given a program *P* that is type correct, and given the client and server versions of that program, *PC* and *PS*, respectively, if *PS* produces a proof that *PC* consumes successfully, then the answer must be the one that *PS* would produce when behaving correctly (non-maliciously), with high probability. Type correctness in **LambdaAuth** boils down to the standard notion of type safety (e.g., don’t use integers as if they were functions), and the proper use of **unauth**, which is simply that you only pass it values of *‘a* **authtype**, in which case it will produce one of type *‘a*.

We can prove this theorem using completely standard, syntactic methods, following how type safety proofs are normally done in programming languages (as detailed, for example, in Benjamin Pierce’s excellent introductory text, Types and Programming Languages). These are the sorts of proofs that graduate students learn in the first few weeks of programming languages courses (e.g., CMSC 631 at Maryland) — they are not hard at all. A feature of such proofs is that they are highly rigorous, e.g., they could be easily mechanized for added assurance, which is great for security applications, and is somewhat in contrast to the more prosaic style of proofs in previous ADS papers.

**Conclusions**

A takeaway message from this post is that methods developed in the programming languages community, both for formalizing language semantics and for implementing them, are a useful complement to methods used in other areas of computer science, in this case cryptography, where reasoning about computation is important.

To repeat what I said at the start: The key here is that * programming language researchers focus on ways of programming* (often embodied as language features, patterns, transformations, or analyses), rather than particular programs. As a result,

*, extending outside of the motivating examples or domain. For*

**PL results are general-purpose****LambdaAuth**, anyone can now easily create new ADSs, e.g., new datastructures used by bitcoin (our paper has several other examples).

Over time, the PL researcher’s toolbox has filled with useful formal and practical constructs/algorithms/mechanisms that apply to whole languages or ways or programming, and thus support general results, like general-purpose ADS programming and not just particular ADSs, in the case of **LambdaAuth** described here. I think there is a great opportunity for further collaboration between cryptographers and programming language researchers in particular; I’ll discuss more possibilities in future posts.

More technical details about **LambdaAuth** can be found in the conference paper and the **LambdaAuth** web site.