Automatic Verification of Distributed and Layered Security Policy Implementations
Sankalp Singh, William H. Sanders, David M. Nicol, Mouna Seri · 2008
Abstract. 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.