Epistemic Models for Security - October 2014

Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.

PI(s): Robert Harper (CMU)
Co-PI(s):
Researchers:

HARD PROBLEM(S) ADDRESSED
Scalability and Composability

Our work addresses the hard problem of scalability and composability. Programs whose security has been expressed through their types in a secure type system are inherently composable. Our framework for defining and reasoning about secure programs helps develop provably secure components that can be combined to create a secure system.

PUBLICATIONS
N/A

ACCOMPLISHMENT HIGHLIGHTS

Key Highlights:

* Our methodology can prove useful properties about what flows of information are and are not possible as a result of concrete authorization policies. We investigated specific example policies and reasoned about the epistemic consequences of programs adhering to these policies.

* Timing channels become important when programs running on behalf of different principals all interact with a central certificate authority that regulates the policy statements made by various principals. We found in related work that timing channels can be substantially mitigated by placing a buffer between the program and the certificate authority.