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 systematically introduce formal foundations
into 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 realworld
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.