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.
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
- The following copyright notice applies to all of the above items that appear in IEEE publications: "Personal use of this material is permitted. However, permission to reprint/publish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from IEEE."
- The following copyright notice applies to all of the above items that appear in ACM publications: "© ACM, effective the year of publication shown in the bibliographic information. This file is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in the journal or proceedings indicated in the bibliographic data for each item."
- The following copyright notice applies to all of the above items that appear in IFAC publications: "Document is being reproduced under permission of the Copyright Holder. Use or reproduction of the Document is for informational or personal use only."