Automatic verification of security policy implementations

Networked systems are ubiquitous in our modern society. They are found in settings that vary from mundane enterprise IT systems to critical infrastructure systems. The security of networked systems is important given their widespread use. In particular, the emerging scenarios and the likely trends for the future of critical networked systems make the security of those systems a paramount concern, especially in the area of controlling access to the critical elements of the system over communication networks; successful cyber-attacks on such systems, in a worst-case scenario, could result in loss of life, or in massive financial losses through loss of data, actual physical destruction, misuse, or theft. Access control is a cornerstone of network security. In a modern networked system, access control is implemented through a variety of devices and mechanisms that include, but are not limited to, router-based dedicated firewalls; host-based firewalls, which could be based in software or hardware; operating-system-based mechanisms, such as the mandatory access control in the National Security Agency's (NSA's) SELinux; and middleware-based mechanisms, such as the Java Security Manager. Such devices and mechanisms collectively implement a networked system's global policy (which is usually implicit), which specifies the overall system-level objectives with respect to resource access. However, it has been shown in empirical studies that misconfiguration of access control enforcement points is common. The problem of identifying those misconfigurations is compounded when several such mechanisms are present, as the complex interactions among those distributed and layered mechanisms can mask problems and lead to subtle errors. In this dissertation, we propose a framework for performing comprehensive security analysis of an automatically obtained snapshot of an access control policy implementation (e.g., firewall rule-sets) to check for compliance against a (potentially partial) specification of the global access policy. We identify and classify possible errors that can be found in global policy implementations, including both policy violations and internal inconsistencies. We provide detailed formalisms that can be used to efficiently model the topology of the networked system being analyzed and the rule-sets from multiple types and makes of firewalls that may be present on the network. The formalisms are XML-based, with sound mathematical underpinnings. We present an XML-based global policy specification language, with algorithms that ensure internal consistency of specifications written in that language and resolve any conflicts. We show that our specification language is at least as expressive as linear temporal logic. We describe an efficient algorithm for exhaustive analysis to identify all the inconsistencies and policy violations. The analysis algorithm utilizes specialized data structures, that we call multilayered rule-graphs, to dramatically improve performance. We provide additional mechanisms for identifying the root causes of any problems discovered. We further enhance the scalability of our analysis by presenting an algorithm for statistical analysis of the networked system; the algorithm uses importance sampling, and produces a sample set of violations and a quantitative estimate of the remainder. To facilitate the analysis, our framework includes techniques that automatically infer the network topology for the system being analyzed based simply on the firewall rule-sets implemented. The framework has been implemented with a sophisticated graphical front-end as the Network Access Policy Tool (NetAPT). We demonstrate the efficiency, scalability, and extensibility of our techniques through analytic evaluation and empirical evidence based on real-world testing. We also present an algorithm for automatically generating a benchmark suite for testing NetAPT; the algorithm learns the defining characteristics of our real-world data sets and generates random networks and firewall rule-sets that are representative of the real-world ones