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.