Skip to main content

Techniques for Compositional Security: Foundations, Mechanized Reasoning and Applications

Researchers: Anupam Datta, Limin Jia, Deepak-Garg

Research Area: Trustworthy Computing Platforms and Devices

Cross Cutting Thrusts: Formal Methods | Software Security

Abstract

Scope: 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. Such attacks have shown up in the wild in many different settings,  including web browsers and infrastructure, network protocols and infrastructure, and application and systems software. While there has been progress on understanding secure composition in specific settings, such as information flow control for non-interference-style properties and network protocols understanding of the general problem of secure composition has not emerged yet. The proposed project will address this important problem by developing a general model of systems and adversaries, a precise formulation of the secure composition problem in this model, and techniques for modular reasoning and design. The technical approach will build on successful techniques for modular reasoning about system correctness (e.g., rely-guarantee), which work when all programs or their invariants are known. In computer security, however, it is unreasonable to assume that the adversary’s program is known a priori. Furthermore, the adversary may be able to supply executable programs to the trusted system at run time. This additional complexity raises new scientific challenges for compositional security. A central idea, which will be developed fully in the proposed project, 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, the proposed project will develop 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.

Outcomes: Compositional Reasoning: The project will codify compositional reasoning principles in the logic of programs for trusted programs whose programs are known and interface-confined untrusted code. In order to reason about dynamically loaded code, we intend to expand the logic of programs with first-class code, and higher-order reasoning principles, building upon existing work on Hoare Type Theory and its concurrent extensions. Finally, we plan to add to the logic of programs forms of rely-guarantee reasoning in the presence of adversaries. In combination with reasoning about interfaces and first-class code, this will provide a general foundation for compositional security.

Web Security Case Study: The modeling and compositional reasoning framework developed in the project will be used 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, endto- end security properties, attacks in the wild, and ways to defend and prove web applications secure against these attacks. The study could have impact on security mechanisms and policies used in web applications in practice. We expect the case study to exercise all features of our programming model and all compositional reasoning principles including the higher-order extensions and rely-guarantee reasoning.

Mechanization: The reasoning methods developed in the project will be mechanized as a tool to check that programs and interfaces satisfy given specifications in our logic of programs. The mechanization will rely on standard theorem provers to discharge verification conditions, and require user input to specify invariants of interfaces. The mechanized tool will be used in teaching a class at our university and also released under a liberal open-source license for use in research, teaching, and industry.