Programming, Verifying, Visualizing, and Deploying Browser Extensions with Fine-grained Security Policies

An environment is described which enables the generation, analysis, and use of secure browser extensions. Each browser extension includes an extension body and a policy expressed in a logic-based specification language. The policy specifies the access control and dataflow privileges associated with the extension body in a fine-grained manner by leveraging the structure and content of resources that are accessible to the browser extension. A suite of analysis tools for testing the safety of the browser extension includes a visualization module identifies features of a resource that are accessible to the policy. A static analysis module uses a static analysis technique to determine whether the extension body satisfies the policy. The environment also includes a conversion module for converting the browser extension, once deemed safe, into a form for use by a particular type of browser. The browser can execute that extension without performing runtime safety checks.