Reasoning about firewall policies through refinement and composition

Network and host-based access controls, for example, firewall systems, are important points of security-demarcation, operating as a front-line defence for networks and networked systems. A firewall policy is conventionally defined as a sequence of order-dependant rules, and when a network packet matches with two or more policy rules, the policy is anomalous. Policies for access-control mechanisms may consist of thousands of access-control rules, and correct management is complex and error-prone. Policies may need to be reconfigured for highly dynamic environments, as threats to, and access requirements for, resources behind a firewall do not usually remain static. Misconfiguration is common, and correct policy management is often reliant on the expert-knowledge of security administrators, and drawing from best practice. The thesis of this dissertation is that a firewall policy should be anomaly-free by construction, and as such, there is a need for a firewall policy language that allows for constructing, comparing, and composing anomaly-free policies. An algebra is proposed for constructing and reasoning about anomaly-free firewall policies. Based on the notion of refinement as safe replacement, the algebra provides operators for sequential composition, union and intersection of policies. The algebra allows a policy specifier to compose policies in such a way, that the result of the composition upholds the access requirements of each policy involved, and allows one to reason as to whether some policy is a safe (secure) replacement for another policy. This approach enables a common framework, whereby knowledge related to detailed access control configurations and standards-based firewall policies can be represented and reasoned about. This dissertation explores the effectiveness of firewall policy specification and analysis, that extends the conventional fivetuple rule to include stateful inspection, TCP flags, ICMP Types/Codes, and additional filter condition attributes. The effectiveness of the algebra is demonstrated by its application to anomaly detection, and standards compliance. The effectiveness of the approach in practice is evaluated through a mapping to/from iptables. The evaluation shows that the approach is practical for large policies. The effectiveness is also evaluated through a mapping to OpenStack network and host-based access controls, and the development of a policy management framework for the Android OS