Towards Verified Trusted Computing Platforms with UCLID5
Trusted execution environments (TEEs), combinations of hardware and software that form a trusted computing base, have grown in adoption over the past decade. Concurrently, there is growing awareness of vulnerabilities arising from features of modern microprocessors, such as transient execution attacks. To fully realize the promise of TEEs, one needs to formally verify their design and implementation in the face of such attacks. In this talk, I will discuss the formal verification of trusted computing platforms and the challenges that arise in this problem domain. These challenges motivate the development of a new approach to formal modeling, specification and verification. The UCLID5 project is developing this approach, which includes multi-modal modeling and specification, verification by reduction to synthesis, integration of inductive learning with deductive reasoning, and oracle-guided learning and synthesis. This talk will give an overview of the problem of verifying trusted platforms and the UCLID5 approach, and present some case studies of applying UCLID5 to this problem domain.
Speaker Biography
Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, spanning the areas of cyber-physical systems (CPS), computer security, distributed systems, artificial intelligence (AI), machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award, the Computer-Aided Verification (CAV) Award for pioneering contributions to the foundations of SMT solving, and the Distinguished Alumnus Award from IIT Bombay. He is a Fellow of the ACM and the IEEE.
