Software Research Talk: Provably Secure Computing using Certified Software and Trusted Hardware, Prof. Sanjit Seshia from Berkeley

Software Research Talk

Title: Provably Secure Computing using Certified Software and Trusted Hardware
Speaker: Prof. Sanjit Seshia from Berkeley
Date: November 9, 2017
Time: 1:30pm
Location: Gates 415

Security-critical applications face a range of threats including exploits in privileged software such as the operating system and hypervisor. In order to protect sensitive data from such privileged adversaries, there is increasing interest in developing and using secure hardware primitives, such as Intel SGX, ARM TrustZone, and Sanctum RISC-V extensions. In this talk, I will discuss the problem of building applications with provable security guarantees by including only these hardware primitives (and very little software) in the trusted computing base. We have developed compiler and verification techniques to develop applications that can be verified (at the level of machine code) to not leak secrets, both via their outputs and certain side channels.
Furthermore, I will discuss how formal models of trusted hardware can be leveraged to
port programs and their correctness proofs across different hardware platforms.

Sanjit A. Seshia is a 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, with a current focus on the areas of cyber-physical systems, computer security, 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, and the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education.

Thursday, November 9, 2017 - 1:30pm to 2:30pm
Gates Computer Science, 353 Serra Mall, Stanford, CA 94305, USA