Verified Security for Browser Extensions

Popup blocking, form filling, and many other features of modern web browsers were first introduced as third-party extensions. New extensions continue to enrich browsers in unanticipated ways. However, powerful extensions require capabilities, such as cross-domain network access and local storage, which, if used improperly, pose a security risk. Several browsers try to limit extension capabilities, but an empirical survey we conducted shows that many extensions are over-privileged under existing mechanisms.

This paper presents a comprehensive new model for extension security that aims to redress the shortcomings of existing extension mechanisms. Our model includes various components. First, we develop a logic-based specification language for describing fine-grained access control and data flow policies that govern an extension’s privilege over web content. We show how to understand security policies by providing visualization tools that highlight the impact of a policy on particular web pages. We formalize the semantics of policies in terms of a safety property on the execution of extensions and we develop a verification methodology that allows us to statically check extensions for safety. Static verification eliminates the need for costly runtime monitoring, and increases robustness since verified extensions cannot raise security exceptions. We also provide compiler tools to translate extension code authored in ML to either .NET or JavaScript, facilitating cross-browser deployment of extensions.

We evaluate our work by implementing and verifying 17 extensions with a diverse set of features and security policies. We deploy our extensions in Internet Explorer, Chrome, Firefox, and a new experimental HTML5 platform called C3. In so doing, we demonstrate the versatility and effectiveness of our approach.