Skip to main content

Principled Approach to Web Security

Researchers: Anupam Datta, Limin Jia, Deepak Garg

Cross Cutting Thrusts: Software Security | Formal Methods

Abstract

Scope:  This project focuses on the following:

  1. Rich access control model for browser resources, like DOM, cookies, local files and remote connections, and its enforcement in browser interfaces using logic-based policies and proof-carrying authorization.
  2. New scripting language that relies on these interfaces and, in addition, controls flow of information between frames, users and remote web sites in accordance with user-approved policies.
  3. Web browser extension that compiles the language to JavaScript and provides runtime support to the compiled code.
  4. Formal description of adversaries that threaten compiled programs and a formal proof that compilation preserves relevant security properties in the face of such adversaries.

Outcomes: Provide a systematic approach to client-side security. Publish designs and theoretical results in research papers and technical reports. Implementation of the language will be released under a permissive open-source license.

Technical Report: Compositional System Security in the Presence of Interface-Confined Adversaries