Secure Composition of Systems and Policies - April 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

System M: A Program Logic for Code Sandboxing and Identification
Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta
In preparation to be submitted to The Computer Security Foundations Symposium (CSF)

3) KEY HIGHLIGHTS

After completing the design of a program logic for reasoning about two key security mechanisms--sandboxing and code identification--for ensuring the security of systems that execute adversary code, we began to investigate how to extract an abstract model of systems that execute adversary-supplied code, independently of the specification language of the system properties. The current program logic and its semantic model are tied to trace properties specified in first-order logic, however, we believe that there is a general semantic model behind such systems.