Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - CIRCUS (An end-to-end verification architecture for building Certified Implementations of Robust, Cryptographically Secure web applications)

Teaser

The security of modern web applications depends on a variety ofcritical components including cryptographic libraries, secure channelprotocols, browser security mechanisms, and application-levelauthorization protocols. Although these components are widely used,their security...

Summary

The security of modern web applications depends on a variety of
critical components including cryptographic libraries, secure channel
protocols, browser security mechanisms, and application-level
authorization protocols. Although these components are widely used,
their security guarantees remain poorly understood, resulting in
subtle implementation bugs and insecure deployments.

The last few years have further deteriorated our confidence in these
security mechanisms. The Snowden reports indicate that the design
and implementation of many cryptographic algorithms may have been
tampered with. Independently, a series of attacks has shown that most
popular modes of the Transport Layer Security protocol (TLS) are
obsolete and no longer reliable. Over and above this turmoil,
websites continue to be hacked and the use of passwords for user
authentication continues to be a weak link in web application
security.

In response to these vulnerabilities, attacks, and potential
weaknesses, the cryptographic and web security communities are
proposing a series of new standards. New elliptic curves are being
standardized to give users an alternative to possibly tampered
algorithms. A new version of Transport Layer Security (TLS 1.3) has
just been published by the IETF and is being implemented by all web
browsers. New web authentication protocols like OpenID Connect
are becoming widely used on major websites.

The security of web applications is at a moment of
transition. These new mechanisms hold much promise but need careful
scrutiny to avoid the traps that their predecessors fell victim
to. Rather than testing one attack at a time, we advocate the use of
formal security verification to identify and eliminate entire classes
of vulnerabilities in one go.

The goal of CIRCUS is to bring together
state-of-the-art research in software verification and cryptographic
protocol analysis to meet this challenge. We aim to develop new tools
and techniques that make it possible to verify the security of
emerging security protocols like TLS 1.3 and OpenID Connect, to develop
high-assurance high-performance libraries that implement modern
cryptographic algorithms and protocols, and to enable new web
applications that can rely on these verified mechanisms to provide strong and proven
security and privacy guarantees to all Internet users.

Work performed

In the first half of our project, we made significant progress on all work packages.
Below we note our main achievements, in terms of publications and real-world impact.

WP1: From verified F* code to efficient C programs
We developed the theoretical foundations for writing efficient stateful code in the F* verification-oriented programming language
in a way that the code can be compiled to programs in the C programming language. We designed and developed a compiler, called KreMLin,
from F* to C and used it to implement a full cryptographic library and a part of the TLS 1.3 protocol (see below). This work was done in collaboration
with Microsoft Research and resulted in a paper at the ICFP conference in 2017, and our compiler is already being used in multiple research projects.

WP2: HACL* - A Verified Modern Cryptographic Library
We designed and developed HACL*: the first cryptographic library in C to be verified for memory safety, functional correctness, and side-channel resistance.
Our library includes a full suite of modern cryptographic algorithms and can be used as a drop-in replacement for crypto libraries currently used in TLS implementations
or in web applications. Our code is not only verified, it is as fast as state-of-the-art handwritten C code. The HACL* library is now being used in production software.
It is incorporated within Mozilla Firefox, the WireGuard VPN, and the Microsoft Everest HTTPS stack. As such, this library is a significant achievement, both for
research and technological transfer. Our work on HACL* was published at the ACM CCS conference in 2017.

WP3: Improving Transport Layer Security (TLS)
We participated in the design and standardization of the TLS 1.3 protocol, and our work is acknowledge in the TLS 1.3 standard.
We published detailed proofs of the TLS 1.3 protocol using verification tools developed in our research group at INRIA.
We also developed two high-assurance implementations of the TLS 1.3 protocol, one in JavaScript and the other in F*.
Our work on TLS 1.3 resulted in two publications at IEEE S&P 2017, one of which was awarded the Distinguished Paper Award.

Independently, we studied the use of block ciphers like 3DES and Blowfish in popular protocols like TLS and OpenVPN and discovered
attacks when such algorithms were used on long-running sessions. In response to our findings, the NIST standards body published
a statement deprecated the use of the 3DES standard, and this statement explicitly acknowledge our work. This work was published
at ACM CCS in 2017. We also worked on multi-party TLS variants, resulting in papers at IEEE Euro S&P 2017 and IEEE S&P 2018.

WP5: Analyzing Secure Messaging Protocols
We developed detailed proofs for the popular Signal secure messaging protocol, which is currently used by WhatsApp,
Facebook Messenger, Microsoft Skype, Google Allo, and Wire. We also published a verified implementation of this protocol
and deployed it as part of the CryptoCat messenger. This work resulted in a paper at the IEEE Euro S&P Conference in 2017.

Final results

Our verification methodology, based on proving our source code in F* and compiling the verified code to C, is one of the most advanced frameworks for developing high-assurance high-performance software. We plan to continue improving this toolchain to make it easier to use for C developers. We are also working on a compiler from F* to WebAssembly, so that our methodology can also be used to develop verified web applications that can be deployed on mainstream web browsers and smartphones.

Our cryptographic library pushes the state-of-the-art for fast verified crypto and is starting to be widely used in mainstream software applications like the Firefox web browser.
We plan to work on incorporating more advanced cryptographic constructions into HACL*. We are currently working on implementing and verifying various post-quantum crypto proposals, as well as privacy-preserving algorithms relying on homomorphic encryption. We are also working on incorporating HACL* code in more open-source software projects, including the Linux kernel.

After the success of TLS 1.3, we are participating in the design and standardization of a new secure messaging protocol at the IETF called Messaging Layer Security (MLS). We plan to build on our expertise in analyzing protocols like Signal and TLS 1.3 to propose new designs and security analysis for this upcoming standard. We anticipate that before the end of the project, MLS will be close to publication and will be implemented by mainstream messaging applications like WhatsApp.

We have also initiated a number of other research directions that have not yet reached maturity. Before the end of the project, we expect to have formalized and published a full security model for the HTML5 standard as it is implemented by mainstream web browsers. We expect to use this model to verify the security of a series of widely used web security protocols, including OAuth 2.0 and OpenID Connect.