Enabling Practical Cross-domain Logic-based Access Control

实现实用的基于跨域逻辑的访问控制

• 批准号: 0917047
• 负责人: Ljudevit Bauer
• 金额: $ 43.56万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0917047&HistoricalAwards=false
• 关键词: Enabling; Practical; Cross; domain; Logic

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.

访问控制是信息安全的关键方面之一。 在过去的十五年里，在提高访问控制系统提供的保证和表达能力方面取得了重大进展，这在很大程度上是通过使用形式逻辑来建模或实现这些系统的。构建访问控制系统的一个特殊挑战是允许授权使用不同授权逻辑的域之间。该项目重点开发一个框架，用于连接不同的、相互不兼容的授权逻辑。 该框架通过非常小的一组原语提供了逻辑之间通信的接口，这些原语对使用它的逻辑的设计没有任何基本限制。 该框架的一部分将是促进访问证明的自动化构建的体系结构。实现基于逻辑的访问控制系统的另一个障碍是通常需要付出大量努力来改造现有系统以支持定理证明器、证明检查器和相关基础设施的使用。 该项目将研究解决该问题的几种方法，包括自动程序重写和轻量级定理证明器和证明检查器的自动构建。