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.

Dagstuhl Seminar

For those of you who might not know, Schloss Dagstuhl is a retreat center for computer science-related workshops. The center “promotes fundamental and applied research, continuing and advanced academic education, and the transfer of knowledge between those involved in the research side and application side of informatics” by hosting workshops that “bring together internationally renowned leading scientists for the purpose of exploring a cutting-edge informatics topic.”

Each year Dagstuhl requests proposals for workshops, and my co-organizers Gilles Barthe, Florian Kerschbaum, Dominique Unruh and I responded with our idea for a PL+Crypto workshop. We also got some initial help from Jonathan Katz. Our proposal was accepted, and ultimately a great group of people agreed to participate during the week of 30 November to 5 December (2014). We organized the workshop following some very helpful guidelines by Shriram Krishnamurthi. We put together a mix of talks and topic-driven discussions on various topics.

Using PL to do Crypto

During the workshop we explored several relationships between PL and Crypto. One connection emerged repeatedly: the use of programming languages to do cryptography, e.g., to implement it, optimize it, and prove it correct. The following diagram depicts three facets of this connection.

Programming languages can be compiled to cryptographic mechanisms

Programming languages can make cryptographic mechanisms easier to use. For example, the systems Sharemind, ShareMonad, CBMC-GC, and Wysteria are all designed to make it easier for programmers to write secure multiparty computations (SMCs).[ref]Some prefer the acronym MPC when referring to secure MultiParty Computation, but we use SMC here.[/ref] In an SMC, we have two (or more) parties X and Y whose goal is to compute a function F of their inputs x and y, whereby each party only learns the output F(x,y), but does not “see” the inputs. Cryptographers have developed ways to compute such functions, such as garbled circuits[ref]This is a recent reference for garbled circuits, not the original reference.[/ref] and computing on secret shares, without need of a trusted third party. The above-cited systems shield the programmer from the workings of these mechanisms, compiling normal-looking programs to use the cryptography automatically. The languages can also provide additional benefits, such compiler-driven optimization.

This line of work is motivated by privacy- and/or integrity-preserving outsourcing of computation, e.g., as promised by The Cloud. Programming languages have been designed to compile to other kinds of crypto aside from SMC, like zero-knowledge proofs and authenticated data structures. Examples include Geppetto, SNARKs for C, and LambdaAuth (featured earlier on this blog). Combinations also exist, such as compiling to support Authenticated SNARKs.

Programming languages for implementing cryptography

The above languages aim to make computations secure through the use of cryptography, introduced by the language’s compiler. We are also interested in implementing the cryptographic algorithms themselves (e.g., for symmetric or public key encryption). The implementation task could be made easier, more efficient, or more secure by employing a special-purpose language. Two representatives in this space are CAO and Cryptol. Both are domain-specific, and both make it easier to connect implementations to tools for automated reasoning. The Seminar also featured work on synthesizing cryptography (block ciphers) from constraint-based specifications.

Programming languages methods to prove security of cryptographic protocols and/or their implementations

When a cryptographer defines a cryptographic protocol, she must prove it is secure. Programming languages methods can be used mechanically confirm that a proof of security is correct. Systems like ProVerif, CryptoVerif, EasyCrypt, and CertiCrypt support cryptographic protocol verification, with varying kinds of assurance. These systems build on ideas developed in general verification systems like Coq or Isabelle.

Likewise, when a programmer implements some cryptography (in a language like C), she would like to formally verify that the implementation is correct (no more Heartbleed!). For example, we’d like to know that an implementation does not have side channels, it uses randomness sufficiently, it has no buffer overflows, etc. Once again, verification can be achieved using tools that are underpinned by PL methods developed in formal verification research. Frama-C and Fstar have been used to verify implementations.

Open Problems

Beyond work that is being done, one goal of the workshop was to identify possible collaborations on future work. PL researchers and cryptographers work on common problems from different points of view, so one obvious next step is to collaborate on these problems.

One relevant problem is side channels. Cryptographers are concerned with side channels in their implementations, e.g., to make sure the time, space, or power consumption during an encryption/decryption operation does not reveal anything about the key. Likewise, PL folk care about side channels expressed at the language level, e.g. work by Andrew Myers’ group on timing channels. Both groups bring a useful perspective.

Another common problem is code obfuscation. It was cryptographers that proved that virtual black box (VBB) obfuscation is impossible, and proposed an alternative indistinguishability-based definition. PL researchers, on the other hand, have looked at language-oriented views of obfuscation effectiveness, e.g., based on abstract interpretation. Just as the halting problem is undecidable, but practical tools exist that prove termination, I believe that there is an opportunity here to find something useful, if not perfect.

More Connection Points

Many more interesting points were made during the workshop that I do not have space to present here. In my next post, I’m going to dig a little deeper into how PL people and Crypto people reason about computations, drawing contrasts and connections. One observation that came up is that we can view the Crypto security goal of connecting the “real” implementation to its “ideal” manifestation as similar to the PL goal of proving an implementation satisfies its specification. This connection suggests we might carry methods from one community to the other.

I look forward to more events that can bring the PL and Crypto communities together. I think each community has something to offer the other, and collaboration could produce some very interesting work!