All modern browsers now support a “private browsing mode”, in which the browser ostensibly leaves behind no traces on the user's file system of the user's browsing session. This is quite subtle: browsers have to handle caches, cookies, preferences, bookmarks, deliberately downloaded files, and more. So browser vendors have invested considerable engineering effort to ensure they have implemented it correctly.
Firefox, however, supports extensions, which allow third party code to run with all the privilege of the browser itself. When not in private-browsing mode, these extensions are permitted to do anything they like...and unfortunately, while in private-browsing mode, they are not tecnically prevented from doing anything, either. What happens to the security guarantee of private browsing mode, then?
We have built a type checker to detect data-leaking actions that might occur while the browser is running in private browsing mode. To a rough first approximation, this type system is similar to the ADsafety system, in that it blocks access to several of Firefox's APIs (e.g., the various ways to write to disk, among other APIs). The essential difference, however, is in encoding the extensions' allowable behaviors in public and private modes as distinct type environments, so that one type-checker suffices for both modes.
blog has a post with more details. For complete detail, our
is available as well. Finally, our type-checker is implemented using our
open-source TeJaS framework, and is available
Github. To use,
src/main.ml on line 9 to set
= BI.Actions, then build and run as normal.