Team for Research in
Ubiquitous Secure Technology

Towards a Formal Foundation of Web Security
Devdatta Akhawe

Citation
Devdatta Akhawe. "Towards a Formal Foundation of Web Security". Talk or presentation, 10, November, 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.

Electronic downloads

Citation formats  
  • HTML
    Devdatta Akhawe. <a
    href="http://www.truststc.org/pubs/762.html"
    ><i>Towards a Formal Foundation of Web
    Security</i></a>, Talk or presentation,  10,
    November, 2010.
  • Plain text
    Devdatta Akhawe. "Towards a Formal Foundation of Web
    Security". Talk or presentation,  10, November, 2010.
  • BibTeX
    @presentation{Akhawe10_TowardsFormalFoundationOfWebSecurity,
        author = {Devdatta Akhawe},
        title = {Towards a Formal Foundation of Web Security},
        day = {10},
        month = {November},
        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.},
        URL = {http://www.truststc.org/pubs/762.html}
    }
    

Posted by Larry Rohrbough on 7 Dec 2010.
Groups: trust
For additional information, see the Publications FAQ or contact webmaster at www truststc org.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.