Epistemic models for security - October 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 structuring of the features of our security language to effectively enforce authorization policies. There are multiple features that represent different aspects of the policy. The authorization logic itself is represented by an encoding of the basic proof constructors of the logic at the level of the type system. These constructors define the universal rules of the logic such as how to form an implication or conjunction. A type signature encodes the specific rules of a given policy for authorization. For example, a given policy may say that if Alice affirms that Bob is her health care proxy then any access that Bob grants to Alice's records will also be granted by Alice implicitly. The third feature for representing the policy is a library of functions for interacting with the entities and objects involved in the policy. The results of these library calls are only determined dynamically, but these results affect how the policy should be enforced for any given run of the program. If Alice affirms that Bob is her health care proxy in one execution of the program but does not in another execution, then the access granted in these two executions will differ accordingly based on the rest of the policy. This structure permits us to statically verify that proofs constructed dynamically are valid provided that the library functions behave as specified. That is to say the proofs are valid up to the contextually relevant components supplied dynamically.