Modern Web browsers provide a "private browsing" mode, wherein the browser does not record the user's behavior such as which sites they visited. This mode is valuable to users of all stripes, from the privacy-conscious to those those worried about persecution by totalitarian regimes. Browser implementers therefore take great care to try to ensure these modes function correctly. However, modern browsers are highly extensible: users can install extensions to customize their browser, and millions have done so. Unfortunately, it is technically challenging for browsers to automatically flag which extensions are privacy-preserving and which are not, so browsers currently do not attempt to offer such guidance -- leaving users to fend for themselves. This work presents a type system for verifying whether extensions violate private browsing mode. The types distinguish Safe values (that may always be used in private mode) from Unsafe ones (that may lead to privacy violations). The type system is engineered to be "lightweight": extensions that never perform unsafe actions should type check without changes, and extension authors must only annotate their extension code when an unsafe action is used. Extensions that pass this check are accompanied by a guarantee that they do not perform privacy-violating actions, and are thus safe to install in private-browsing mode.
TWC: Small: Extensible Web Browsers and User Privacy