Verifying Web Browser Extensions’ Compliance with Private-Browsing Mode
Benjamin S. Lerner, Liam Elberty, Neal Poole, and Shriram Krishnamurthi
  author = {Benjamin S. Lerner and Liam Elberty and Neal Poole
            and Shriram Krishnamurthi},
  title = {Verifying Web Browser Extensions' Compliance with 
           Private-Browsing Mode},
  booktitle = {European Symposium on Research in 
               Computer Security (ESORICS)},
  year = {2013},
  month = sep

Modern web browsers implement a private browsing mode that is intended to leave behind no traces of a user's browsing activity on their computer. Currently, browser vendors ensure they have implemented this intent through subtle, whole-program reasoning about the browser. As a result, this feature is in direct tension with support for extensions, which let users add third-party functionality into their browser. To date, Mozilla and Google have taken different approaches in their support for extensions in private browsing mode, but both approaches are suboptimal and neither can reliably verify the behavior of extensions.

We tackle this problem by creating a type system to analyze JavaScript extensions for observation of private browsing mode. Using this type system, extension authors and app stores can convince themselves of an extension's safety for private browsing mode. In addition, some extensions intentionally violate the private browsing guarantee; our type system accommodates this with a small annotation overhead, proportional to the degree of violation. These annotations let code auditors narrow their focus to a small fraction of the extension's codebase.

This paper explains the design of the type system, highlighting the new features needed to handle potentially-but-not-always unsafe APIs. We evaluate our system by retrofitting type annotations to Firefox's APIs and to a sample of actively used Firefox extensions, and discuss some of the challenges involved. Finally, we used the type system to verify several extensions as safe, find actual bugs in several others (which have been confirmed by their authors), and find dubious behavior in the rest.