RISCV and Security: how, when and why?
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.
Helena Handschuh is a Security Technologies Fellow at Rambus, Inc. Her research and responsibilities include: managing the foundational security technologies team in charge of research in crypto and post-quantum crypto; research in power analysis and side-channel attacks and countermeasures; security architecture for new products and services; prototyping of new products and security standardization. She was formerly a Technical Director of Cryptography Research, Inc. (part of Rambus), and Chief Technology Officer at Intrinsic-ID. She was also the manager of the Applied Cryptography and Security Group and manager of the Card Application Security team at Gemplus (now Gemalto/Thales). She authored more than 50 peer-reviewed papers and holds 20+ patents in the areas of security and cryptography. Dr. Handschuh earned an M.S. in networks and communication engineering from the Ecole Nationale Superieure de Techniques Avancees (ENSTA, Paris), an M.S. in algorithms and cryptography from the Ecole Polytechnique, as well as a Ph.D. in cryptography from the Ecole Nationale Superieure des Telecommunications (ENST, Paris).
Developing High-Performance Mechanically-Verified Cryptographic Code
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.
Bryan Parno is an Associate Professor with a joint appointment in Carnegie Mellon University's Computer Science Department and Electrical & Computer Engineering Department, and a Senior Member of ACM and IEEE. After receiving a Bachelor's degree from Harvard College, he completed his PhD working with Adrian Perrig at Carnegie Mellon University, where his dissertation won the 2010 ACM Doctoral Dissertation Award. He then spent six years as a Researcher in Microsoft Research before returning to CMU.
Bryan's research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. In 2011, he was selected for Forbes' 30-Under-30 Science List. He formalized and worked to optimize verifiable computation, receiving a Best Paper Award at the IEEE Symposium on Security and Privacy for his advances. He coauthored a book on Bootstrapping Trust in Modern Computers, and his work in that area has been incorporated into the latest security enhancements in Intel CPUs. His research into security for new application models was incorporated into Windows and received Best Paper Awards at the IEEE Symposium on Security and Privacy and the USENIX Symposium on Networked Systems Design and Implementation. He has recently extended his interest in bootstrapping trust to the problem of building practical, formally verified secure systems, for which he received a Distinguished Paper Award at the USENIX Security Symposium. His other research interests include user authentication, secure network protocols, and security in constrained environments (e.g., RFID tags, sensor networks, or vehicles).