Abstract
With the ever-increasing complexity of modern software and hardware systems, security threats like Spectre and Meltdown reveal a distinct class of challenges: vulnerabilities that arise when hardware violates the security assumptions made by software. In this talk, I will share our research progress on two fronts: discovering blind spots in software-hardware security threat models, and building high-assurance systems. On the assurance side, we explore two approaches, reducing the Trusted Computing Base (TCB) and scaling formal verification. Our blind spot attack has influenced how industry designs next-generation processors, and our verification technique is the first to scale model checking to one of the most complex open-source out-of-order processors.
Biography
Mengjia Yan is an Associate Professor in the EECS department at MIT. She is a security computer architect whose research advances secure processor design by bridging computer architecture, systems security, and formal methods. She also designed the Secure Hardware Design (SHD) course, now widely adopted by universities worldwide to teach computer architecture security. Her work and contributions have been recognized with the Sloan Fellowship, IEEE/TCCA Young Computer Architect Award, an NSF CAREER Award, the Intel Rising Star Faculty Award, an ACM Research Highlight, and multiple MICRO Top Picks.