Secure Composition of Systems and Policies - January 2015

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Anupam Datta, Limin Jia
Co-PI(s):
Researchers:

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
This refers to Hard Problems, released November 2012.

Scalability and Composability

Our work addresses the Scalability and Composability problem. The reasoning principles we have developed allow both sequential and parallel composition of programs. Our program logic takes into consideration that components execute in a potentially adversarial environment, and therefore, the compositionality of components in the presence of adversaries is built into our semantic model.

2) PUBLICATIONS

A Logic of Programs with Interface-confined Code
Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta
Accepted to The Computer Security Foundations Symposium (CSF)

3) KEY HIGHLIGHTS

Interface-confinement is one of the common mechanisms that secure untrusted code by executing it inside a sandbox that confines its interaction with key system resources to a restricted set of interfaces. This practice is seen in Web browsers, hypervisors, and other security-critical systems. Motivated by these systems, we developed a program logic for modeling and proving safety properties of systems that execute adversary-supplied code via interface-confinement. System M is the first program logic that allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep typing analysis. System M can be used to model and verify protocols as well as system designs.