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.