Epistemic models for security - July 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 main highlight of the past quarter has been the extension of our language to embed the authorization logic within the type system. We represent proofs of authorization at the level of types so that static checking verifies that the proofs are well formed. These are open proofs that have holes for assumptions that are supplied dynamically at runtime. Filling these holes represents consulting an authorization server or other resource that monitors the dynamic state of the authorization policy. The authorization server is responsible for filling in the contextually relevant components of the authorization proofs that are not available statically. In this way, we can verify that the proofs are well formed up to the success of dynamic library calls to the server.

Representing the authorization proofs in this way allows us to use existing machinery to check the proofs as part of type checking. However, it also imposes limitations on how expressive we can make the embedded authorization logic. To verify that the logic is sufficiently expressive, we have also devised a few example applications and represented them in this style. One interesting example is the encoding of access constraints on patients' health records. There are several ways that access to a patient's record may be granted to a physician: the patient may explicitly consent, the patient may need urgent medical care, the patient may authorize a relative to consent for him or her, etc. We are able to encode these various situations in our authorization logic.