Verifying web browser extensions' compliance with private-browsing mode
BS Lerner, L Elberty, N Poole…?- European Symposium on?…, 2013 - Springer
BS Lerner, L Elberty, N Poole, S Krishnamurthi
European Symposium on Research in Computer Security, 2013?SpringerModern web browsers implement a private browsing mode that is intended to leave behind
no traces of a user's browsing activity on their computer. This feature is in direct tension with
support for extensions, which can silently void this guarantee. We create a static 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?…
no traces of a user's browsing activity on their computer. This feature is in direct tension with
support for extensions, which can silently void this guarantee. We create a static 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?…
Abstract
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. This feature is in direct tension with support for extensions, which can silently void this guarantee.
We create a static 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.
We have retrofitted type annotations to Firefox’s apis and to a sample of actively used Firefox extensions. We used the type system to verify several extensions as safe, find actual bugs in several others (most of which have been confirmed by their authors), and find dubious behavior in the rest. Firefox?20, released April?2, 2013, implements a finer-grained private browsing mode; we sketch both the new challenges in this implementation and how our approach can handle them.
Springer