Automatic Verification of Distributed and Layered Security Policy Implementations
Automatic Verification of Distributed and Layered Security Policy Implementations
复制标题
分布式分层安全策略实施的自动验证
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Mouna Seri
中科院分区：
文献类型：
--
作者：
Sankalp Singh;W. Sanders;D. Nicol;Mouna Seri
长期以来，访问控制一直是入侵防御的关键。旨在确保安全的现代联网系统具有一个全局策略，该策略通常是隐式的，它指定了关于访问各种资源的总体系统级目标。该策略既指明了哪些是不可接受的，从而可以防止来自网络内部和外部的入侵企图，也指明了必须允许哪些访问，从而使系统的基本功能不会受到损害。该策略通过配置大量本地设备和机制来实现，包括基于路由器和基于主机的防火墙以及自主或强制的基于操作系统的访问控制机制(例如，SELinux)。这些分布式和分层机制之间的复杂交互可能会掩盖问题并导致微妙的错误。在本文中，我们介绍了一个框架，用于对自动获得的访问控制策略实现的快照执行全面的安全分析，以检查是否符合全局访问策略的(可能是部分的)规范。该框架已作为访问策略工具实现。APT允许在高抽象级别上对安全策略进行推理，从而有助于增强对现有入侵防御机制的有效性的信心。我们描述了我们的分析技术，并通过对各种测试用例使用APT来演示它们的效率、可伸缩性和可扩展性。
Access control has long been the linchpin of intrusion prevention. Modern networked systems that are intended to be secure have a global policy, usually implicit, that specifies the overall system-level objectives with respect to access to various resources. The policy indicates both what is inadmissible, so that the intrusion attempts from within and without the network may be prevented, and what accesses must be allowed, so that the essential functionality of the system is not compromised. This policy is implemented through the configuration of myriad local devices and mechanisms, including router-based and hostbased firewalls and discretionary or mandatory OS-based access control mechanisms (e.g., SELinux). The complex interactions among these distributed and layered mechanisms can mask problems and lead to subtle errors. In this paper, we introduce a framework for performing a comprehensive security analysis of an automatically obtained snapshot of the access control policy implementation to check for compliance against a (potentially partial) specification of the global access policy. The framework has been implemented as the Access Policy Tool. APT helps to increase confidence in the efficacy of the intrusion prevention mechanisms in place by allowing for reasoning about the security policy at a high level of abstraction. We describe our analysis techniques and demonstrate their efficiency, scalability, and extensibility by using APT for a variety of test cases.