The Community for Technology Leaders
2011 IEEE Symposium on Security and Privacy (2011)
Oakland, California USA
May 22, 2011 to May 25, 2011
ISSN: 1081-6011
ISBN: 978-0-7695-4402-1
pp: 115-130
ABSTRACT
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 \ibex, a new framework for authoring, analyzing, verifying, and deploying secure browser extensions. Our approach is based on using type-safe, high-level languages to program extensions against an API providing access to a variety of browser features. We propose using Data log to specify fine-grained access control and dataflow policies to limit the ways in which an extension can use this API, thus restricting its privilege over security-sensitive web content and browser resources. We formalize the semantics of policies in terms of a safety property on the execution of extensions and develop a verification methodology that allows us to statically check extensions for policy compliance. Additionally, we provide visualization tools to assist with policy analysis, and compilers to translate extension source code to either. NET byte code or JavaScript, facilitating cross-browser deployment of extensions. We evaluate our work by implementing and verifying~\NumExt extensions with a diverse set of features and security policies. We deploy our extensions in Internet Explorer, Chrome, Fire fox, and a new experimental HTML5 platform called C3. In so doing, we demonstrate the versatility and effectiveness of our approach.
INDEX TERMS
security, verification, type system, policy languages, web browsers, extensions
CITATION

B. Livshits, M. Fredrikson, N. Swamy and A. Guha, "Verified Security for Browser Extensions," 2011 IEEE Symposium on Security and Privacy(SP), Oakland, California USA, 2011, pp. 115-130.
doi:10.1109/SP.2011.36
126 ms
(Ver 3.3 (11022016))