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.
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. When used to model a system, such logics can confirm that the system exhibits various desirable correctness properties, e.g., that its decision procedure will never erroneously permit an access if such an access is not consistent with access-control policy. These guarantees can be even stronger when the gap between model and system is bridged by making the logical infrastructure part of the system, e.g., when reference monitors require proofs that access requests are consistent with policy. Much of the work on logic-based access control has been in developing expressive and flexible access-control logics. Each of these logics has advantages and disadvantages and is well suited to describe some set of access-control scenarios. Because of this, and for administrative reasons, organizations with different needs will adopt different, possibly incompatible, access-control logics. A particular challenge in building access-control systems is how to allow delegation between domains that use different authorization logics. Instead of trying to develop the authorization logic that all domains should use, this project focused on developing a framework for interfacing different, mutually incompatible authorization logics. The framework we developed provides an interface for communication between logics via a very small set of primitives that imposes no fundamental constraints on the design or nature of the logics that use it. We showed that our framework had desirable theoretical properties -- e.g., that it doesn't interfere with the consistency of the logics that use it -- and developed a modular, efficient proof checker. Beyond broadening the reach of logic-based access control to more realistic, cross-domain settings, the work carried out as part of this project has had several other forms of impact. The prototype proof checker developed for this project showed itself to be a useful infrastructure component for several efforts to build modern access-control infrastructure, including in the context of a distributed, peer-to-peer file system and for (cyber-)physical access to office space via smartphones. Efforts to better understand security policy enforcement in distributed settings led to advances in formal modeling of and reasoning about run-time enforcement in distributed systems. Research carried out as part of this project also led to establishment of several international collaborations, and hence broad dissemination of results, both within and beyond academia.
