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.