Enabling Practical Cross-domain Logic-based Access Control

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Access control is one of the key aspects of information security. In the past decade and a half, significant progress has been made in increasing the assurance and expressiveness offered by access-control systems, in large part through the use of formal logics to model or implement these systems. A particular challenge in building access-control systems is to allow delegation between domains that use different authorization logics. This project focuses on developing a framework for interfacing different, mutually incompatible authorization logics. The framework provides an interface for communication between logics via a very small set of primitives that imposes no fundamental constraints on the design of the logics that use it. Part of this framework will be an architecture to facilitate the automated construction of proofs of access. Another barrier to implementing logic-based access-control systems is that substantial effort is typically required to retrofit existing systems to support the use of theorem provers, proof checkers, and associated infrastructure. This project will investigate several approaches to solving this problem, including automated program rewriting and automated construction of lightweight theorem provers and proof checkers.