Towards a Formal Foundation of Web Security

To Appear at the 21st Usenix Security Symposium (Usenix Security) , August 2012


We propose a formal model of web security based on an abstraction of the web platform and use this model to analyze the security of several sample web mechanisms and applications. We identify multiple distinct threat models that can be used to analyze web applications, ranging from a web attacker who controls malicious web sites and clients, to stronger attackers who can control the network and/or leverage sites designed to display user-supplied content. We propose two broadly applicable security goals and study five security mechanisms. In our case studies, which include HTML5 forms, Referer validation, and a single sign-on solution, we use a SAT-based model-checking tool to fid two previously known vulnerabilities and three new vulnerabilities. The case study of a Kerberos-based single sign-on system illustrates key differences between network protocols and web protocols and finds a vulnerability that arises because of the way cookies, redirects, and embedded links are used.

Source Code Release

The Web Security model project is available opensource.