Mengjia Yan "The Interplay of Efficient Formal Verification and Secure Processor Design"
- Sponsor
- Siebel School of Computing and Data Science
- Speaker
- Mengjia Yan, Associate Professor within the Electrical Engineering and Computer Science Department at MIT
- Contact
- Anthony Raucci
- raucci@illinois.edu
- Phone
- 217-300-0198
- Originating Calendar
- Siebel School Speakers Calendar
Abstract:
Modern systems are built on complex software and hardware, creating a large attack surface and a fragile trusted computing base (TCB). This talk focuses on how formal verification can help secure this system stack by offering rigorous security guarantees, and how security insights can in turn help make verification more effective.In the first part of the talk, I will discuss how insights about secure processor design can be used to scale formal verification to much more complex hardware than previously possible. In the second part, I will broaden the scope to the software-hardware boundary, and show how reasoning about security at the assembly level can significantly reduce the TCB and offer stronger guarantees. Overall, the talk highlights how verification and security insights can inform each other in building more trustworthy systems.
Bio:
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.