University of North Carolina at Chapel Hill
Rui Zhang is a PhD candidate in the Computer Science Department at University of North Carolina at Chapel Hill, advised by Professor Cynthia Sturton. Her research interests lie at the intersection of formal analysis techniques and hardware security. Her work has resulted in formal, 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 2018. She was nominated as one of two candidates for Google PhD fellowship representing UNC Chapel Hill in 2016. She received her master’s degree from Columbia University in 2015 and her bachelor’s degree from Peking University in 2013.
Hardware presents an enticing target: an attacker who controls the hardware of a machine can often gain unrestricted access to the entire machine. The recent Spectre and Meltdown attacks, along with their variants, have shown how vulnerable modern computer hardware is. The current state of the art to detect and eliminate vulnerabilities in hardware designs uses assertion based verification, which combines formal static analysis and simulation based testing. While powerful, they are not well-suited to the identification and analysis of security vulnerabilities, and the security properties needed for the verification are hard to identify and develop. My research focuses on developing systems to help hardware designers efficiently detect design-time security vulnerabilities, and build more secure hardware designs. My research makes contribution in two directions: security property identification and exploit program generation. First, I develop a semi-automatic approach SCIFinder to identify security properties of processor designs. I rely on security errata to find out some initial security assertions, then I use machine learning techniques to expand the set of security assertions. The security assertions built can be useful for similar designs, but repeating the whole process for each new design can be tedious. Thus, I develop a tool Transys to automatically translate security assertions from one design to similar designs to further reduce the effort and leverage existing security properties. Second, I develop an end-to-end tool Coppelia that automatically generates exploit programs. It helps designers better analyze, understand, and assess the security threat for vulnerabilities in hardware.