International Association
for Cryptologic Research

Project Everest is constructing a high-performance, standards-compliant, formally verified implementation of the HTTPS ecosystem, including TLS, X.509, and the core cryptographic algorithms. This talk will present an overview of how we verify our implementations are correct, cryptographically secure, and resilient to basic side channels. We will focus on our EverCrypt cryptographic provider, a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for the same functionality) and multiplexing (choosing between multiple implementations of the same algorithm). Through a combination of abstraction and zero-cost generic programming, we show how agility can simplify verification without sacrificing performance, and we demonstrate how C and assembly can be composed and verified against shared specifications. The result is several functionalities whose performance matches or exceeds the best unverified implementations. Altogether, EverCrypt consists of over 100K verified lines of specs, code, and proofs, and it produces over 45K lines of C and assembly code.

In this talk we will provide an overview of the current activities of the RISCV Foundation, including the creation of a Security Standing Committee about a year ago which is in charge of assessing new threats and opportunities in security in the RISCV world; we will discuss progress being made by the security-related task groups. The first one is working on specifying extensions of the base instruction set architecture (ISA) that will enable high-performance and high security cryptographic operations (AES, SHA-2, Public Key Cryptography); the second one is looking at creating extensions and hardware/software specifications to enable a trusted execution environment built on top of a RISCV processor; we will also provide details on the activities of the Security Standing Committee itself, and what some of the plans are to tackle the newest microarchitectural cache timing side-channel attacks such as Spectre, Meltdown, Foreshadow, etc. We will review some additional work on secure RISCV and existing security extension initiatives by academia around the world. Finally, we will describe some approaches of how a side-channel and DPA-resistant RISCV CPU could be built and elaborate on the research we have been focused on in the past months.