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.
