Epistemic models for security - April 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 the past quarter is the successful extension of our methodology to enforce progress-sensitive non-interference (PSNI) of concurrent communicating processes. As noted in related work, PSNI is a security condition that is preserved under parallel composition, unlike many weaker non-interference variants for concurrent processes. As with other composability results, this means that the individual components of a large system can all be verified as satisfying PSNI independently and that their parallel composition to form the full system will also satisfy this property. We have extended our methodology of reasoning about flows of knowledge due to traces of sequential programs to these concurrent programs by building an epistemic model of the additional flows of knowledge engendered by concurrent execution.

Unfortunately, PSNI is an extremely restrictive property. Our moderately conservative method for enforcing PSNI is to prevent processes from sending low messages after they have received a high message. While this restriction may be considered excessively severe, ruling out many seemingly benign programs is necessary in the concurrent setting to avoid unintended leaks of information. However, the power of concurrency also somewhat relaxes this condition. A program that plans to emit a low message in the future cannot receive any high messages itself, but it can spawn a child process to interact on high security channels while maintaining its own ability to send low messages. In this way, the ability to spawn child processes mollifies the severe restrictions of PSNI.