CT-ISG: Collaborative Research: A New Approach to Testing and Verification of Security Policies

基于策略的访问控制是在应用程序和网络级别实现隐私和安全的最基本和最广泛使用的机制之一。考虑到安全策略的高度重要性和微妙性，确保这些策略的正确性很重要，但也很困难。安全政策中的一个微小错误可能导致无法弥补的后果，如果不是悲惨的话。因此，确定政策规格与其预期功能之间的差异是一项至关重要的任务。为了实现这一目标，该项目采用了一种新的方法来测试和验证安全策略，包括应用程序级安全策略（如XACML策略）和网络级安全策略（如防火墙策略）。为了实现这一点，该项目正在定义两种统一的安全策略表示：程序代码表示和决策树表示。第二，该项目正在开发一套严格和系统的安全政策测试技术。第三，该项目正在寻求安全策略的有效和可扩展的验证和更改影响分析技术。第四，这个项目探索了测试和验证有状态安全策略的方法。该项目正在开发用于测试和验证应用程序级和网络级安全政策的框架和技术。该项目还将产生概念和理论，从根本上推进安全政策的知识和理解。由NSF支持的研究产生的概念，理论，算法和工具有望促进严格的安全策略测试和验证实践，这将导致更好的策略质量和更高的安全保证。此外，这项研究的结果将使依赖于安全策略正确性的相关领域的进一步创新成为可能。

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.