Hardware provides the foundation of trust for computer systems. Defects in hardware designs routinely cause vulnerabilities that are exploitable by malicious software and compromise the security of the entire system. While mature hardware validation tools exist, they were primarily designed for checking functional correctness. How to systematically detect security-critical defects remains an open and challenging question.
In this talk, I will present my research on developing formal methods and practical tools for automated hardware security validation. First, I will discuss how to validate a hardware design given some security properties. I will present Coppelia, which is an end-to-end tool that designs hardware-oriented backward symbolic execution to find violations and generate exploit programs. Second, I will discuss how to efficiently build security properties. I will introduce SCIFinder, a methodology that leverages known vulnerabilities to mine and learn security invariants. I will then describe Transys, which automatically translates security properties across similar or different generations of hardware designs. These solutions have been applied to open-source RISC-V and OR1k CPUs, and have detected both existing and new vulnerabilities. I will conclude my talk by describing future directions on further improving formal methods to validate the security of modern hardware.
Speaker Biography
Rui Zhang is a PhD candidate in the Computer Science Department at the University of North Carolina at Chapel Hill. Her research interest lies in the areas of hardware security and formal methods, with a focus on developing automated systems and tools for detecting vulnerabilities and validating the security of hardware designs. Her research has been recognized with a best paper award nomination at MICRO and a candidate of Top Picks in Hardware and Embedded Security. She is an invited participant at the Rising Stars in EECS Workshop and the Rising Stars in Computer Architecture Workshop. She received her master’s degree from Columbia University in 2015 and her bachelor’s degree from Peking University in 2013.