Epistemic models for security - January 2016

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 programming of a type checker for our core security language. This implementation of our secure type system is an important tool for demonstrating the practicality of our techniques. By using the type system implementation, we can construct more elaborate examples than are conveniently verified on paper. These more elaborate examples will assure us that the technique of encoding the authorization logic and policy at the kind and constructor level of a dependently typed language is practical for a significant range of applications. We have already encoded some simple policy examples in the language and verified that the type checker can validate proofs in the policy. While these example policy rules are relatively small, having an automated type checker will greatly assist in verifying that more complex policies can be enforced in our framework. To achieve this goal, we will augment the implementation of the language with a friendlier user interface that will facilitate the development of more elaborate policies through the judicious use of convenient syntactic sugar. Another goal will be the incorporation of more expressive error messages to assist in correcting invalid policies and programs. An interesting additional problem that may fall beyond the scope of this work is addressing unintended consequences of a policy. While the type checker can verify whether a policy is well formed and validate a proof within the context of that policy, it is not a theorem prover and therefore cannot determine all possible authorization proofs that are possible from a given policy. In the worst case, a policy may be inconsistent and authorize arbitrary access. There may be tools within the theorem prover literature for addressing this issue that could be adapted to our setting.