Towards a Formal Foundation of Web Security
To Appear at the 21st Usenix Security Symposium (Usenix Security) , August 2012
@Misc{akhawe12formal,
author = {Devdatta Akhawe and Adam Barth and Peifung Eric Lam and John Mitchell and Dawn Song},
title = {Towards a Formal Foundation of Web Security},
booktitle = {Proc. of the 23rd IEEE Computer Security Foundations Symposium (CSF), Edinburgh 2010},
year = {2010},
}
Abstract
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.