Enabling Practical Cross-domain Logic-based Access Control

点击翻译按钮获取中文摘要

Access control is one of the key aspects of information security. Inthe past decade and a half, significant progress has been made inincreasing the assurance and expressiveness offered by access-controlsystems, in large part through the use of formal logics to model orimplement these systems.A particular challenge in building access-control systems is to allowdelegation between domains that use different authorization logics.This project focuses on developing a framework for interfacingdifferent, mutually incompatible authorization logics. The frameworkprovides an interface for communication between logics via a verysmall set of primitives that imposes no fundamental constraints on thedesign of the logics that use it. Part of this framework will be anarchitecture to facilitate the automated construction of proofs ofaccess.Another barrier to implementing logic-based access-control systems isthat substantial effort is typically required to retrofit existingsystems to support the use of theorem provers, proof checkers, andassociated infrastructure. This project will investigate severalapproaches to solving this problem, including automated programrewriting and automated construction of lightweight theorem proversand proof checkers.