TC: Small: Analysis for a Cloud of Policies: Foundations and Tools

计算机和人类生活在一个由政策控制的世界里。 在最低层，策略决定信息如何在网络中流动;在最高层，它们描述如何在应用程序之间共享用户的个人信息。 当然，作为策略作者的最终用户也会犯错误：规则可能会产生意想不到的后果，多个策略可能会以其作者不希望的方式进行交互。 用户可以从工具中受益，帮助他们理解他们编写和维护的策略。 政策分析是指在这些情况造成危害之前发现它们的严格方法。 考虑到个人和敏感信息迁移到基于云的应用程序，主流策略上下文的分析器对计算基础设施有明显的影响。先前的研究表明，一阶逻辑是捕获和分析许多基于应用程序和网络的策略的合适基础。 特别是，根据调查结果进行的分析为政策制定者提供了具体和详细的反馈。 这个项目的重点是技术，使基于一阶逻辑的真实世界的政策有效的搜索。具体而言，该项目追求（1）一阶逻辑中模型查找算法的基础研究，（2）跨多个抽象级别（如云计算中发现的）分析策略联合的方法，（3）处理额外的策略功能，如数字约束和动态网络路由，以及（4）根据需求或场景自动生成策略修复的方法。 PI现有的Margrave策略分析器可以作为这项研究的测试平台和部署工具。

Computers and people live in a world governed by policy. At the lowest level, policies determine how information flows within networks; at the highest level, they describe how users' personal information is shared across applications. Of course, end-users, as policy authors, make mistakes: rules can have unintended consequences and multiple policies can interact in ways that their authors didn't intend. Users can benefit from tools to help them understand the policies they write and maintain. Policy analysis refers to rigorous methods for detecting these situations before they cause harm. Given the personal and sensitive information migrating to cloud-based applications, analyzers for mainstream policy contexts have clear impact on computing infrastructure.Prior research has shown that first-order logic is a suitable foundation for capturing and analyzing many application- and network-based policies. In particular, analyses based on scenario-finding provide concrete and detailed feedback for policy authors. This project focuses on techniques to make scenario-finding effective for real-world policies based on first-order logic. Specifically, the project pursues (1) foundational research on algorithms for model-finding in first-order logic, (2) methods to analyze federations of policies across multiple levels of abstraction (such as found in cloud computing), (3) handling additional policy features such as numeric constraints and dynamic network routing, and (4) methods to automatically generate repairs to policies against requirements or scenarios. The PIs' existing Margrave policy analyzer serves as a testbed and deployment vehicle for this research.