CT-ISG: Representation, Analysis, and Verification of Access Control in Dynamic Environments

自定义控制策略已经从简单的矩阵发展为非平凡的规范：它们与使用它们的应用程序分开，用特定于域的语言编写;它们通常由以下内容组成：（有时是地理上分布的）片段，使用语义丰富的策略组合操作符组合这些片段;并且它们咨询由来自包括系统的底层应用和操作环境的许多源的信息组成的动态环境。 这些特征使得政策很难正确，部分原因是政策制定者必须了解他们的政策将如何与不断变化的环境相互作用。因此，政策制定者需要越来越强大的工具来帮助理解他们的政策的效果。 这些工具必须支持常见的创作场景。 作者通常有一个“有效”的策略和一个封装了所需更改的新策略。 测试可以增强信心，使更改达到预期的效果，但通常会错过预期之外的效果。 对于这样的场景，采用诸如变更影响分析之类的过程要有用得多，该过程在考虑环境的动态特性的同时从语义上比较两个策略。 传统的基于属性的分析，如形式验证，虽然有用，不支持这种情况下，本项目正在开发的理论基础和原型工具，分析现实的访问控制策略在其动态环境。 这些工具支持基于属性的验证和无属性的分析，例如对工业标准策略语言（如XACML）的更改影响分析。 这个项目的新颖组件是它的细粒度和丰富的动态环境模型，以及它对适应常见创作场景的无属性分析的关注。

Access-control policies have grown from simple matrices to non-trivial specifications in their own right: they are written, separately from the applications that use them, in domain-specific languages; they are often composed of (sometimes geographically distributed) fragments, which are combined using semantically rich policy-combination operators; and they consult a dynamic environment comprised of information from many sources including the underlying application and the operating environment of the system. These features make policies hard to get right, in part because policy authors must understand how their policies will interact with an environment that is constantly changing.Policy authors thus need increasingly strong tools to help understand the effects of their policies. These tools must support common authoring scenarios. Authors often have a policy that "works" and a new policy that encapsulates a desired change. Testing can foster confidence that the changes do what is desired, but generally miss effects that weren't expected. For such scenarios, it is far more useful to employ a process such as change-impact analysis, which semantically compares two policies while respecting the dynamic nature of the environment. Traditional property-based analyses such as formal verification, while useful, do not support this scenario.This project is developing the theoretical foundations and prototype tools for analyzing realistic access-control policies in their dynamic environments. The tools support both property-based verification and property-free analyses such as change-impact analysis for industrial standard policy languages (such as XACML). The novel components of this project are its fine-grained and rich model of the dynamic environment and its focus on property-free analyses that accommodate common authoring scenarios.