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 anddevelopers' 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-applicationcommunication protocols via program verification. 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 Certication of Symbolic Transaction (CST) that verifies the security properties of every web transaction on-the-y byinvoking static verication at runtime. The threat model we consider in this thesis is thestandard 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 CSTto ve commercially deployed applications to secure APIs from well-known companiesincluding Facebook, Amazon, PayPal, and Microsoft.