Abstract
The web is our primary gateway to many critical services and offers a powerful platform for emerging applications. However, security of the web platform is a major concern. Web vulnerabilities are pervasive, yet techniques for finding and defending against them are at a nascent stage. How can we build a secure web platform for the future? Towards this goal, my work investigates a broad range of solutions including new browser abstractions, languages, verification techniques and analyses. I present two examples of my work which introduce formal foundations into practical systems used in today’s web platform. First, I present a system for automatically finding vulnerabilities in JavaScript applications using dynamic symbolic execution. This system has discovered several previously unknown flaws in widely used web applications without raising any false positives. A key feature that enables this precision is our new decision procedure for handling complex string operations found extensively in real-world code. In the second example, I present a new type system for ensuring integrity of web application code by construction. The type system is designed to be bolted onto existing web frameworks and has been adopted in the compilation infrastructure for commercial web applications such as Google+. These examples demonstrate that by developing new formal techniques which can be realized in practical systems, we can build a web platform that is secure by construction.
Brief Biography
Prateek Saxena is a PhD student in Computer Science at UC Berkeley. His research interests are in computer security and its areas of intersection with programming languages, formal methods, compilers and operating systems. His current work focuses on software and web security. He is the recipient of several awards, including the Symantec Research Fellowship Award in 2011 and the AT&T Best Applied Security Paper Award in 2010.
