This research project helps secure the privacy of web browser users. It specifically targets the browser addon framework, which allows third-party developers to extend the browser's functionality. These addons are written in JavaScript and have extraordinary privileges and access to sensitive user information. Therefore, vetting third-party addons to prevent malicious or accidental security violations is critical. However, the current vetting process for browser addons is manual and ad-hoc, making this process both tedious and error-prone. The goal of this research project is to enhance and automate addon vetting by using static analysis for JavaScript to enforce formal security policies. The approach taken by this project is three-fold: (1) design formal security policies to provide provable guarantees; (2) create a provably-sound static security analysis for JavaScript-based browser addons; and (3) develop new tools for explaining security problems in addon code so that third-party developers can revise insecure add ons to eliminate vulnerabilities. This work benefits society as a whole by giving people assurance that their sensitive information is being treated securely. The work also benefits academia and industry by providing the first-ever provably-sound JavaScript static analysis for browser addons. The techniques that are developed will advance understanding of how to usefully analyze dynamic languages such as JavaScript, and the analysis framework itself will enhance research infrastructure by providing a platform for researchers to develop static analyses for JavaScript.
SHF: Small: Static Analysis for Safe Browser Addons