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.