Protecting Incorrectly Implemented Web Applications From Online Adversaries

Implementation errors are commonly found in modern web applications. They can be caused by a multitude of factors, including weaknesses in browsers' security policies and
developers' misinterpretations of web protocols (e.g., OAuth and OpenId). In this thesis, we show that even under the assumption that web applications are implemented incorrectly, their security can be improved through two fronts: 1) Enhancing the application isolation mechanism of web browsers, and 2) securing inter-application
communication protocols via program verification. For 1), we created a mechanism called pp Isolation to enhance isolation boundaries of web applications running inside a browser. For 2), we created a formal verification framework called Certication of Symbolic Transaction (CST) that verifies the security properties of every web transaction on-the-
y by
invoking static verication at runtime. The threat model we consider in this thesis is the
standard web attacker with additional capabilities of a malicious user.
The two defenses proposed in this thesis are lightweight and backward compatible.
App Isolation can be deployed as an opt-in feature for websites; and we have applied CST
to ve commercially deployed applications to secure APIs from well-known companies
including Facebook, Amazon, PayPal, and Microsoft.
i