Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
IBEX: 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. The IBEX project develops a foundational view of browser extension security, and provides a way to build extensions that are verifiably secure.


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 an ML dialect called F* to either .NET or JavaScript, facilitating cross-browser deployment of extensions.  


To date, we have implemented and verified 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.

Currently underway: A new frontend to IBEX which allows translating extensions authored in JavaScript into F* for verification.

  • Arjun Guha, Matthew Fredrikson, Benjamin Livshits, and Nikhil Swamy, Verified Security for Browser Extensions, in Proceedings of the IEEE Symposium on Security and Privacy (Oakland), IEEE, 22 May 2011.