30.11.14 - 05.12.14, Seminar 14492

The synergy between programming languages and cryptography

The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.

Motivation

Increasingly, modern cryptography (crypto) has moved beyond the problem of secure communication to a broader consideration of securing computation. The past thirty years have seen a steady progression of both theoretical and practical advances in designing cryptographic protocols for problems such as secure multiparty computation, searching and computing on encrypted data, verifiable storage and computation, statistical data privacy, and more.

More recently, the programming-languages (PL) community has begun to tackle the same set of problems, but from a different perspective, focusing on issues such as language design (e.g., new features or type systems), formal methods (e.g., model checking, deductive verification, static and dynamic analysis), compiler optimizations, and analyses of side-channel attacks and information leakage.

The main objectives of the seminar are to cross-fertilize ideas between the PL and crypto communities, to exploit the synergies for advancing the development of secure computing, broadly speaking, and to foster new research directions in and across both communities. The programme will include tutorials to ensure common understanding and familiarity with existing tools, and research sessions covering the following (by no means complete) areas:

  • Formal tools for provable security: Moving beyond the traditional Dolev-Yao analysis, PL researchers have recently made progress on formally reasoning about standard cryptographic (reductionist) proofs of security, using concepts such as, e.g., Hoare logic, dependent type systems, and abstract interpretation.
  • Automated generation and analysis of cryptographic constructions: Program verification naturally suggests the possibility of developing automated tools for synthesizing new cryptographic algorithms and protocols.
  • Composability: Composability is a well known challenge in cryptographic protocol design, and is an area that has received significant study in the PL community as well.
  • Verified implementations: Work here fills the gap between the high-level descriptions of cryptographic protocols and deployed implementations.
  • Domain-specific programming languages for cryptography: Such languages can make advanced cryptographic techniques and abstractions more accessible, more efficient, and less error prone.
  • Information leakage: PL techniques are well suited to analyzing information flow, and understanding what amount of information leakage might be acceptable for certain applications.

The participants of this seminar will be drawn from both the PL and crypto communities, and will include researchers who have already started integrating techniques from both areas. This seminar presents an exciting opportunity to hear about the latest research and discover new connections!