CSE Colloquium: Better Foundations for Secure Software: Minimize Trust and Verify It

Zoom Information 

Join from PC, Mac, Linux, iOS or Android: https://psu.zoom.us/j/698086820 

or iPhone one-tap (US Toll): +13126266799,698086820# or +16468769923,698086820# 

or Telephone: 

Dial: 

+1 312 626 6799 (US Toll) 

+1 646 876 9923 (US Toll) 

+1 253 215 8782 (US Toll) 

+1 301 715 8592 (US Toll) 

+1 346 248 7799 (US Toll) 

+1 669 900 6833 (US Toll) 

Meeting ID: 698 086 820 

International numbers available: https://psu.zoom.us/u/adBsnTPXaN 

Abstract: Software systems are ever-growing in size and complexity while being rife with vulnerabilities. Patches and defenses are continuously deployed, but the software attack surface is extremely large and attackers invariably find ways to gain a persistent foothold. An effective way to end the arms race between vulnerabilities and defense tools is by isolating the software using trusted hardware. With such isolation, what is the least amount of code that needs to be bug-free to securely run user applications? At the moment, even after using trusted hardware, this number can be upwards of a few million lines of code. Can we do any better? In this talk, I present two key results from my work that shows a foundational approach to safeguard applications against large and potentially buggy software. First, I present a principled way of using hardware isolation to securely execute Linux applications while only trusting a few thousand lines of code. This system has been adopted by two startups. Second, I show the feasibility of full formal verification of the trusted code by proving guarantees over a large subset, such as the file system interface. Overall, these implementations point to a new way of executing secure applications with a thousand lines of trusted and verified code. Finally, I will summarize my long-term vision for building the next generation of better, trusted, and verified secure hardware and software designs. 

Biography: Shweta Shinde is a postdoctoral scholar at UC Berkeley. Her research is broadly at the intersection of trusted computing, system security, program analysis, and formal verification. Her work has been published at top venues in security (IEEE S&P, CCS, Usenix Security, NDSS), programming languages (PLDI), and software engineering (FSE). Her research has been commercialized at three start-ups and has led to a direct impact at various companies. Shweta received her Ph.D. from the National University of Singapore in 2018 where she was awarded the Dean's Graduate Research Excellence Award for her research. 

Webpage: https://people.eecs.berkeley.edu/~shwetas