Sound JavaScript Analysis for Securing Browser Addons

JavaScript is a ubiquitous language on the Web; it is used not only to enhance web pages, but also to enhance the functionality of web browsers themselves in the form of browser addons. These addons have almost complete access to a user’s information: browser history, cookies, passwords, clipboard, geo-location, mouse and keyboard actions, the local file system, and more. Malicious addons that steal this information and send it over the network are trivially easy to write, and yet can be difficult to detect; several real-world examples of such addons have made recent news. Therefore, vetting third-party addons is critical both for users (whose information is at risk) and for browser providers (whose reputations are at risk). However, the current vetting process for addons submitted to official addon repositories is manual, ad-hoc, and error-prone.

These observations motivate a sound static analysis for JavaScript that can largely automate the vetting of JavaScript-based addons. Unfortunately, a sound, precise, and tractable analysis of any sort for the full JavaScript language does not currently exist. This is due to the inherent dynamic nature of JavaScript, its obscure and surprising corner-cases, confusing implicit type conversions, and other behaviors that make analysis difficult. However, soundness is a critical requirement for vetting addons, since attackers can take advantage of any unsoundness in the analysis to escape detection.

In this talk I will describe JSAI, a provably-sound JavaScript abstract interpreter we have developed in the PL Lab at UC Santa Barbara. JSAI is based on a formally-specified translation from JavaScript to an intermediate language called notJS, and an abstract semantics derived directly from a formal concrete semantics. The implementation of the abstract interpreter is in almost one-to-one correspondence with the formalisms. I will provide empirical evident of JSAI’s effectiveness on real-world JavaScript programs. Finally, I will discuss preliminary results from applying JSAI to the problem of vetting browser addons. We have early results from running a JSAI-based secure information flow analysis on a large corpus of real Mozilla Firefox addons; these results are encouraging and demonstrate the practicality and effectiveness of our approach.

Speaker Bios

Ben Hardekopf is an assistant professor in the Computer Science Department at the University of California, Santa Barbara. He received his Ph.D. from the University of Texas at Austin in 2009. His research interests are in programming languages with an emphasis on program analysis.