Category Archives: Secure computation

Secure computation broadly refers to goal (and techniques to achieve it) that a computation runs securely despite the computational platform, the participants, and/or their interactions are untrusted.

Formal Reasoning in PL and Crypto

In my last post, I summarized some of the topics and problems considered at a recent Dagstuhl seminar I co-organized on the Synergy between Programming Languages and Cryptography. The post surveyed how programming languages often interface with cryptography in the construction of secure systems, and in particular how they can make it easier to implement cryptography, use it, or verify its correctness.

Beyond using PLs as a tool for easier/safer use of Crypto, there is an opportunity for certain kinds of thinking, or reasoning, to cross over fruitfully between the PL an Crypto communities. In particular, both communities are interested in formalizing systems and proving properties about them but they often use different methods, either due to cultural differences, or because the properties and systems of interest are simply different. During the workshop we identified both analogous, similar styles of reasoning in two communities and connection points between the different styles of reasoning. In this post I briefly highlight a few examples of each, and point to future research opportunities.

Continue reading

1 Comment

Filed under Formal verification, Program Analysis, Secure computation, Semantics, Software Security, Uncategorized

The Synergy between Programming Languages and Cryptography

I recently had the pleasure of co-organizing a Dagstuhl Seminar on the synergy between ideas, methods, and research in programming languages and cryptography.

Dagstuhl Seminar on the Synergy between Programming Languages and Cryptography

This post and the next will summarize some interesting discussions from the seminar. In this post, I will look at how programming languages often interface with cryptography, surveying the research of the seminar participants. In my next post, I’ll dig a little deeper into one topic in particular, which is how formal reasoning in PL and Crypto compare and contrast, and how ideas from one area might be relevant to the other.

Ultimately, I came away convinced that the combination of PL and Crypto has much to offer to the problem of building secure systems.

Continue reading


Filed under Formal verification, Research, Research directions, Secure computation, Software Security

ADS, generically, part II

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.

Continue reading

Leave a Comment

Filed under Secure computation, Software Security, Uncategorized

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.

Continue reading


Filed under Secure computation

Securing computation

This post is the introduction of a series that discusses research bringing together ideas from the Programming Languages and Cryptography (Crypto) communities. The combination of ideas aims to produce secure computation technologies that are easier to use efficiently in a general-purpose setting, and easier to reason about, than when applying the Crypto ideas directly. My next post will be on work I’ve recently published in this area in collaboration with colleague cryptographers. Subsequent posts will consider other areas of interesting research (mostly not mine).

Continue reading

1 Comment

Filed under Secure computation