2014-12-05 13:30
Mike Hicks

Mike Hicks, 5 December 2014, 1:30pm

Mike Hicks

University of Maryland

Title : Authenticated Data Structures, Generically

hosted by Derek Dreyer; MPI-SWS Saarbruecken, Campus E1 5, room 029

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.

Joint work with Andrew Miller, Jonathan Katz, and Elaine Shi, at UMD


Michael W. Hicks is a Professor in the Computer Science department and
UMIACS at the University of Maryland and is the former Director of the
Maryland Cybersecurity Center (MC2). His research focuses on using
programming languages and analyses to improve the security,
reliability, and availability of software. He is perhaps best known
for his work exploring dynamic software updating, which is a technique
by which software can be updated without shutting it down. He has
explored the design of new programming languages and analysis tools
for helping programmers find bugs and software vulnerabilities, and for
identifying suspicious or incorrect program executions. He has
recently been exploring new approaches to authenticated and
privacy-preserving computation, combining techniques from cryptography
and automated program analysis.