Policy-based access control is one of the most fundamental and widely used mechanisms for achieving privacy and security at both application and network levels. Given the high importance and delicacy of security policies, ensuring the correctness of these policies is important, and yet difficult. A tiny error in security policies could lead to irreparable, if not tragic, consequences. Therefore, identifying discrepancies between policy specifications and their intended function is a crucial task. To achieve this goal, this project pursues a new approach to testing and verification of security policies, including application-level security policies (such as XACML policies) and network-level security policies (such as firewall policies). To accomplish this, this project is defining two unified representations for security policies: program code representation and decision tree representation. Second, the project is developing a suite of rigorous and systematic security policy testing techniques. Third, this project is pursuing efficient and scalable verification and change-impact analysis techniques for security policies. Fourth, this project explores methods for testing and verifying stateful security policies. The project is developing frameworks and techniques for testing and verifying both application-level and network-level security policies. The project will also produce concepts and theories that fundamentally advance the knowledge and understanding of security policies. The concepts, theories, algorithms, and tools produced by this NSF-supported research are expected to promote rigorous security policy testing and verification practice, which will lead to better policy quality and higher security assurance in general. Furthermore, the results of this research will enable further innovations in related fields that depend on the correctness of security policy.
