ForestFirewalls: Getting Firewall Configuration Right in Critical Networks (Technical Report)

TL;DR

ForestFirewalls introduces an automated, high-level approach to configuring SCADA firewalls, reducing errors and enhancing security through abstraction, simplification, and validation in critical industrial networks.

Contribution

It presents a novel automation framework for SCADA firewall configuration that abstracts implementation details and ensures accuracy through automated validation.

Findings

Effective on a real SCADA network

Reduces manual configuration errors

Improves security policy compliance

Abstract

Firewall configuration is critical, yet often conducted manually with inevitable errors, leaving networks vulnerable to cyber attack [40]. The impact of misconfigured firewalls can be catastrophic in Supervisory Control and Data Acquisition (SCADA) networks. These networks control the distributed assets of industrial systems such as power generation and water distribution systems. Automation can make designing firewall configurations less tedious and their deployment more reliable. In this paper, we propose ForestFirewalls, a high-level approach to configuring SCADA firewalls. Our goals are three-fold. We aim to: first, decouple implementation details from security policy design by abstracting the former; second, simplify policy design; and third, provide automated checks, pre and post-deployment, to guarantee configuration accuracy. We achieve these goals by automating the implementation of a policy to a network and by auto-validating each stage of the configuration process. We test our approach on a real SCADA network to demonstrate its effectiveness.

Tables

Table 1. TABLE I: High-level comparison of Original vs Generated configurations (LoC - Lines of Code).

Type	Device-level
	Obsolete-ACL
	Generic permit-
	Intra-ACL
	interaction count
Original case study	2720	2	324	167
ForestFirewalls generated	714	0	0	0

Equations

