Epistemic models for security - January 2015

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:

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
Scalability and Composability

We are using a combination of methods to achieve modular analysis of the security properties of concurrent imperative programs: a type system based on the lax modality to express and enforce information flow constraints and a novel linear epistemic logic to analyze the execution traces of programs to derive which principals learn which secrets in a given run. We prove that for a well-typed program, a low-security principal can learn a high-security secret only if it is explicitly authorized to do so by an integrated authorization logic. All of these methods, being grounded in logic and type theory, are inherently compositional in nature.

2) PUBLICATIONS
N/A

3) KEY HIGHLIGHTS

The major highlight of this past quarter is the additional application of our technique to concurrent communicating processes. We reason about the potential knowledge transferred through the communicating processes just as we previously reasoned about knowledge transferred through assignments to memory. In both cases, we have a trace of the security relevant actions performed by a sequential or concurrent program, and we reason about the consequences of those actions in a substructural epistemic logic. This advance demonstrates the flexibility of our methodology.

Modeling concurrent interaction of multiple processes significantly widens the scope of this work. Many contexts where security is critical involve several processes communicating while accessing data of various security levels. For example, the scripts executing within a web browser interact in this manner. We hope to successfully apply our technique, which was initially designed for a sequential setting, to this wider range of concurrent programs, and thereby demonstrate that our approach can address security vulnerabilities in a wide scope of programs. Our current conjecture is that many of the issues that arise from concurrency such as timing channel leaks can be resolved by viewing these concurrent programs as a sequential program that schedules between the concurrent threads. In this way, the same techniques that we used to prevent sequential leaks can be adapted to prevent timing channel leaks.