CIRCUS: Certified Implementations of Robust, Cryptographically Secure Components

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. A series of attacks, some of them , 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. The work of our team contributed to a new version of Transport Layer Security (TLS 1.3) that has been published by the IETF and is being implemented by all web browsers and servers.

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, 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.