TITLE: Better Foundations for Secure Software: Minimize Trust and Verify It
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.
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.