Abstract: The state of the art for hardware security verification relies heavily on manual inspection, code review, and functional verification techniques to identify security vulnerabilities. This labor-intensive process doesn’t scale, significantly reduces productivity, and provides no assurance that a security flaw will be found. Maintaining the status quo leaves hardware vulnerable to attacks exploiting hardware, firmware, and software weaknesses.

This presentation describes a framework for scalable hardware security verification. The methods focus on information flow tracking and include static analysis, simulation/emulation, and formal verification. The presentation discusses the challenges in hardware security verification, including developing and refining properties, creating security metrics, understanding vulnerabilities, debugging potential security flaws, and scaling to industry designs. The talk highlights our security verification efforts on the Caliptra and OpenTitan hardware roots of trust.

Ryan Kastner is a professor in the Department of Computer Science and Engineering at UC San Diego, where he holds the William Nachbar endowed chair. He received a Ph.D. in Computer Science at UCLA, a Master’s degree (MS) in engineering, and Bachelor’s degrees (BS) in Electrical Engineering and Computer Engineering, all from Northwestern University. He leads the Kastner Research Group whose current research interests fall into three areas: hardware acceleration, hardware security, and remote sensing. He is the co-director of the Wireless Embedded Systems Master of Advanced Studies Program. He also co-directs the Engineers for Exploration Program. He is the co-founder of Cycuity, which develops hardware security verification solutions. He is an IEEE Fellow.

Abstract: Modern superscalar execute a large number of instructions in parallel, and, like other massively parallel systems, exhibit numerous race conditions. While the illusion of sequential execution hides the architectural effects of these race conditions, observing microarchitectural state can expose these races. Transient execution attacks, such as Spectre and Meltdown, exploit such races to bypass security boundaries and leak information. However recent research extended the understanding of microarchitectural races identifying multiple use cases. This talk, explores microarchitectural races beyond transient execution attacks. It identifies basic primitives that allow inducing race conditions and exploiting them, showing that these primitives allow arbitrary computation over microarchitectural state. It then demonstrates some use cases for microarchitectural races, including code obfuscation, augmenting cache attacks, and reverse engineering.

Yuval Yarom is a Professor of Computer Security at Ruhr University Bochum. His research focuses on the interface between the software and the hardware. In particular, He is interested in the discrepancy between the way that programmers think about software execution and the concrete execution in modern processors. Before that, he was an Associate Professor at the University of Adelaide, the Vice President of Research in Memco Software, and a co-founder and Chief Technology Officer of Girafa.com. Yuval earned his Ph.D. in Computer Science from the University of Adelaide in 2014, and an M.Sc. in Computer Science and a B.Sc. in Mathematics and Computer Science from the Hebrew University of Jerusalem in 1993 and 1990, respectively.