MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Authenticated Data Structures, Generically

Michael W. Hicks
University of Maryland
SWS Colloquium

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.
SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Friday, 5 December 2014
13:30
90 Minutes
E1 5
029
Saarbrücken

Abstract

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

Contact

Claudia Richter
0681 9303 9103
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
207
passcode not visible
logged in users only

Claudia Richter, 12/03/2014 12:42
Claudia Richter, 12/03/2014 12:39 -- Created document.