$$p_A(s)=\{\begin{array}{ll}s,& \text{if }s\in A,//accept\\ \varphi ,& \text{if }s\in A^c,//deny.\end{array}$$

$$q_{m_1}^t\oslash q_{m_2}^t=\{\begin{array}{ll}{q}_{m_1}^t,& \text{if }s\prec m_1\\ q_{m_2}^t,& \text{if }s\prec m_2\text{ and}s\nprec m_1\\ deny,& \text{otherwise,}\end{array}$$

$$q_{m_1}^t\ominus q_{m_2}^t=\{\begin{array}{ll}{q}_{m_2}^t,& \text{if }s\prec m_2\\ q_{m_1}^t,& \text{if }s\prec m_1\text{ and}s\nprec m_2\\ deny,& \text{otherwise.}\end{array}$$

$$R(q_m^a,s_1)=\{\begin{array}{ll}0,& \text{if s1 fails for permit rule qma}\\ 1,& \text{if s1 succeeds for permit rule qma}.\end{array}$$

Full text

In this paper, we propose ForestFirewalls, a high-level approach to configuring SCADA firewalls. Our goals are three-fold. We aim to: first, decouple implementation details from security policy design by abstracting the former; second, simplify policy design; and third, provide automated checks, pre and post-deployment, to guarantee configuration accuracy. We achieve these goals by automating the implementation of a policy to a network and by auto-validating each stage of the configuration process. We test our approach on a real SCADA network to demonstrate its effectiveness.

I Introduction

“The single most important factor of your firewall’s security is how you configure it.”

Rubin and Greer [36]

Supervisory Control and Data Acquisition (SCADA) networks control the distributed assets of many industrial systems. Power generation and water distribution are just two examples that illustrate the critical nature of these networks. Others include factory automation, sewage management, airport control systems and chemical plant control.

SCADA networks are not like corporate IT networks [38]. IT networks can accept a degree of reliability orders of magnitude lower than the network controlling a power station. A fault in the latter will cost serious money, if not lives.

At the same time, SCADA networks often incorporate highly vulnerable devices. The Programmable Logic Controllers (PLCs) that control physical devices such as gas valves have highly constrained memory and computational power. Today, they often include network functionality such as a TCP/IP stack, but exclude sophisticated security functionality.

Despite their name, PLCs are not user programmable. The plant operator does not program them – that requires a programming board that pushes low-level code into an EPROM. The devices come pre-installed with code (and security holes). There are many PLCs in a power station, along with similar devices providing telemetry, and their upgrade is likely to occur only during a major overhaul of a plant, which might happen once in a decade (if that often).

These devices would be vulnerable if exposed to the Internet, and a plant operator cannot fix the vulnerabilities. Air gaps have been proposed as a solution to protect these devices, but an air gap is no longer a feasible approach for many reasons. In fact, Byres calls the idea a myth [8] to emphasise how poor a solution it is. The only viable protection today is a firewall, or series of firewalls [38, 9].

As Rubin and Greer note [36], it is, therefore, vital that these firewalls are configured correctly. Misconfiguration of SCADA firewalls can lead to security breaches, resulting in significant physical and environmental damage, financial loss or worse, the loss of human lives. A recent example is the hacking of a German steel mill by cyber attackers in 2014 that destroyed its blast furnace [4].

Unfortunately, firewall configuration, in practice, is a complicated and repetitive manual task. It involves training in proprietary and device-specific configuration languages, and long and complex device configurations. Lack of automation tools to assist this task has resulted in unoptimised, error-prone configurations [40, 41, 35].

The problem is exacerbated in SCADA plants where industrial engineers generally lack specialised networking and security knowledge. Such knowledge is often brought in through third party contractors. These IT security specialists are usually unfamiliar with the specific requirements of industrial engineering, and are on-site only for brief periods.

A cost-effective alternative to training plant engineers to become IT specialists is to build network operations tools that derive firewall configurations from high-level policy. Approaches using SDN have been proposed [37, 25], but they remain a distant reality for SCADA networks, where TCP is still a recent innovation. And power plants are insecure now [35]! SCADA networks need a solution that works now, using off-the-shelf technology. In this paper, we propose such a solution: ForestFirewalls.

Our system provides a mechanism for specification of security policy at a level a non-IT specialist could understand. What’s more, it forces good designs on its users through principles derived from the study of real SCADA firewall configurations [35] and International Society for Automation (ISA) best practices [2, 7, 38]. Most notably:

• $\bullet$

Single source of truth: more specifically, “Security managers need a single place to look for the corporate policies on who gets in and who doesn’t.” [20]. This general principle in computer science [5] applies doubly here.

• $\bullet$

Simplify: we don’t try to provide every possible security feature. At best, advanced features create confusion, and at worst, bad implementations can create security flaws.

• $\bullet$

Verify everything again and again: there is a clear danger in assuming any one piece of software functions correctly, from the firewall up to and including our own system. We check the configuration works at every level possible.

• $\bullet$

No implicit rules: implicit rules allow unexpected interactions, and undesirable consequences [35]. Desired flows must be explicitly allowed.

• $\bullet$

Rule order should not matter: it should be possible to add, or subtract a policy rule without considering its effect on every other rule. Surprisingly, none of the existing firewall configuration platforms [13, 14, 11, 23] achieved this. Operators using these tools, must provide correct rules and maintain correct rule order to avoid adverse interactions.

• $\bullet$

Separate structure from function [30]: decoupling

network topology (i.e., structure) from policy specification (i.e., function) facilitates high-level requirements based policies without network-centric minutiae like IP addresses.

• $\bullet$

Convenience: security and convenience are usually at odds, but wherever possible convenience should be provided. This is not a luxury – lack of convenience is one of the main reasons operators circumvent their own security.

Our system comprises a suite of tools to write policy, validate, test configurations, and create real configurations, and is designed to be user extensible.

We demonstrate it with a real example, derived from the actual (but anonymised) firewall configurations of a real SCADA plant. The example is intentionally small for clarity, but it shows a core set of functionality. The example includes several zones, two firewalls, and multiple real services much as they would run in the real network. Our testbed uses two different firewalls: one Cisco and one Linux-based, in order to show both the device independent nature of our policy language, and that heterogeneous network devices can be configured in the same network. The network offers multiple services: DNS, HTTP, … etc., and we use test traffic on the network to show correct function.

The proof of the pudding is that we can specify this network’s policy in only 80 Lines of Code (LoC), to generate the equivalent of 2720 device-level LoC found in a real SCADA case study [35]. This order of magnitude reduction, along with rigorous validation, shows the value of ForestFirewalls.

II Related work

A useful firewall configuration platform should allow policies to be specified abstractly, flexibly enough and in detail. There are many products and security management tools with varying levels of sophistication introduced by firewall vendors [13, 14, 11, 23], but policies still cannot be specified using high-level requirements.

For example, Cisco introduced security levels for quick and easy access between internal and external firewall interfaces [13], but these cannot specify detailed traffic restrictions. Hence, Access Control Lists (ACLs) are required to supplement these levels. Security levels may also not map to clear security policies. This hinders firewall auto-configuration, which needs clear policies [5] to permit traffic.

High-level security polices need to be based on security abstractions. The choice of the abstraction determines the level of decoupling between network topology and security policy. For one, Firmato [3] uses a role-based abstraction in its network grouping language that is independent of the firewalls and routers used in the network. But, the abstraction does not intuitively map policy to topology and requires minutiae like IP addresses to be input through the policy specification, to implement policy on a network instance.

For another, Cisco has introduced security policy management tools (e.g., VNMC for VSG policy management) to cater for complexities introduced in network virtualisation [15]. For scalability, the tools allow operating systems (i.e., VMs) to be allocated to zones and policies to be defined per zone. But, each VM still needs to be defined using minutiae like hostnames. ForestFirewalls decouples policy from topology using a more intuitive Zone-Conduit abstraction. The direct zone-to-network mapping allows policy to exclude IP addresses or hostnames as input.

The ability to debug configuration errors is also a highly desirable feature in a firewall configuration platform. But, this debugging should support abstract queries, free of network centric minutiae. Fang [29] and Lumeta [39] are interactive tools that facilitate firewall rule debugging, but the queries they support use network-centric minutiae as input.

Also desirable would be if the configuration platform supported more general-purpose abstract queries like service reachability and traffic isolation queries. Network programming languages supporting such queries have been proposed (e.g., NetKAT [1]), but they too, rely on minutiae as input; and are not specifically aimed at configuring firewalls.

Ability to create and correctly compose distributed policies is also necessary in a firewall configuration platform. Doing so, allows users from multiple policy sub-domains (e.g., SCADA engineers, Corporate admins) to manage their own policies. Policy Graph Abstraction (PGA) [32] provides such a framework for SDN networks, Cloud infrastructure and Network Functions Virtualisation (NFV) environments. It can automatically compose distributed policies into a coherent, conflict-free policy set. But, PGA leaves out how logs, alerts and alarms (i.e., reports) should be enabled in security-critical middle boxes like firewalls. These reports are critical to detect misconfigurations and network security setup failures. Our solution allows reports to be encapsulated with security policy via a framework designed by us.

Additionally, it is essential in SCADA networks to have assurance of expected configuration behaviour prior to deployment, since downtime must be minimised. SANE [10] proposes a central Domain Controller with trusted privileges to reduce end-host initiated attacks in corporate networks. It supports topology-independent high-level declarative policies but provides no pre-deployment guarantee of correct configuration behaviour. ForestFirewalls uses simple automated emulations to achieve this goal.

Most related works do not propose a high-level description that intuitively decouples policy from topology. In some cases [3], topology needs to be explicitly mapped to policy through the specification per host/subnet basis. There is also no automated pre- and post-deployment verification of policies. Moreover, none of the above works examine SCADA networks, with unique security requirements and best practices compared to Corporate networks.

The prior work also does not address a key practical issue- complexity. Firewall vendors have concentrated on new and impressive features to create systems with as much or more complexity as the base firewall configurations.

Our research tackles this problem head-on. Our solution, ForestFirewalls, uses security abstractions to drastically reduce firewall policy specification complexity. These abstractions decouple policy from topology intuitively, so firewall policies can be described using high-level requirements independent of vendor and network intricacies. Automated verification is also built-in to our system to mitigate misconfigurations. ForestFirewalls also provides a formalism to compose rule sets into a coherent, conflict-free policy set. These features collectively, make firewall configuration a commodity skill rather than a specialisation, so business managers and plant engineers alike can manage their SCADA firewalls.

III Requirements

Bush and Bellovin [5] identified the following core requirements of an automated security configuration system:

• $\bullet$

Clear policies: an automated system cannot resolve between a plausible and a correct policy [5]. For example, between allowing HTTP access to a publicly shared Web server or to a sensitive internal Web server. So the policy must be clearly understood by a Manager.

• $\bullet$

Database driven: all device configurations and their changes must be recorded in a single reference point [5], which allows fast response to security incidents as well as accurate security audits.

• $\bullet$

Meta-configurations: specifications or instructions

about real configurations need to be obtained by abstraction and parameterisation.

However, there are extra issues not described by [5]. For one, there is an assumption that the auto-configuration system generating the configurations is correct. But proof of correctness must stem from validation, as we describe next.

III-A Policy verification

SCADA operators need assurance that the device configurations generated produce the expected security outcome, both pre- and post-deployment. We use multiple verification stages (1) to provide this assurance.

Upper verification tier: it is important initially to check a specified firewall policy against available industry best practices [9, 38]. These automated compliancy tests are critical in SCADA networks where more restrictive practices are required to minimise their vulnerability to threats from less secure networks (e.g., the Internet). Best practice violations can be accurately identified by conducting equivalence and inclusion checks on the canonicalised policies. See VII.

Complex firewall policies also produce unintended consequences through rule overlaps [42, 27]. So it is additionally necessary to check policies from high-level through firewall-level for inconsistencies. We do so accurately, using a mathematical and logic based formal tool: Alloy [21].

Middle verification tier: the second stage helps debug configuration problems prior to deployment. Network emulation offers a cost effective method to test configurations before actual deployment [24]. The Netkit open source software package [31] provides such an emulation platform with virtual devices and interconnections via User Mode Linux (UML). Automated pathological traffic tests, together with Netkit emulations, can verify that the generated configurations produce the expected outcome prior to deployment.

Lower verification tier: the final stage guarantees that the real firewalls operate as intended, post deployment. The automated tests are extended from emulations to the real network, to generate live-traffic and reveal unexpected configuration behaviour in the real firewalls.

Automated verification can drastically reduce the number of firewall misconfigurations. It can be used to identify best-practice violations and adverse policy interactions, and prevent those from propagating to the physical firewalls. Most importantly, it provides users with a guarantee of the security outcome prior to implementation.

III-B Firewall reporting

A second issue not described by [5], but key to autoconfiguration, is the need to be able to constantly examine the status of security provided by the firewalls in a network. We discuss this briefly here to keep within the scope of this paper – see [33] for an extended discussion.

Firewall security status can be monitored using the diverse logs, alerts and alarms available. We refer to these together as firewall reports. These reports are critical in identifying firewall misconfigurations and detecting failures in the network security setup. But, the industry standards available for reporting and analysing firewall data are scant and vague. So, we developed a firewall reporting framework [33] considering the granularity and scope requirements of the various reporting use cases.

We learnt key lessons, in developing this reporting framework. For one, a firewall is a poor source of data in some reporting use cases (e.g., accounting) [33], although they are often used in this way. In those cases, it is better to report elsewhere in the network and release a firewall’s resources for its primary function: traffic filtering. Where firewall reporting must be enabled, it needs to be at the correct granularity. Employing an inferior granularity prevents collecting sufficient data to satisfy use-case requirements, using an overly-fine granularity simply wastes resources.

Additionally, security policy and reporting policy need to be encapsulated (i.e., coupled) together [33]. Decoupling the two can lead to bad decisions, for instance, it would allow adding security policies that are not verified.

III-C Decouple policy from network

A third issue not described by [5], but key to autoconfiguration, is the need to decouple policy from the network implementation.

In practice, network architects and business managers decide what type of services are allowed through firewalls. Network engineers then implement these policies. Intuitively, separation of the network intricacies from policy specification better suits these distinct phases. Conceptually this is analogous to the separation of architects and building contractors in construction. Contractors don’t usually decide what roof shape a building should have.

Network topology can change often in response to new business needs, upgrades and service demands. This may alter the devices and administratively assigned parameters such as IP addresses and hostnames in the network.

Comparatively, security policies are static. These policies commonly only involve dozens of distinct services [35], so policy complexity is relatively low to that of the network. This relative simplicity and invariant nature leads to decoupling policy from the network. The adage “Structure and function should be independent” [30] truly applies here.

Decoupling structure from function, has these advantages:

• $\bullet$

Policy is specifiable via high-level, vendor neutral111Vendor platform and device independent requirements. requirements: which assists management-level policy makers not fluent in network-centric details.

• $\bullet$

It centralises policy management and promotes reuse:

a single topology-independent organisation policy (i.e., source of truth) can be maintained across sites.

• $\bullet$

It streamlines network changes and upgrades: the policy can be quickly re-mapped to a new topology, retaining previous levels of protection.

• $\bullet$

It simplifies best-practice enforcement: best practice standards can be precisely specified in absence of proprietary details of specific networks.

Security abstractions are key to decoupling policy from the underlying network.

IV Security abstractions

A good high-level security abstraction captures the underlying network security concepts naturally and concisely. For one, in real networks, we might group systems with a similar set of traffic services enabled. For another, traffic restrictions between two systems may be enforced by a single or a series of firewalls. A good abstraction should decouple what is restricted between systems from how it is restricted.

The American National Standards Institute (ANSI)/ ISA introduce the Zone-Conduit abstraction to segment and isolate the sub-systems in a control system [2]. But, the Zone-Conduit model in its original specification is too flexible for automation. To increase its precision, we needed to add several extensions [35]. We describe our modified version here.

IV-A Our modifications to the ISA model

The Zone-Conduit model is a graph $G=(Z,C)$ where $Z$ is the set of zones, and $C\subset Z\times Z$ is the set of conduits.

A zone is a logical or physical grouping of an organisation’s systems with similar security requirements, based on criticality and consequence [2]. By grouping systems in this manner, a single zone-policy can be defined for all members of a zone. For example, 3 disjoint security zones can be defined to accommodate low, medium and high-risk systems, with each device assigned to its respective zone, based on their security level needed. A low-risk system can be accommodated within a medium or high security zone without compromising security, but not vice versa.

A conduit provides the secure communication path between two zones, enforcing the policy between them [2]. Security mitigation mechanisms (e.g., firewalls) are implemented within a conduit. A conduit could consist of multiple links and firewalls, but logically is a single connector. Conduits abstract how a policy is enforced, so we can focus on what needs to be enforced.

We conducted real SCADA firewall configuration case studies [35] and found that the ISA Zone-Conduit model in its original specification is too flexible for automation. For one, the ISA model allows alternate ways of defining zones and conduits to cater for business models. It loosely permits 1:n or n:1 mapping between conduits, firewalls and policy.

We refine the model through several extensions [35]. First, we enforce a 1:1 mapping between policies and conduits. Second, dedicated Firewall-Zones are used to capture firewall management policies. Third, Abstract-Zones are used to capture the distinct policy requirements of serial firewalls. Carrier-Zones are also used to abstract any carrier based transit outside of an administrative domain’s control.

The ISA standard also loosely allows sub-zones to be defined, enabling multiple policies within a zone. Doing so, implies that selected subsystems in a zone (e.g., a server) could have their own separate policies. Allowing exceptions would impart a false sense of security: these systems are only as secure as the zone itself, in the absence of firewalls enforcing a real separation. We tighten the specification further in our approach by strictly enforcing a single zone-policy.

A single zone-policy leads to every device within a zone having the same set of permissions to initiate, accept or block one or more services. Hence, a zone is the smallest unit of abstraction for which a policy can be applied to and we do so simply and unambiguously using inter-zone flows.

Once extended, the best practice produces a tight specification suitable for auto-configuration. We can now begin to formally define firewall security policies based on this refined Zone-Conduit model.

IV-B Policy on a single conduit

A conduit policy in the refined Zone-Conduit model can be constructed from an ordered set of rules $[p_{1},p_{2},...,p_{n}]$ that act on packet sequences to accept, deny, or in some cases, modify them. Particularly, a policy rule $p_{1}$ operates on ${\cal A}=\{atomic\ packet\ sequences\}$, where an atomic packet sequence is a complete packet sequence that cannot be decomposed into smaller subsequences (except themselves and the null sequence- $\phi$). Complete means that a decision on two concatenated complete subsequences is the same as that on the joint sequence, i.e., $p_{1}(s_{1}+s_{2})=p_{1}(s_{1})+p_{1}(s_{2})\text{,}\forall s_{1},s_{2}\in{\cal A}$, where $+$ is an associative concatenation operator. ${\cal A}$ is closed under $+$ and $\phi$ is the identity. So, ${\cal A}$ is a monoid and policy rules $p(\cdot)$ are monoid endomorphisms on ${\cal A}$ (i.e., mappings from ${\cal A}$ to itself that preserve the semigroup structure of the operator $+$ and identity $\phi$).

Typical policy rules accept/deny packets, i.e., for $A\in{\cal A}$

[TABLE]

This type of rule doesn’t allow modification or creation of packets. Real firewall rules can modify or create packets. For instance a firewall might

• $\bullet$

update certain header fields related to QoS; or

• $\bullet$

might defragment, or fragment packets; or

• $\bullet$

be integrated with Network Address Translation (NAT) or Virtual Private Network (VPN) functionality.

The scope for packet modification is huge, but within a firewall, many modifications don’t change fields that would affect further rules in subsequent firewalls, e.g., QoS or TTL changes. In order to have a tractable problem, we restrict the firewall rules to such modifications, and thus consider all rules to be in the form given in 1.

We also cannot construct a policy rule for any possible subset of ${\cal A}$, due to the limitations of technology used in a firewall. The subsets of ${\cal A}$ for which rules can be defined is actually a sigma algebra $\sigma({\cal A})$ [6].

The particular sigma algebra will be generated by the finest possible partition of ${\cal A}$ determined by the firewall technology used. So for a given firewall technology, ${\cal A}$ can be broken into sets $A_{i}\subset{\cal A}$ such that $A_{i}\cap A_{j}=\{\}$ and $\cup_{i}A_{i}={\cal A}$, and we can implement rules $p_{A_{i}}$, but cannot define any rule $p_{B}$ where $B$ is a strict subset of some $A_{i}$.

Firewall rules in practice however, are implemented by specifying a predicate and an action. A firewall enforces actions based on predicate matching, and firewall policies found in practice are built using multiple policy rules [35].

IV-C Positive, explicit policies

A firewall policy in practice, is made up of multiple predicate matching rules that can be combined using several strategies: first match, last match or all match. If we presume here the conservative security option: an implicit deny- all rule in place, then an accept rule $q^{a}_{m}$ (where $m$ is the predicate) defines accept packet set $A=\{s\in{\cal A}\mid s\prec m\}$, where $s\prec m$ denotes $s$ matches $m$. A single deny rule $q^{d}_{m}$ has no affect, i.e., $A=\{\}$.

When we combine two (ordered) rules $(q^{t}_{m_{1}},q^{t}_{m_{2}})$ where $t\in\{a,d\}$, we define operators based on the matching order:

first match

[TABLE] 2. 2.

last match

[TABLE]

Clearly the operations $\oslash$ and $\ominus$ are associative, e.g., $(q_{1}\oslash q_{2})\oslash q_{3}=q_{1}\oslash(q_{2}\oslash q_{3})$, but not commutative or equivalent.

This is a problem. We need a policy to hold the same semantics regardless of how the rules are ordered, in order to simplify policy specification.

So, we restrict ourselves to accept rules, conditional on an implicit deny-all rule. This restriction

• $\bullet$

is rich enough to represent all rules [34] and

• $\bullet$

the operators are then commutative and equivalent [34].

Equivalent results also hold if we only allow deny rules, but this option is less secure as it is easier to accidentally leave something out of a deny list than to include it.

Therefore, we adopt a security whitelisting model, i.e., we restrict inter-zone flows to express positive abilities222Refers to the ability to initiate or accept a traffic service. and deny all flows that are not explicitly allowed. Doing so, renders the rule order irrelevant in a policy. A policy now holds the same semantics, irrespective of how its rules are organised. Hence, policy makers need not consider the order when adding or removing policy rules. By being explicit, we also prevent services being accidentally enabled implicitly.

We can use the conduit-policy definition to also check for equivalence as well as inclusion of policies [34]. In VII we will demonstrate how doing enables evaluation of actual firewall policies against industry best practices for violations.

So far, we considered policy rules on a single conduit. We now generalise these policies to a network, or rather the simplified Zone-Conduit model of the network.

IV-D Network policy

For policy space $\Phi=\{p:{\cal A}\rightarrow{\cal A}\mid p\mbox{ is a monoid endomorphism}\}$, we can define a network policy as

Definition 1** (Network Policy).**

A network policy $\mathcal{P}=(G,P)$ means a Zone-Conduit graph $G(Z,C)$ with policy functions $p_{ij}\in\Phi$ for $(i,j)\in C$.

When comparing network policies, it is also useful to partition the policies on the networks (e.g., $p_{ij}$ in Definition 1) into equivalence classes [34]. We refer to these partitions as Semantic Partitions (SPs) as they have the same meaning.

IV-E Isolation of traffic

An important element in architecting a network’s security is the proper isolation of traffic between zones, i.e., it is necessary to guarantee the privacy and integrity of a host’s data while eliminating unwanted traffic (malicious or not) between hosts, that can hinder a network’s performance.

A common method of providing this guarantees is to construct modular policies using network slices [19]. A network slice is a piece of the network that can be programmed independently from the rest of the network. If we restrict traffic to a network slice, the behaviour of the entire security policy is precisely that of that slice alone. So, regardless of how complex a network’s policy may be, we need consider only the policy of the slice corresponding to traffic flow between two zones, to ensure proper traffic isolation between them.

In our revised Zone-Conduit model, a conduit provides this network-slice behaviour. A conduit policy does not modify packets intended for another, so to ensure traffic isolation between two zones, we simply need to consider the policy of the conduit connecting those zones. For example, in the policy below, traffic flow from Z1 to Z2 is strictly controlled by the policy of conduit (Z1,Z2).

Policy Company_policy { Z1 -> Z2 : https, dns; Z2 -> Z3 : http, ftp, dns;}

So, users from multiple policy subdomains (e.g., corporate admins, SCADA engineers) can simply manage the policies of the conduits that corresponds to their subdomain, and have guarantee of traffic isolation.

V System overview

We now describe our auto-configuration system design as depicted in 2, with the details outlined below:

High-level security policy: The topology-independent policy input file created using ForestFirewalls. See VI for details.

Compile to intermediate-level (IL) policy: Parses the high-level policy to an intermediate format for checking.

Network topology: The input network topology described in the XML-based graph file format GraphML [18]. The file contains information of all devices of the underlying network and their interconnections. The crucial aspects are the details of the topology near the firewalls.

Generate network-level, vendor-neutral policy: Down-compiles high-level policy to network-level, by coupling policy to the input network topology. See V-A.

Verify IL policy against best-practices, via Alloy: Formally checks an IL policy for SCADA best-practice violations and for correctness. Best-practice checks employ canonicalised policies while a mathematical and logic based tool, Alloy [21], finds anomalies within the policy. See V-B.

Verify network-level policy via Alloy: Formally checks network-level policy for correctness via Alloy [21]. See V-B.

Device templates: A vendor and device specific meta-configurations repository that currently supports UML IP-Tables, Cisco ASA5505 models, and is easily extensible.

Generate device-level configurations: The rendering of device-specific configurations for firewalls using the network-level policy and the device templates.

Verify via emulations: Device configurations are pushed to an emulated network for pre-deployment testing. Test scripts are auto-executed in this network, to generate pathological traffic and validate configurations. See V-C.

Real network: Device-specific configurations are pushed to hardware in a real network. At present this is conducted manually333Automation of pushing device configurations is more development than research., but we intend to automate it.

Verify via real traffic tests: Automated tests are created for the real-network, generating real-traffic, to verify post-deployment behaviour of firewall configurations. See V-C.

V-A Network-level policy generation

A high-level policy is implemented on a network by coupling the policy to the network topology instance. The resultant network-level ACL rules are vendor/device neutral. This generic format allows easy checking of rules for inconsistencies. The policy generation steps are outlined below.

V-A1 Zone-Conduit model construction

The system first builds a Zone-Firewall model, containing the disjoint zones and their firewall interconnections [35] using the network topology. Additional Firewall-Zones, Abstract-Zones and Carrier-Zones are added to the model as required.

Next, the network conduits are defined to create the Zone-Conduit model. The Zone-Conduit model of the input network may not always match that perceived by the policy creator. So, we must cross check the real model against that provided through the specification. If mismatched, an error is reported indicating incompatibility.

V-A2 Network coupling and rule translation

An implicit mapping between a zone and its host/subnet composition is created when defining the zones in the input network. This mapping readily translates the high-level policy to the underlying network. The source and destination zone of each high-level rule can be substituted with the corresponding IP address ranges from this mapping. The equivalent network ACL rules can be obtained from the cross product of these IP address ranges and the original rule operator and service description. We can represent rule translation through a mapping $t:\Phi\rightarrow\Gamma$, where $\Phi$ is the high-level policy space and $\Gamma$ is the network-level policy space.

Multicast rules may also be required for the correct operation of certain protocols. For instance, when OSPF is specified as a dynamic routing protocol by the user, multicast rules are required to enable neighbour relationships to correctly form within a single OSPF area. Similarly, stateful protocols (e.g., TCP) require return path rules in addition to the forward path rules for correct operation. ForestFirewalls handles these requirements automatically, generating and incorporating any supplementary rules as necessary.

V-A3 Path selection and conduit configuration

The system identifies possible Zone-Conduit communication paths for each high-level policy rule. Paths that are deemed impractical are eliminated. For instance, (i) traffic cannot transit a Firewall-Zone. Firewall-Zones only enable traffic flow to and from the firewall but cannot forward traffic, (ii) a traffic path cannot form loops around firewalls. If a path requires a traffic packet to traverse a particular firewall interface more than once, it is discarded, (iii) traffic originating from or terminating at a Firewall-Zone must have a valid external path through the network.

Our system configures all conduits, using valid paths. A conduit implements a default deny-all policy between its interconnecting zones. This strategy promotes defence in depth [2, 9], which prevents a single point of failure from triggering cascading security breaches across the network.

The system evaluates each conduit’s firewall-interface layout to determine how the Access Control List (ACL) rules should be applied on these interfaces (inbound or outbound).

Our high-level policy is easily adapted to incorporate new zone additions to a network. The updated policy is swiftly re-implemented on the network to protect the new zones.

V-B Formal policy verification

Policy-rule overlaps can cause unintended consequences. These overlaps can be redundancies or conflicts [27, 42]. Redundant rules can be removed without affecting the semantics of a policy. Such rules reflect configuration inefficiencies. A conflict occurs when a rule overlaps with preceding rules but specifies a different action, creating ambiguity. Correct ordering of rules is typically required to avoid rule conflicts.

Our system only supports positive permissions. So, we remove conflicts by design, rendering rule order irrelevant. Redundancies are still possible, so we need to check for these.

We find redundancies using a model checker: Alloy [21]. Formal model-checking is generally complex, so Alloy aims to find counter-examples to illustrate problems. Essentially it’s a refuter [21] not a prover. But, its ability to comprehensively analyse a model, even within finite bounds, makes it very useful [21]. For Alloy based verification, see VII.

A policy also needs to be checked for SCADA best practice compliance. Checking policies by exhaustive comparison would be highly inefficient. A more efficient approach would be to derive a unique, canonical, representation of each policy. Policy canonicalisation can be represented through a mapping $c:\Phi\rightarrow\Theta$, where $\Theta$ is the canonical space of policies. Inclusion and equivalence checks on the canonical policies, help identify any violations. For details, see VII.

V-C Automated testing

We use a network emulator – Netkit – for our pre-deploy-ment tests. The emulator is open source and enables virtual devices and interconnections using UML [31]. AutoNetkit is a tool designed to automate emulated network experimentation via Netkit [24]. We have extended AutoNetkit, with basic firewall capabilities, to generate our emulations.

When the emulated network is run, automated tests specific to the input policy create pathological traffic to verify expected firewall configuration behaviour. ForestFirewalls uses Expect – a UNIX scripting and testing utility – to generate these test-scripts. Expect enables automated interactions with programs that expose a text terminal interface [26]. Netkit automatically launches these scripts within its Virtual Machines (VMs), once the VMs are running. The scripts run sequentially, with independent outcomes.

Expect test scripts verify that the permits rules in a policy works correctly (i.e., positive vetting). A permit rule fails if its observed behaviour is different from that expected. We can use a result function $R$, to track what rules fail. For a permit rule $q^{a}_{m}$ with accept packet set $A=\{s\in{\cal A}\mid s\prec m\}$ and a test-packet sequence $s_{1}\in A$ the result function is

[TABLE]

A failed permit rule means its corresponding test packets are not delivered to the intended destination.

In addition to positive vetting, we need to check that all other services not explicitly enabled are blocked. This negative vetting is conducted using automated, exhaustive port-scans employing nmap and tshark.

The same test-suite can be used in the real network, post configuration deployment. The tests now generate live-traffic, verifying expected real-firewall behaviour.

VI Policy specification framework

A useful network policy specification framework should cater for management-level policy makers as well as competent programmers. Policy makers need to define high-level policies to meet business goals. Programmers may wish to extend the framework to add more features. A layered approach (3) supports both cases.

VI-A A layered approach

Policy definition high-level language: designed primarily for non-expert users to define services and security policies, it uses a library of services and security policies in conjunction with a simple language. The service library consists of Internet Assigned Numbers Authority (IANA) well-known services and the policy library contains common SCADA security policies, all easily extensible by a non-expert user. The language syntax and semantics are also intuitively simple for non-expert users. Informative warnings and errors are returned for fast debugging. See VI-B.

Class library layer: dedicated to expert Programmers, this layer features an Object Oriented Programming (OOP) based, well-defined object hierarchy that consists of rules for constructing protocols (e.g., TCP, UDP) and services. Detailed checking of object specific attributes (e.g., TCP/UDP port numbers are between 0-65535) are handled by their respective classes. A direct mapping between the grammar rules and the Classes makes the library easily extensible, but it is only intended that expert protocol engineers would extend this. Most operators would use the higher layer.

High-level language grammar: dedicated to the language designers, this layer consists of Backus-Naur Form (BNF) rules that control the language semantics. The grammar includes basic checking (e.g., argument length, null checks), but delegates detailed checking to the class library layer. The rules are static and can only be altered by the language designers (us). This preserves the original objectives of a high-level abstraction that is intended to change slowly.

Our layered policy-specification architecture leads to a vendor and device neutral policy-specification framework. The system suits naive users, but the framework is easily extensible to cater for new network applications and protocols.

VI-B ForestFirewalls high-level language

Simply put, the ForestFirewalls specification language allows a user to instantiate a high-level firewall policy. Below is the definition (a complete example can be found in VIII).

ForestFirewalls’ parser is currently implemented in Python and Ply (a lex and yacc implementation for Python). It translates a ForestFirewalls specification (i.e., a .policyml file) into its Intermediate Language (IL) representation using object definitions from the underlying class library, also implemented in Python.

VI-B1 Service and Service-group description

A service is defined using the syntax

service <service-name> { protocol=<protocol-base>; <protocol-attributes-list>; }

For example, a custom implementation of HTTP, based on the above service description format is given by

service custom_http {protocol=tcp; tcp.dest_port=8080; comment=‘‘Internal Web’’;}

All unspecified attribute values have defaults assigned (e.g., here tcp.source_port=0-65535). Service specific comments are enabled via the omment field. This type of ode documentation allows commentary in the lower tiers to be auto-generated. The aim is to help document network and device level firewall rules to avoid the common problem that rules cannot be deleted because no one remembers why they exist.

ForestFirewalls prohibits the description of generic services such as all-TCP or all-IP for several reasons. For one, SCADA case studies [35] reveal that users exploit generic rules where possible for convenience, such as allowing all-IP traffic just to enable EIGRP traffic. However, far more services than necessary are thus admitted through firewalls.

Secondly, such inherently broad services don’t contribute towards forming well-defined security policies. They cloud the ability to accurately see the type of cyber threats a network is being protected from.

A service can be formally represented by tuple $(Pr,PrA,$ $PrV)$ where $Pr\in\Lambda;\Lambda=\{all\ IP\ protocol\ numbers\}$ and $PrA\subset\Upsilon,PrV\subset\Pi;$ $\Upsilon=\{tcp/udp/icmp\ etc.\ protocol\ attributes\}$ and $\Pi=\{protocol\ attribute\ values\}$.

We use a service-group to bundle services and other service-groups (i.e., nesting is allowed)

service_group <group-name>{ <service-or-group-list>}

Service-groups provide a level of indirection, so application protocols used to achieve network functionality (e.g., Web services) can change without needing policy alterations.

A service-group is really a set $SG=\{(Pr_{i},PrA_{i},PrV_{i})$ $|Pr_{i}\in\Lambda,PrA_{i}\subset\Upsilon\,PrV_{i}\subset\Pi\}$. The specification supports set operations: union (,), intersection (^) and difference (), so, new service groups can be constructed by applying these operators on existing service groups.

The following snippet defines a service-group containing various example Web services:

service_group Web { http, https, dns }

VI-B2 Zone-group description

A zone-group bundles a set of zones or other zone-groups and is defined using the syntax

zone_group <group-name> {<zone-or-group-list>}

A zone-group is a as a set of disjoint zones $ZG\subset\Omega$ where $\Omega=\{all\ zones\}$. Multiple zone-group declarations are checked for duplicates to minimise code redundancy.

The snippet below describes an example zone-group, depicting hree_zones : a se of zones in a network which is made up of 3 disjoint zones.

zone_group three_zones {corp, scada, dmz}

We also allow similar syntax and set operators for defining groups of TCP/UDP ports or ICMP types.

VI-B3 Policy-rule description

A high-level policy rule can be defined as below with an operator to direct the inter-zone flow explicitly. The end-zones defined by zone-or-group-name have traffic flow of type service-or-group-name enabled.

policy_rule <rule-name> { <first-zone-or-group-name> operator <second-zone-or-group-name> : <service-or-group-name> }

where operator == ‘->’ or ‘<->’

For example, the following policy rule models the capabilities of a orp_ \verb orate_zone with regards to \verb Web traffic {\small \begin{verbatim} policy_rule corp_web_rule { orp_zone -¿ DMZ : Web

The above description can be represented as a policy rule $q^{a}_{m}$ with accept packet set $A=\{s\in{\cal A}\mid s\prec m\}$ where predicate $m=(s.hdr.source\_address\ in\ Corp\_zone\ \wedge\ s.hdr.dest\_$ $address\ in\ DMZ\ \wedge\ s.hdr.service==Web)$.

VI-B4 Policy description

A rule_group object is used to hold one or more security policy rules and can be defined using the following format

rule_group security_policy { <rule1>, <rule2>, ... }

A security policy is a set of rules $RS=\{q^{a}_{m_{i}};m_{i}-predicate\}$, each rule has an accept packet set $A=\{s\in{\cal A}\mid s\prec m_{i}\}$. Similarly, we can specify firewall reporting policy using a reporting _rule object [34]

reporting_rule reporting_policy { <attributes-list>}

A global policy object then encapsulates security policy with reporting policy [34]

policy <policy-name> { security_policy; reporting_policy; }

VI-B5 ForestFirewalls library file imports

In large industrial control plants, multiple policy sub-domains exist (e.g., corporate admins, SCADA engineers, network engineers, different departments) that set their own policies to be applied to the network components they own or manage. Namespace importation facilitates such distributed policy management and promotes reuse of policy. For instance, we can imagine the ISA creating a best practice ruleset for SCADA as a baseline for new installations.

Non-expert programmers may, however, be unfamiliar with the use of a complex namespace library with many features. We developed a namespace hierarchy that is simple, yet provides rich features for managing and reusing namespaces. ForestFirewalls’ namespace hierarchy consists of generic library definitions for all users with additional support for custom namespace creation. This allows to compose distributed policies into a coherent policy set, free of inconsistencies.

VII Verification

Once a high-level policy is parsed by ForestFirewalls, it is stored in IL code and needs to be checked for SCADA best-practice violations as well as for correctness.

VII-A Best-practice compliance

Two policies with different rule sets, can have the same underlying semantics (i.e., they allow the same set of services between zones). 4(a) and 4(b) illustrate the idea based on TCP port filtering of single packets. Each rectangle indicates the allowed packets of a single rule. Combined, the rules cover the same set of allowed packets. Comparing policies exhaustively is highly inefficient. So, we derive a unique, canonical, representation of each policy to efficiently compare them. In our canonicalisation mapping $c:\Phi\rightarrow\Theta$, where $\Theta$ is the canonical space of policies, all equivalent policies of $\Phi$ map to a singleton. For $p^{X},p^{Y}\in\Phi$, we note the following (the proof follows the definition)

Lemma 2**.**

Policies $p^{X}\equiv p^{Y}$ iff $c(p^{X})=c(p^{Y})$.

Thus, comparison is eased by the canonicalisation of policies. We illustrate the idea using TCP policy rules (4) and dissect the polygon formed in our example policy into horizontal partitions (Figure 4(c)), using a Rectilinear-Polygon to Rectangle conversion algorithm [17]. Each partition is chosen to provably guarantee its uniqueness. Canonical policy elements are derived by translating each partition back to a rule and ordering the resulting rule-set uniquely in increasing IP protocol number and source and destination port numbers. We find a unique partition quickly rather than a guaranteed minimal partition. The result is a deterministic, ordered set of non-overlapping rules. So, intra-policy verification can be performed by comparing canonical policy components. For instance Is $c(p^{Z1\to Z2})=c(p^{SCADA\to Corp})$ ? Another useful notation, linked to the goal of policy comparison, is that policy $P^{A}$ includes policy $P^{B}$. Particularly in SCADA networks, the notation helps evaluate whether the policies are compliant with industry-recommended practices in [38, 9]. These guidelines specify potentially dangerous services (e.g., HTTP) that should be prohibited from traversing inbound and/or outbound from the (protected) SCADA-Zone. A violation here, means increasing the vulnerability of a SCADA-Zone to cyber attack. Unlike corporate networks, this increased exposure could potentially render SCADA systems unavailable, and cause significant financial loss or at worse loss of human lives. We indicate that a policy complies with another if it is more restrictive and define the following

Definition 3** (Inclusion).**

A policy $p^{X}$ is included in $p^{Y}$ on ${\cal A}$ iff $p^{X}(s)\in\{p^{Y}(s),\phi\}$, i.e., $X$ either has the same effect as $Y$ on $s$, or denies $s$, for all $s\in{\cal A}$. We denote inclusion by $p^{X}\subset p^{Y}$.

So, we can now evaluate whether an input policy adheres to the SCADA best practice policy using an inclusion check Is $p^{Input}\subset p^{BestPractice}$ ?

VII-B Policy correctness

A partial snippet of the Alloy language specification (i.e., .als) file auto-generated by ForestFirewalls for the IL policy is shown in Figure 8 in the Appendix. It depicts a formal model with 3 signatures: Service, PolicyRule and SecurityPolicy. In our initial model, a Service has the basic members: ip_protocol, source_port, dest_port and icmp_type. Of these members, only ip_protocol is mandatory. A PolicyRule has 4 members: one1 and \verb one2 to capture the zone names, an peratr and a single ervice element. %The \verb operator i a set of integers containing {1} (representing a uni-directional permit: ->) or {1, 2} (representing a bi-directional permit: <->). The bi-directional permit is deconstructed as -> {1} and <- {2} for simplicity, but the latter operator is omitted in the high-level The global constraints are partially shown (lines 17–27 in Figure 8), requiring the universal set (Univ) of PolicyRule to comprise entirely of rules in the policy. Univ of Service must also comprise of PolicyRule services. Predicates can determine if two given rules or services overlap (not shown). Service overlaps are found by computing their intersection and testing if the result has members. String type members (e.g., zone1, zone2) can be directly compared. PolicyRule overlaps are checked similarly. A ‘no_rule_overlaps’ assertion (also not shown) is used to locate distinct rules with overlapping criteria. If found, a counter-example is returned, indicating potential inconsistencies in the high-level policy. Counter-examples can be inspected through Alloy’s GUI to find the underlying cause(s). Currently, Alloy is itself run manually and output counter-examples help debug data. We do not auto-correct rules as this requires human discretion. When overlaps are absent in the high-level policy, there should also be none in network-level policy, in theory. But we cannot simply ‘trust’ our system to always correctly generate network-level policy. So, we re-check the generated policy for overlaps and verify the fact. The Alloy export generated for network policy verification is similar to the high-level export. The key exception is the source and destination zone names are now replaced with IP address ranges in an ACLRule. Additionally, the Service signature also has members depicting protocol state. We also define an assertion here to check for ACLRule overlaps.

VIII A concrete example

We show here a concrete example, illustrating our methodology and the prototype system. The example is based on an actual SCADA case study [35] with the multi-firewall network configuration shown in 5. Due to security concerns and non-disclosure agreements, a modified version of the real network is presented for discussion. Steps have been taken to keep the core security strategies intact, but details such as IP addresses are anonymised.

R1 is a Cisco ASA 5505 firewall and R2 and GW are Linux IPtables firewalls. 5 shows these best already. The subnet summary is below. The Corporate network (Corp): Provides access to business applications and the Internet. Demilitarised Zone (DMZ): Responsible for enabling connectivity between R1 and R2. The distinct vendor firewalls provide defence in depth [9] by having different modes of failure and firewall-software redundancy. The SCADA network (SCADA): Responsible for providing networked access to plant equipment. Corp and SCADA could accommodate 2,046 and 65,534 hosts respectively. Corp hosts management workstations, a HTTP server, a HTTPS server, a FTP server, an Email server, a syslog server and a DNS server. SCADA has Oracle database servers, management workstations and a HTTPS server.

VIII-A Policy goals

We consider a simple policy which nonetheless covers many of the aspects that occur in more complex, real-life SCADA policies [35]. Its premise is that internal corporate users are trusted, but are restricted to use safe protocols when accessing SCADA. External users are allowed access only to content that is explicitly made public. The policy has these goals:

• $\bullet$

orp hosts can access the \verb Oracle servers and the HTTPS server in \verb|SADA—. They can also access all HTTP, HTTPS, DNS resources on the Internet.

• $\bullet$

CADA hosts can access Web, Email and DN servers on orp . Additionally, they can perform file transfer using FTP and HTTP with respective \verb orp servers.

• $\bullet$

Corp’s HTTP, FTP, Email servers are Internet accessible.

• $\bullet$

R1, R2 can be managed from orp using HTTPS and SSH. R2 can be managed from \verb SADA using SSH. R1 can also be managed from R2 using SSH.

• $\bullet$

A Syslog server located in Corp stores firewall logs.

• $\bullet$

OSPF is enabled across the entire site.

• $\bullet$

Firewall reporting is enabled for policy verification.

VIII-B Implementation

A partial snippet of the ForestFirewalls high-level description implementing the above policy goals is depicted in Figure 10 in the Appendix. We start by importing the required library files containing the predefined lists of IANA well known services. Next, the Zone-Conduit security model is supplied as a GraphML file. The zones within this model can be grouped as necessary (lines 9-15), to simplify the specification process and increase readability. We also define custom port-groups, services and service-groups as needed. A passive mode FTP data service is enabled through the firewalls (lines 18–20) as it’s the best-practice approach[38, 9]. Ping is also defined for connectivity tests. High-level rules are defined to match the policy goals listed earlier. Finally a policy object is used to hold all the rules (line 48).

VIII-C Procedure and Results

Once the high-level policy is parsed, the corresponding Alloy export is generated by ForestFirewalls for verification. Checking the ‘no_rule_overlaps’ assertion (not shown) returns a counter-example, indicating potential inconsistencies in the specification. Upon inspection of the counter-example details in Alloy (6), we see that rules enabling HTTP services (ip_protocol=6, dest_port=80) between zones Z3 and Z1, initiate the overlap. The root cause is the web and file_transfer service-groups in the high-level policy (lines 22 and 25 in Figure 10), both containing HTTP. Once this is rectified (remove HTTP from file_transfer), no further counter-examples are found by Alloy.