Computer-Aided Formal Security Analysis of the Web Platform

Over the last two decades, a set of standards published by the W3C, IETF and WHATWG was consolidated to form the Web Platform, a full-fledged application platform as opposed to the initial design of the Web as a set of hyperlinked documents. The current state of the standardization of the Web, fragmented into a multitude of documents maintained by different organizations, complicates the process of reasoning about the security of the platform as a whole. This led to the introduction of vulnerabilities originating from unforeseen interactions between different Web components. This situation stems from the fact that Web specification often include informally-defined or implicit assumptions about the security of other features. In this thesis we argue for the need of a rigorous and formal definition of Web security in terms of invariants that are guaranteed to be valid across the Web platform. In particular, in this work, we study the security mechanisms of the modern Web and formalize them in the form of Web invariants. We propose two methodologies for validating Web invariants on a new model of Web specifications (WebSpec) and on browser implementations (Chromium, Firefox, Safari) that allowed us to discover new inconsistencies and propose sound mitigations. We then focus on application security and study the lesser-known Web threat model of the related domain attacker, measuring its impact on the security of the most popular sites on the Web. Finally, we turn our attention to cookies and their long history of vulnerabilities, discussing new violations of their integrity protections and new attacks enabled by related-domain attackers.