RESEARCH ROADMAP FOR 2016-17 


WORKPLAN


We will pursue two complementary lines of work.

PRIVACY

Differential privacy is a rigorous and quantitative notion of statistical privacy, and one of the most promising formal definitions of privacy to date. Since its initial formulation ten years ago, differential privacy has attracted substantial attention throughout computer science, including areas like databases, machine learning, and optimization, and more.

There are several reasons for this success.
For one, differential privacy allows a formal trade-off between privacy and accuracy: differentially private algorithms come with a privacy guarantee expressed in terms of two parameters epsilon (expressing the privacy cost) and delta (expressing the probability of violating the privacy cost). For both parameters, smaller values offer stronger privacy guarantees. Another important advantage differential privacy is that it composes well: differentially private algorithms can be easily combined to build new private algorithms.

The differential privacy literature offers several composition theorems, which provide the foundation of several formal verification techniques. In a series of work (POPL 2012, POPL 2015, LICS 2016, CCS 2016), we have developed verification methods for differential privacy, and used them to analyze many algorithms from the literature. We will further enhance our verification methods in order to make them support analysis of recent proposals for differential privacy.
Moreover, we will further explore the foundations of these approaches.


CRYPTOGRAPHY

We need cryptographic implementations that we can trust. However, our trust in cryptographic implementations has been repeatedly undermined by a proliferation of bugs, side-channel attacks, logical flaws and suspected backdoors. Real-world cryptography aims to address this problem, by applying the principles of provable security to analyze widely used protocols under the light of more precise security definitions and adversary models. This is an essential step towards making provable security practically relevant, but it is bound to be limited in the level of implementation detail that can be captured in the abstractions used. Indeed, reconciling provable and practical security requires a close interplay between cryptography and programming language theory, which can provide tools to rigorously reason about the properties of implementations.

Although this relationship has been explored before, often in specialized settings, there lacks a general framework that unifies the previous contributions, brings a broad perspective on the current state-of-the-art, identifies new opportunities for cross-fertilization between cryptography, programming languages, and formal methods, and provides a blueprint for future research.

In a recent article (FSE 2016, best paper award), we realize in the important case of MEE-CBC, an essential component of the TLS protocol, a vision to deliver strong mathematical guarantees, in the style of provable security, on low-level implementations of cryptographic software. We lay down a formal framework over which one can derive the security of implementations from a combination of three properties: black-box security in the computational model, implementation correctness, and leakage simulation. In a companion article (USENIX Security 2016), we develop an automated verification technique to mitigate cache timing-attacks. Our technique is an adaptation of product program, which arises in the context of program verification.
We will further explore language-based approaches to mitigate cache side-channel attacks from cryptographic implementations. On the one hand, we will explore applications of our verification methodology to other settings. On the other hand, we will explore the preservation of the cryptographic constant-time property by compilation.

In parallel, we will further explore a scalable approach to formally verifying implementations of higher-level cryptographic systems, directly in the computational model. As an example, we will consider Yao's celebrated secure function evaluation protocol, where a computation is first expressed as a Boolean circuit, and then translated into an equivalent garbled form that can be evaluated securely in an untrusted environment. Our goal will be to build verified implementations of garbling schemes and a verified implementation of Yao's secure function evaluation protocol. We will also a general-purpose certified compiler that translates C programs into Boolean circuits. We envision the circuit compiler to be an extension to the CompCert compiler. In order to gain acceptance from the broader community, we also intend to ensure that our compiler outperforms competing tools for the domain of cryptography.