Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired end-to-end security property: an adversary may exploit complex interactions between components to compromise security.
This project addresses this important problem by developing a general model of systems and adversaries and techniques for modular reasoning and design. A central idea is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is constrained to the interfaces it has access to, but may combine interface calls without restriction. At a technical level, we are developing an expressive concurrent programming language with recursive functions for modeling interfaces and higher-order data for modeling code obtained at run time, and a logic of programs to capture reasoning principles for compositional security. We are using this framework to develop a systematic basis for web security, to formalize attacker models for web browsers proposed in literature and develop new ones, and to build an understanding of relevant security policies, end-to-end security properties, attacks in the wild, and ways to defend and prove web applications secure against these attacks. This study could have impact on security mechanisms and policies used in web applications in practice. The reasoning methods developed in the project will be mechanized in a tool.
