Jason Crampton
email: jason.crampton@rhul.ac.uk

James Sellwood
email: james.sellwood.2010@live.rhul.ac.uk

Inter-ReBAC: Inter-operation of Relationship-based Access Control Model Instances

Keywords: access control, path condition, relationship, principal matching, policy graph, principal activation, authorization, secure inter-operation

Relationship-based access control (ReBAC) models define authorization policies and make authorization decisions on the basis of relationships between the entities in a system. We present a framework through which multiple ReBAC model instances can interoperate so that requests initiated in one system may target resources in a second system. Further, our framework is able to support requests passing through a chain of inter-connected systems, thus enabling many systems to be connected together or a single large system to be decomposed into numerous component subsystems. Whilst the underlying principles of this framework can be applied to any ReBAC model, we introduce its formal application to our RPPM model [3], the first, and most actively developing, general computing ReBAC model.

Introduction

Access control is a fundamental security service, employed within a system to manage the interaction between (user) processes and (system-protected) resources. Historically, access control in general-purpose computing systems has used discretionary and role-based access control (RBAC) models. Recent work on relationship-based access control (ReBAC), inspired originally by social networks [1, 2, 6], has shown that alternatives are viable for both specialist and general computing applications [4, 5, 8]. In ReBAC, the specification and evaluation of authorization policies is based on the relationships which exist between entities of a system. The use of paths of relationships has several advantages over roles, not least because they can naturally reflect the more complex, contextspecific nature of human interaction which otherwise requires the use of many, highly parameterized, roles [3].

Whilst the consideration of paths of relationships is key to request evaluation in any ReBAC model, different models support varying capabilities and constructs for representing and processing these relationships. However, the relationships between entities in the modelled system are, intuitively, always represented as an edge-labelled graph. Such system graphs indicate the scope of a model instance; the system's entities (vertices in the graph), relationships (labelled edges), and policies are bounded by the graph and the system's authorization requests are evaluated within it. Whilst a system is modelled by a single ReBAC model instance (and therefore by a single graph), there are several motivating situations in which multiple model instances may need to interact.

Firstly, systems are frequently connected together in order to support a wider range of services. In such cases, a subject in one system may request to perform an action on an object in a remote system. Currently such requests cannot be supported in ReBAC models unless a single "super-graph"1 model captures every entity and relationship within the two, and all intermediary, systems. This requires global policies, outside of the "authority" of any one component system, putting at risk the autonomy of all. The inter-connection of discrete autonomous subgraphs is, therefore, desirable. Secondly, ReBAC models containing very large system graphs (stand-alone, or super-graph as just discussed) will be impacted by the fact that request evaluation in such models has a time complexity linked to the number of nodes in the graph, whether they are relevant to the request being evaluated or not. It is, therefore, desirable to decompose such very large system graphs into smaller discrete autonomous subgraphs. Whilst request evaluation complexity in each of these subgraphs will still be linked to the number of nodes, the practical complexity is expected to be greatly reduced as many requests will only involve a subset of subgraphs (assuming appropriate routing is available).

We, therefore, develop a framework by which two ReBAC system graphs may be connected and requests initiated in one may be authorized in the other. We introduce a formal application of this framework in RPPM, as we believe RPPM is naturally suited to this task. It supports the modelling of general computing environments, to which inter-operation is highly relevant. Further, its two step request evaluation process and use of security principals provide a natural "break point" at which a request may be transferred from one system to another (particularly when employing graph-based policies). RPPM provides a convenient basis for combining paths from multiple graphs without searching end-to-end across the, potentially numerous, inter-connected system graphs.

Due to space limitations we do not provide a review of the operation of stand-alone RPPM instances; this background can be found in [3, 4]. Section 2 introduces the Inter-RPPM framework as a specific example of our ReBAC interoperation approach. Section 3 describes its request evaluation process. In Section 4 we discuss related work and in Section 5 we draw conclusions. The Appendix contains pseudocode for three algorithms required to support Section 3.

Inter-RPPM

The goal of our inter-operation framework is to connect distinct and autonomous system graphs in such a way that we are not required to define and evaluate relationship paths traversing a single super-graph. We, therefore, introduce an inter-operation framework which maintains the autonomy of individual system graphs by preserving their individual request evaluation scopes, system models and policies. In order to provide connectivity between system graphs, a construct external to the system graphs is required. We, therefore, introduce the concept of a bridged system group and employ bridging relationships2 , called bridges, between hub entities within distinct component system graphs. A request to access a remote resource will need to be evaluated by a sequence of RPPM systems. Bridges provide the link through which we propagate information about the outcome of each system's "local" request evaluation to the next system in the sequence; where it subsequently informs another local evaluation.

We employ a hierarchical dot notation to label elements: that is G.v and G ′ .v represent different nodes (with the same label v) when G and G ′ are distinct system graphs. [START_REF] Crampton | Path conditions and principal matching: a new approach to access control[END_REF] When all of the elements of a tuple, such as (v, v ′ , r), belong to the same system graph G, we will write G.(v, v ′ , r) to simplify notation.

Definition 1. Let G = {G 1 = (V 1 , E 1 ), . . . , G n = (V n , E n )} be a set of system graphs. A bridge is an edge of the form (G i .v, G j .v, bridge-to) such that G i = G j . A bridged system group is a pair (G, β), where β is a set of bridges.
Informally, a bridged system group comprises two or more RPPM model instances whose system graphs are connected by one or more bridges. Each bridge connects two hub entities; one each from two distinct component system graphs. We illustrate this framework with a simple example which we construct from two, initially disconnected, model instances, identified by their system graphs 1a.

G 1 = (V 1 , E 1 ) and G 2 = (V 2 , E 2 ), shown schematically in Figure
In Figure 1b we illustrate the inter-connection of G 1 and G 2 through the bridge (G 1 .h, G 2 .h ′ , bridge-to) and develop the example further in Figure 1c to incorporate three system graphs inter-connected via six bridges. [START_REF] Crampton | Relationships, paths and principal matching: a new approach to access control[END_REF] Bridges are

directed -(G 1 .h ′ , G 3 .h ′ , bridge-to) connects G 1 .h ′ to G 3 .h ′ ,
but not vice versa -and are represented by an arrow. However, there may also exist a bridge (G 3 .h ′ , G 1 .h ′ , bridge-to) in which case we will use a double-headed arrow to represent the pair of bridges between G 1 .h ′ and G 3 .h ′ .

Any bridged system group defines inter-system paths, obtained by traversing the bridges. A system graph sequence defines the sequence of system graphs along

G 1 G 2 (a) Disconnected system graphs G 1 G 1 .h bridge-to G 2 .h ′ G 2 (b) Bridged system group (1,2) G 1 G 1 .s G 1 .h bridge-to G 2 .h ′ G 1 .h ′ bridge-to G 3 .h ′ G 2 G 2 .h bridge-to 3 .h bridge-to G 3 G 3 .v (c) Bridged system group (1,2,3)
Fig. 1: Bridged system group examples such a path, where no system graph may be repeated and the directionality of the bridging relationships constrain the sequence. System graph sequences are a key component of the request evaluation process as they identify a path from the system originating a request to the system graph containing the target object. Multiple such paths may exist; we require that the access control policy decision point (PDP) within a system be able to determine the single, least cost path.

To achieve this we require that an extra-model administrator assign costs to bridges, and that hub entities maintain and exchange system path information using a modified path-vector routing protocol. Each hub communicates with adjacent hubs to which it directs a bridging relationship, retrieving the cost of their total (least) cost path to every other hub, and therefore every other system graph, in the bridged system group (where an infinite cost indicates an unreachable hub). [START_REF] Crampton | ARPPM: administration in the RPPM model[END_REF] Upon receiving these path costs the hub adds to each the cost of the bridge connecting it to that neighbour; it will then update its local system path table to reflect the least cost path (if it didn't already know it) to every remote hub, along with which adjacent hub each least cost path passes via. A system's PDP can collate this information from each of its local hub entities in order to determine the single, least cost path to a target system graph, or to determine that no such path exists. Henceforth, when identifying a system graph sequence between two system graphs we assume the least cost such sequence.

Request Evaluation in Inter-RPPM

The basic RPPM model evaluates local requests within a stand-alone system graph using two steps: compute principals (where principal-matching rules are evaluated to determine whether security principals match to the request) and compute authorizations (where authorization rules are evaluated to determine if the matched security principals are authorized to perform the requested action).

Within Inter-RPPM, remote requests are made by a subject G.s to perform a remote action G ′ .a (where G = G ′ ) on a remote object G ′ .v. To support these remote actions we introduce an originating remote request (ORR) and an incoming remote request (IRR). [START_REF] Fong | Relationship-based access control: protection model and policy language[END_REF] The ORR represents the remote request as it is specified within the originating system graph. The IRR contains additional data which enable subsequent system graphs to contribute to the evaluation. When processing remote requests, every traversed system graphs' PDP employs the compute principals step (whether evaluating an ORR or IRR), but only the target system graph's PDP computes authorizations. Essentially, non-originating system graphs re-compute the set of matched principals based on the set computed by the preceding system graph and identified in the IRR.

A policy graph is used during the compute principals step to order the evaluation of principal-matching rules and to enable principals to be "activated" when specific other principals are matched to a request. Definition 2. Given a system graph G = (V, E) and a set of principals P , a policy graph G ρ is a directed acyclic graph with a unique root (of in-degree 0) such that each vertex is a principal-matching rule (φ, ψ, p). The set of principals includes a special principal called the null principal and the principal-matching rule for the root is defined to be (all, none, null).

The edges of the policy graph determine which rules trigger other rules. The concept of the principal-matching rule's target is extended to support rules in which the targets (positive, φ, and negative, ψ) may identify sets of principals which must exist (or not) in the current set of matched principals or, as previously, paths of relationships which must exist (or not) in the system graph. More formally, we evaluate a policy graph with respect to a request, in order to compute a set of matched principals, as per Algorithm 1 (see Appendix). [START_REF] Gong | Computational issues in secure interoperation[END_REF] A remote request is initiated in the originating system graph as an originating remote request (ORR), which is evaluated as per Algorithm 2 (see Appendix). [START_REF] Rizvi | Relationship-based access control for an open-source medical records system[END_REF] Definition 3. Given two distinct system graphs G = (V, E) and G ′ = (V ′ , E ′ ) in a bridged system group (G, β), an originating remote request takes the form

G.q = (G.s, G ′ .v, G ′ .a), 9 where G.s ∈ V , G ′ .v ∈ V ′ and G ′ .a ∈ G ′ .A.
When processing the ORR, the originating system's PDP must take into account that the target object is located in a distinct system graph from the subject. Therefore, the ORR is processed by performing compute principals between the subject and the hub entity which links the originating system graph to the next graph in the system graph sequence (lines 1, 3 and 4). [START_REF] Shehab | SERAT: secure role mapping technique for decentralized secure interoperability[END_REF] Note that line 4 passes an empty set to the EvaluatePolicyGraph algorithm (defined in Algorithm 1) as no principals have yet been matched to this remote request. The result of processing the policy graph is a set of matched principals for traversing the originating system graph. This is then passed, along with the details of the request, across the bridging relationship to the next system in the system graph sequence (lines 5 and 6). 11 In non-originating system graphs, the remote request takes the form of an incoming remote request (IRR), evaluated as per Algorithm 3 (see Appendix); its processing differs in intermediate and target system graphs. Within an IRR, the subject component of the ORR is replaced with a tuple identifying the originating subject, the hub entity through which the request was received by the current system and the set of matching principals which resulted from the preceding system's processing of the request. Definition 4. Given a bridged system group (G, β) and a system graph sequence (G 1 , . . . , G i-1 , G i , . . . , G ℓ ), an incoming remote request processed by system graph

G i = (V i , E i ) takes the form G i .q = ((G 1 .s, G i .h, G i-1 . ρ ), G ℓ .v, G ℓ .a),
where G i .h ∈ V i is the hub through which the request entered G i and G i-1 . ρ is the set of matched principals computed by the preceding system graph.

When processing an IRR in an intermediate system graph, the system's PDP must take into account that neither the subject nor target object are located in the current system graph. Therefore, the IRR is processed by performing compute principals between two hub entities: the hub entity G i .h through which the request entered the system and the hub entity which links the intermediate system graph to the next graph in the system graph sequence (lines 4 and 5). The set of matched principals from the preceding system graphs is input into the graph policy evaluation (line 5) and may result in additional principals being activated (and added to it), as discussed in Section 2. As with processing an ORR, the cumulative set of matched principals that results is then passed, along with the details of the request, across the bridging relationship to the next system in the system graph sequence (lines 6 and 7). This process continues until it reaches the target system.

When processing an IRR in the target system graph, the policy graph evaluation is performed between the hub entity through which the request entered the system and the object of the request, note G i = G ℓ (line 10). Once again this makes use of the preceding system graph's set of matched principals. However, once a local set of matched principals is determined the compute authorizations step is performed. This allows a set of authorization decisions to be determined (line 11). A definitive decision is then determined, with RPPM's default decision process and conflict resolution process employed as with local requests (line 12).

Related Work

Whilst our work in respect of ReBAC inter-operation is novel, the inter-operation of other access control model instances has been considered in previous literature.

In particular, research into the use of RBAC in multi-domain scenarios has led to several approaches to inter-operation based principally upon role mapping.

Shehab et al. define a distributed secure interoperability protocol in which users are assigned roles in remote domains based upon cross domain access agreements [10]. The order in which roles are acquired within each domain they access is referred to as the user's access path. These paths are checked to ensure the principles of autonomy and security [7] are both satisfied. In Inter-RPPM remote requests, by construction, are unable to target local resources and the outcome of local request evaluation is unchanged by the additions discussed in this paper. Therefore, both of these principles are satisfied trivially.

Shafiq et al. take this further by introducing a policy composition framework that integrates the RBAC policies of initially distinct domains [9]. They, additionally, implement a conflict resolution technique to deal with conflicts which may arise from the differences in how each domain models or references its access control policies. Within Inter-RPPM we have intentionally avoided integrating the policies of component model instances, and instead have provided a framework through which those policies may be applied to remote requests.12 This places a greater requirement upon the manual definition of appropriate policies within each component model instance; however, it ensures a consistent policy language.

Conclusion

We have defined an inter-operation framework through which multiple RPPM system graphs may be connected and remote authorization requests may be evaluated. The connecting of systems is commonplace; however, the ability to decompose large systems into inter-connected smaller systems is a significant contribution of this paper and of particular importance in the application of Re-BAC models. Decomposition enables a trade-off to be made between the computational complexity of a ReBAC model against the number of model instances which are employed to control authorizations within a large system.

The inter-connection of ReBAC (system) graphs through directed bridging relationships, and the use of system graph sequences and the path-vector routing protocol to identify paths between those graphs is applicable to remote request evaluation, no matter the model. This paper introduces its formal application in RPPM, although it is equally applicable to our more recent model, ARPPM [5] (something we leave for future work). 13 In cases where principal abstraction is not available, however, an alternative means of allowing each component graph's evaluation to contribute must be developed. We leave the development of such mechanisms to future work, only noting that an end-to-end path approach will produce a super-graph and thus, potentially, be limited by the increase in computational complexity associated with an increase in the number of nodes.

Appendix: Algorithms

The pseudocode for the algorithms used to support inter-connection of RPPM instances is shown below.

6:

Securely send G.q and G. ρ to G ′′ .h via G.h 7: else 8:

Reject malformed ORR

9: end if

Algorithm 3 ProcessIRR

Require: System graph Gi = (Vi, Ei), IRR Gi.q = ((G1.s, Gi.h, Gi-1. ρ ), G ℓ .v, G ℓ .a), policy graph Gi.Gρ = Gi.(Vρ, Eρ) Ensure: Set of matched principals Gi. ρ sent to next graph in system graph sequence (intermediate system graph) or authorization decision made (target system graph)

1: if Gi = G ℓ then 2:
// intermediate system graph

3:

LCPG i ,G ℓ ← DetermineLeastCostPathToSystemGraph(G ℓ )

4:

Gi.h ′ ← IdentifyLocalHubForLCP(LCPG i ,G ℓ )

5:

Gi. ρ ← EvaluatePolicyGraph(Gi.h, Gi.h ′ , Gi-1. ρ )

6:

Gi+1.h ← IdentifyNeighbourHubForLCP(LCPG i ,G ℓ )

7:

Securely send Gi.q and Gi. ρ to Gi+1.h via Gi.h ′ 8: else 9:

// target system graph 10:

Gi. ρ ← EvaluatePolicyGraph(Gi.h, G ℓ .v, Gi-1. ρ )

11:

Gi. ̺ ← ComputeAuthorizations(Gi. ρ )

12:

DecideAuthorizationResult(Gi. ρ , Gi. ̺ )

13: end if

Algorithm 1 2 : 5 :G

 125 EvaluatePolicyGraph (ordered compute principals)Require: System graph G = (V, E), start node u ∈ V , target node v ∈ V ,policy graph Gρ = (Vρ, Eρ), and set of matched principals ρ Ensure: Returns set of matched principals ρ 1: while Perform breadth-first search of Gρ starting at root vertex do Evaluate current vertex, (φ, ψ, p) ∈ Vρ 3:if G, u, v |= φ and G, u, v |= ψ then System graph G = (V, E), ORR G.q = (G.s, G ′ .v, G ′ .a), policy graph G.Gρ = G.(Vρ, Eρ)Ensure: Malformed ORR rejected or set of matched principals G. ρ sent to next system graph in system graph sequence1: LCP G,G ′ ← DetermineLeastCostPathToSystemGraph(G ′ ) 2: if G ′ reachable then 3: G.h ← IdentifyLocalHubForLCP(LCP G,G ′ )4:G. ρ ← EvaluatePolicyGraph(G.s, G.h, ∅) ′′ .h ← IdentifyNeighbourHubForLCP(LCP G,G ′ )

We use the term super-graph to identify a large system graph which models multiple systems which might otherwise be modelled by distinct stand-alone system graphs.

We require an extra-model administrator to be responsible for the management of these bridging relationships.

Where there is no ambiguity through context or element naming we continue to leave out the prefix for convenience and clarity. So we do not prefix V1 and E1 in G1 = (V1, E1), for example.

Note that the example of Figure1ccould equally represent three distinct system graphs which have been connected together, or a large stand-alone system graph which has been decomposed into three subsystems.

The directionality of bridges is enforced by hub entities not exchanging system path information against the direction of an incident bridge.

Recall that a system graph sequence will document the chain of system graphs between the originating system graph and the target system graph.

Note that we do not add the null principal to the set of matched principals (line 4 of Algorithm 1) so that it does not interfere with authorization decisions, no matter the conflict resolution strategy employed; and that the algorithm is passed a set of matched principals to which any it matches are added.

In Algorithm 2 and Algorithm 3 calls to EvaluatePolicyGraph have been simplified, removing the system graph and policy graph arguments so as to highlight the start entity, target entity, and set of matched principals arguments.

Note that the originating remote request G.q = (G.s, G ′ .v, G ′ .a) retains the same underlying structure as a local request made within the same system graph G.q = G.(s, v, a).

The function DetermineLeastCostPathToSystemGraph requires the PDP to interrogate its local hubs and to collate their responses, as described in Section 2.

An appropriate mechanism (e.g. digital signatures) must be in place to enable the receiving system to ensure the authenticity and freshness of such details.

That being said we support the use of remote principals where desired to provide for more robust policies.

We believe that administrative requests will always be local to a model instance (maintaining system autonomy) and so only operational requests (equivalent to the requests discussed in this paper) may be conducted remotely.


Ultan Neville

Simon N Foley

Reasoning About Firewall Policies Through Refinement and Composition

Keywords: Firewalls, Algebra, iptables, Anomalies, Policy-composition

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 is used to specify and reason about iptables firewall policy configurations. A prototype policy management toolkit has been implemented.

Introduction

Firewall configuration management is complex and error-prone, and a misconfigured policy may permit accesses that were intended to be denied or vice-versa. We regard the specification of a firewall policy as a process that evolves. Threats to, and access requirements for, resources behind a firewall do not usually remain static, and over time, a policy or distributed policy configuration may be updated on an ad-hoc basis, possibly by multiple specifiers/administrators. This can be problematic and may introduce anomalies; whereby the intended semantics of the specified access controls become ambiguous.

In this paper, we present a firewall policy algebra FW 1 for constructing and reasoning over anomaly-free policies. The algebra allows policies to be composed in such a way that the result upholds the access requirements of each policy involved; and permits one to reason as to whether some policy is a safe (secure) replacement for another policy in the sense of [START_REF] Foley | The specification and implementation of commercial security requirements including dynamic segregation of duties[END_REF][START_REF] Jacob | The varieties of refinement[END_REF]. The proposed algebra is used to reason about iptables firewall policy configurations. A partial mapping for the iptables filter table is given in the algebra. iptables is a command line utility used to define policies for the Linux kernel firewall Netfilter [START_REF]Linux iptables -CLI for configuring the Linux kernel firewall[END_REF]. We focus on stateful firewall policies that are defined in terms of constraints on source/destination IP/port ranges, the TCP, UDP and ICMP protocols, and additional filter condition attributes.

The primary contribution of this paper is an algebra FW 1 , that can be used to reason about firewall policies using refinement and composition operators. The effectiveness of the algebra is demonstrated by its application to anomaly detection, and standards compliance.

The paper is organised as follows. Section 2 introduces the notion of adjacency, which is at the heart of reasoning about/composing firewall rules that involve IP/port ranges. In Section 3 we define datatypes for firewall rule attributes, such as IP/port ranges. Section 4 defines the firewall policy algebra FW 1 . In Section 5, we use FW 1 to reason about firewall policies in practice. Section 6 describes a prototype policy management toolkit for iptables and presents some preliminary results. Related work is outlined in Section 7 and Section 8 concludes the paper. The Z notation [START_REF] Spivey | The Z Notation: A Reference Manual[END_REF] is used to present the algebra and has been syntax-and type-checked using the f uzz tool.

A Theory of Adjacency

A firewall policy is conventionally defined as a sequence of order-dependent rules. A rule is composed of filter conditions and a target action. Filter conditions usually consist of fields/attributes from IP, TCP/UDP headers; with the most commonly used attributes being source/destination IP/port, and network protocol. Target actions are usually allow or deny [START_REF] Al-Shaer | Firewall policy advisor for anomaly discovery and rule editing[END_REF][START_REF] Cuppens | Detection and removal of firewall misconfiguration[END_REF].

Range-based filter condition attributes (IPs/ports) have logical mappings to intervals of N. For example, the port range that includes all ports from SSH up and including HTTP can be written as the interval [22 . . 80]. Consider as part of a running example, a system that is capable of enforcing firewall rules where the filter condition attribute for the rules is destination port range. Then if we had a rule that allowed all ports from SSH to HTTP, it may look like: (i , [22 . . 80], allow ), where i is the index of the rule in the policy, [22 . . 80] is the required port range, and allow means that network traffic matching this pattern be permitted traversal of the firewall. Suppose we had a second rule, that specifies allow everything from Quote Of The Day (QOTD) up to and including FTP Control. Then (j , [17 . . 21], allow ), specifies that for the rule at index j ; the required port range [17 . . 21] is allowed. Intuitively, we can see that the port ranges for the rules at index i and index j are adjacent, and we may want to join rules i and j into a single rule that looks like (k , [17 . . 80], allow ). This notion of adjacency becomes more complex when we consider comparing/composing firewall rules comprising 2 . . n filter condition attributes.

The Adjacency Specification

In this section we define the filter condition attribute relationships of adjacency, disjointness and subsumption. These relationships are at the heart of adjacency, and ultimately the FW 1 algebra.

Let IV[min, max ] be the set of all intervals on the natural numbers, from min up to and including max . Intervals are defined by their corresponding sets.

IV[min, max ] == {S : P N | ∃ ⊥, : S • ∀ x : S • min ≤ ⊥ ≤ x ≤ ≤ max } For example, IV[1, 3] gives {[1 . . 1], [1 . . 2], [1 . . 3], [2 . . 2], [2 . . 3], [3 . . 3]}.
For ease of exposition and when no ambiguity arises, we may write an interval as a pair [⊥ . . ], rather than by the set it defines. Let IPv 4 define the set of all possible IPv4 address ranges, and similarly, let Port define the set of all possible network port ranges, where

IPv 4 == IV[0, 2 32 -1] ∧ Port == IV[0, 2 16 -1].
Adjacency Two intervals are adjacent if their union defines a single interval. We generalize this to any attribute of type X , whereby for a, b ∈ X , if a X b, then a and b are adjacent in the set X .

[X ]

:

P X → (X ↔ X ) ∀ a, b : X • a X a ∧ (a X b ⇒ b X a) For example, interval [1 . . 2] is adjacent to interval [3 . . 3], thus [1 . . 2] IV[1,3] [3 . . 3]. It follows for a, b ∈ N that a N b ⇔ (a = b ∨ a + 1 = b ∨ b + 1 = a),
and given S , T ∈ P X then S P X T ⇔ true.

Disjointness Two intervals are disjoint if they don't intersect. Given a, b ∈ X , a | X b denotes a and b are disjoint in X .

[X ]

| : P X → (X ↔ X ) ∀ a, b : X • ¬ (a | X a) ∧ (a | X b ⇒ b | X a)
For example, [1.

.2] and [3. Subsumption An interval I subsumes (covers) an interval J , if

J ⊆ I . For a, b ∈ X , if a X ← b then b covers a in X .
The properties of reflexivity, transitivity and antisymmetry define X ← as a non-strict partial order over X [START_REF] Birkhoff | Lattice Theory[END_REF].

[X ]

← : P X → (X ↔ X ) ∀ a, b, c : X • a X ← a ∧ (a X ← b ∧ b X ← c ⇒ a X ← c) ∧ (a X ← b ∧ b X ← a ⇒ a = b) For example, [1 . . 3] covers [3 . . 3], thus [3 . . 3] IV[1,3] ← [1 . . 3]. It follows for a, b ∈ N that a N ← b ⇔ a = b, and given S , T ∈ P X , then S P X ← T ⇔ S ⊆ T .
For a set X and S ∈ P X , the flattening function S gives the cover-set for the elements of S .

[X ]

:

P X → P X ∀ S : P X • S = S \ {a, a : S | a X ← a ∧ a = a • a} For example, IV[1, 3] = {[1 . . 3]}.
We define a difference operator for S , T ∈ P X , where S \ P X T gives the relative compliment of T in S .

[X ]

\ : P(P X ) → P X × P X → P X ∀ S , T :

P X • S \ P X T = {a : S ; c : X | c X ← a ∧ (∀ b : T • ¬ (c X ← b)) • c} For example, IV[1, 3] \ IV[1,3] {[1 . . 1], [3 . . 3]} = {[2 . . 2]}.

Filter Condition Attribute Datatypes

In this section we define the datatypes used to construct the filter condition attributes for the FW 1 policy model.

The Adjacency Datatype

For a set X , the Adjacency datatype α[X ], is the set of all closed subsets of X partitioned by adjacency. Adjacency Ordering An ordering can be placed over Adjacency-sets, and is defined as follows.

α[X ] == {S : P X | (∀ a, b : S | a = b • ¬ (a X b))} For example α[IV[1, 3]] gives {{[1 . . 1]}, {[1 . . 2]}, {[1 . . 3]}, {[2 . . 2]}, {[2 . . 3]}, {[3 . . 3]}, {[1 . . 1],[3 . .
[X ] ⊥, : α[X ] not : α[X ] → α[X ] ≤ : α[X ] ↔ α[X ] ⊗ , ⊕ : α[X ] × α[X ] → α[X ] ⊥ = ∅ ∧ = X ∀ S , T : α[X ] • notS = \ α[X ] S ∧ S ≤ T ⇔ (∀ a : S • ∃ b : T • a X ← b) ∧ S ⊗ T = {U : α[X ] | ∀ c : U • ∃ a : S ; b : T • c X ← a ∧ c X ← b} ∧ S ⊕ T = {U : α[X ] | ∀ c : U • ∃ a : S ; b : T • a X ← c ∨ b X ← c}
The elements ⊥, ∈ α[X ] define the least and greatest bounds, respectively, on α[X ], where for any S ∈ α[X ], then ⊥ ≤ S ≤ . Adjacency negation defines a valid complement operator in α[X ], where (S ⊕not S ) = and (S ⊗not S ) = ⊥.

Adjacency Intersection Under this ordering, the meet, or intersection S ⊗ T of S , T ∈ α[X ] is defined using subsumption, as the cover-set for the generalized union of all Adjacency-sets, where each element of (S ⊗ T ) is covered by an element in both S and T . Intuitively, this means that the values of the meet are all non-empty intersections of each value in S with each value in T . Under the ordering relation ≤, ⊗ provides a greatest lower bound (glb) operator, and S ⊗ T is covered by both S and T , that is (S ⊗ T ) ≤ S and (S ⊗ T ) ≤ T .

Adjacency Union

The join of S , T ∈ α[X ] is defined using subsumption, as the generalized intersection of all Adjacency-sets, where each element of (S ⊕ T ) covers an element in either S or T . Intuitively, this means that the values of the join are exactly a union of the elements from both S and T . Given the definition of ordering using subsumption, it follows that the Adjacency join provides a lowest upper bound (lub) operator. Since ⊕ provides a lub operator we have S ≤ (S ⊕ T ) and T ≤ (S ⊕ T ).

Proposition The poset (α[X ], ≤) forms a distributive lattice with compliment operator not. This follows from the definition of ≤ as a subsumption ordering/an antisymmetric preorder, the properties of not, the intuitive definition of the meet of S , T ∈ α[X ] as all non-empty intersections of each value in S with each value in T , and the intuitive definition of the join operation as an exact union of the elements from both S and T [START_REF] Levine | Lemma 3, Example 6.) Algebraic Combinatorics[END_REF].

Given the adjacency, disjointness and subsumption relations; then for S , T ∈

α[X ], we define S α[X ] T ⇔ true ∧ S | α[X ] T ⇔ S ⊗T = ⊥ ∧ S α[X ] ← T ⇔ S ≤ T .

The Duplet Datatype

A duplet is an ordered pair, where the set of all duplets for types X , Y , is defined as

δ[X , Y ], where δ[X , Y ] == X × Y . For example, δ[IV[1, 1], IV[1, 2]] gives {([1 . . 1],[1 . . 1]), ([1 . . 1],[1 . . 2]), ([1 . . 1], [2 . . 2])}, and δ[α[IPv 4], α[Port]]
gives the set of all duplets for adjacency-free IP/port-ranges.

Recall the earlier example of the firewall system that supports only destination port range filter conditions. Suppose we want to extend the expressiveness of the policy rules for this system to include a definition for destination IP range.

Then α[δ[α[IPv 4], α[Port]]],
is the set of all closed subsets of adjacency-free IP/port-range duplets, partitioned by adjacency. Consider two policy requirements, where network traffic is to be allowed to the IP range [1 . . 3] on ports [1 . . 3], and to the IP range [2 . . 4] on ports [2 . . 4]. Then modelling this using sets of adjacency-free duplets, we have S ,

T ∈ α[δ[α[IPv 4], α[Port]]], where S == {({[1 . . 3]}, {[1 . . 3]})} and T == {({[2 . . 4]}, {[2 . . 4]})}.
Duplet Disjointness A pair of duplets are disjoint if the attributes in the first coordinate are disjoint, or the attributes in the second coordinate are disjoint.

For (a 1 , b 1 ), (a 2 , b 2 ) ∈ δ[X , Y ], then: (a 1 , b 1 ) | δ[X ,Y ] (a 2 , b 2 ) ⇔ (a 1 | X a 2 ∨ b 1 | Y b 2 ) For example, ¬ (S | α[δ[α[IPv 4],α[Port]]] T ).
Duplet Adjacency A pair of duplets are adjacent if the attributes in the first coordinate are adjacent, and the attributes in the second coordinate are not disjoint. Thus, we have:

(a 1 , b 1 ) δ[X ,Y ] (a 2 , b 2 ) ⇔ (a 1 X a 2 ∧ ¬ (b 1 | Y b 2 )) For example, S α[δ[α[IPv 4],α[Port]]] T .
Duplet Subsumption A duplet is distinguished from a standard ordered pair, whereby we explicitly define orderings separately in each coordinate. For example, suppose we wanted to join adjacent policies S and T , then under a 'standard' Cartesian product ordering we have

S ⊕ T = {({[1 . . 4]}, {[1 . . 4]})}.
This obviously results in an overly permissive policy, conversely; an overly restrictive policy if we were composing deny rules. A duplet (a

1 , b 1 ) covers a duplet (a 2 , b 2 ) in δ[X , Y ], if a 1 covers a 2 in X , and b 2 covers b 1 in Y . Thus: (a 2 , b 2 ) δ[X ,Y ] ← (a 1 , b 1 ) ⇔ (a 2 X ← a 1 ∧ b 1 Y ← b 2 ) Then we have S ⊕ T = {({[1 . . 4]}, {[2 . . 3]}), ({[1 . . 3]}, {[1 . . 1]}), ({[2 . . 4]}, {[4 . . 4]})}.
Thus, the join, or union (S ⊕ T ) of S and T , defines the adjacencyfree coalescence of all duplets from S and T . For reasons of space, we do not give the implementation definition for this operation.

The Stateful/Protocol Datatype

In this section, we define the network protocols of interest for the model and encode a notion of state. The iptables command line utility allows the end-user to specify one (or all) of seven different protocols in a rule [START_REF]Linux iptables -CLI for configuring the Linux kernel firewall[END_REF]. For reasons of space, we focus only on the TCP, UDP and ICMP protocols.

Let Flags be the set of TCP flags, where Flags :

:= syn | ack | fin | psh | rst | urg.
The TCP protocol is defined as the set of all sets of pairs of sets of Flags, whereby for each pair; the first set contains the flags that are to be examined in a packet-header, and the second set contains the flags that must be set (in a packet-header). In [START_REF]Linux iptables -CLI for configuring the Linux kernel firewall[END_REF], these are referred to as the comp and mask values for a packet, respectively. Let TCP be the set of all sets of comp/mask pairs, where TCP == P(P Flags × P Flags). Let [TypesCodes] be the set of all valid ICMP Type/Code pairs. For simplicity and reasons of space, we do not consider how the values of TypesCodes may be constructed, other than to assume that the usual human-readable notation can be used, such as (8,0) and (17,0) ∈ TypesCodes. The iptables conntrack modules' statelist [START_REF]Linux iptables -CLI for configuring the Linux kernel firewall[END_REF] may be defined as follows. Let State be the set of connection tracking states for a packet/connection, where State ::

= new | established | related | invalid | untracked.
Let Protocol define the set of all protocols, given as the set of all duplets over TCP , UDP ([0 . . 1]), ICMP (P TypesCodes) and the set of all sets of connection tracking states (P State).

Protocol == δ[TCP , δ[{0, 1}, δ[P TypesCodes, P State]]]
Proposition The Protocol datatype forms a product-lattice structure. This follows from the definition of Protocol as the product of powerset/binary lattices [START_REF] Birkhoff | Lattice Theory[END_REF]. [START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF] The F W 1 Policy Algebra

In this section we define an algebra FW 1 , for constructing and reasoning about anomaly-free firewall policies. We focus on stateful firewall policies that are defined in terms of constraints on source/destination IP/port ranges, the TCP, UDP and ICMP protocols.

A filter condition is a five-tuple (s, sprt, d , dprt, p), representing network traffic originating from source IP range s, with source port range sprt, destined for destination IP range d , with destination port range dprt, using statefulprotocols p. Let FC define the set of all filter conditions, where:

FC == δ[α[IPv 4], δ[α[Port], δ[α[IPv 4], δ[α[Port], Protocol ]]]]
A firewall policy defines the filter conditions that may be allowed or denied by a firewall. Let Policy define the set of all firewall policies, whereby:

Policy == {A, D : α[FC ] | ∀ a : A; d : D • a | FC d }
A firewall policy (A, D) ∈ Policy defines that a filter condition f ∈ A should be allowed by the firewall, while a filter condition f ∈ D should be denied. Given (A, D) ∈ Policy then A and D are disjoint: this avoids any contradiction in deciding whether a filter condition should be allowed or denied. Given that A and D are also both adjacency-free; then Policy defines the set of anomaly-free firewall policies in the sense that they contain no redundancy, shadowing, or other anomalies [START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF].

Note that (A, D) ∈ Policy need not partition FC : the allow and deny sets define the filter conditions to which the policy explicitly applies, and an implicit default decision is applied for those filter conditions in FC \ α[FC ] (A ⊕ D). For the purposes of modelling iptables firewalls it is sufficient to assume default deny, though we observe that FW 1 can also be used to reason about default allow firewall policies. The policy destructor functions allow and deny are analogous to functions first and second for ordered pairs:

allow , deny : Policy → α[FC ] ∀ A, D : α[FC ] • allow (A, D) = A ∧ deny (A, D) = D
Policy Refinement An ordering can be defined over firewall policies, whereby given P , Q ∈ Policy then P Q means that P is no less restrictive than Q, that is, any filter condition that is denied by Q is denied by P . Intuitively, policy P is considered to be a safe replacement for policy Q, in the sense of [START_REF] Foley | The specification and implementation of commercial security requirements including dynamic segregation of duties[END_REF][START_REF] Jacob | The varieties of refinement[END_REF] and any firewall that enforces policy Q can be reconfigured to enforce policy P without any loss of security. The set Policy forms a lattice under the safe replacement ordering and is defined as follows.

FW 1 ⊥, : Policy : Policy ↔ Policy , : Policy × Policy → Policy ⊥ = (∅, FC ) ∧ = ( FC , ∅) ∀ P , Q : Policy • P Q ⇔ ((allow P ≤ allow Q) ∧ (deny Q ≤ deny P )) ∧ P Q = (allow P ⊗ allow Q, deny P ⊕ deny Q) ∧ P Q = (allow P ⊕ allow Q, deny P ⊗ deny Q)
Formally, P Q iff every filter condition allowed by P is allowed by Q and that any filter conditions explicitly denied by Q are also explicitly denied by P . Note that in this definition we distinguish between filter conditions explicitly denied in the policy versus those implicitly denied by default. This means that, everything else being equal, a policy that explicitly denies a filter condition is considered more restrictive than a policy that relies on the implicit default-deny for the same network traffic pattern. Safe replacement is defined as the Cartesian product of Adjacency orderings over allow and deny sets and it therefore follows that (Policy, ) is a poset.

⊥ and define the most restrictive and least restrictive policies, that is, for any P ∈ Policy we have ⊥ P . Thus, for example, any firewall enforcing a policy P can be safely reconfigured to enforce the (not very useful) firewall policy ⊥.

Policy Intersection Under this ordering, the meet P Q, of two firewall policies P and Q is defined as the policy that denies any filter condition that is explicitly denied by either P or Q, but allows filter conditions that are allowed by both P and Q. Intuitively, this means that if a firewall is required to enforce both policies P and Q, it can be configured to enforce the policy (P Q) since P Q is a safe replacement for both P and Q, that is; (P Q) P and (P Q) Q. Given the definition of safe replacement as a product of two Adjacency lattices, it follows that the policy meet provides the glb operator. Thus, P Q provides the 'best'/least restrictive safe replacement (under ) for both P and Q.

Policy Union The join of two firewall policies P and Q is defined as the policy that allows any filter condition allowed by either P or Q, but denies filter conditions that are explicitly denied by both P and Q. Intuitively, this means that a firewall that is required to enforce either policy P or Q can be safely configured to enforce the policy (P Q). Since provides a lub operator we have P (P Q) and Q (P Q).

Proposition The set of all policies Policy forms a lattice under safe replacement. This follows from the definition of as a Cartesian product of two Adjacency lattice orderings.

Constructing Firewall Policies

The lattice of policies FW 1 provides us with an algebra for constructing and interpreting firewall polices. The following constructor functions are used to build primitive policies. Given a set of adjacency-free filter conditions A, then (Allow A) is a policy that allows filter conditions in A, and (Deny D) is a policy that explicitly denies filter conditions in D.

Allow, Deny

: α[FC ] → Policy ∀ S : α[FC ] • Allow S = (S , ∅) ∧ Deny S = (∅, S )
This provides what we refer to as a weak interpretation of allow and deny. Network traffic patterns that are not explicitly mentioned in parameter S are default-deny and therefore are not specified in the deny set of the policy. The following provides us with a strong interpretation for these constructors:

Allow + , Deny + : α[FC ] → Policy ∀ S : α[FC ] • Allow + S = (S , not S ) ∧ Deny + S = (not S , S )
In this case (Allow + A) allows filter conditions specified in A, while explicitly denying all other filter conditions, and (Deny + D) denies filter conditions specified in D while allowing all other filter conditions.

Proposition A firewall policy P ∈ Policy can be decomposed into it's corresponding allow and deny sets, and re-constructed using the algebra; for any (A, D) ∈ Policy, since A and D are disjoint then:

(Allow + A) (Deny D) = (A, FC \ α[FC ] A) (∅, D) = (A, D) = (Allow A) (Deny + D)

Reasoning About Policies in Practice

Sequential Composition A firewall policy is conventionally constructed as a sequence of rules, whereby for a given network packet, the decision to allow or deny that packet is checked against each policy rule, starting from the first, in sequence, and the first rule that matches gives the result that is returned. The algebra FW 1 can be extended to include a similar form of sequential composition of policies. The policy constructions above can be regarded as representing the individual rules of a conventional firewall policy.

Let (Allow A) o 9 Q denote a sequential composition of an allow rule (Allow A) with policy Q with the interpretation that a given network packet matched in A is allowed; if it does not match in A then policy Q is enforced. The resulting policy either: allows filter conditions in A (and denies all other filter conditions), or allows/denies filter conditions in accordance with policy Q. We define:

(Allow A) o 9 Q = (Allow + A) Q = ((A ⊕ allow (Q)), (( FC \ α[FC ] A) ⊗ deny(Q))) = ((A ⊕ allow (Q)), (deny(Q) \ α[FC ] A))
which is as expected. A similar definition can be provided for the sequential composition (Deny D) o 9 Q, whereby a given network packet that is matched in D is denied; if it does not match in D then policy Q is enforced. We define:

(Deny D) o 9 Q = (Deny + D) Q = (allow (Q) \ α[FC ] D, deny(Q) ⊕ D)
While in practice its usual to write a firewall policy in terms of many constructions of allow and deny rules, in principle, any firewall policy P ∈ Policy can be defined in terms of one allow policy (Allow allow (P )) and one deny policy (Deny deny(P )) and since the allow and deny sets of P are disjoint we have P o 9 Q = (Deny deny(P )) o 9 (Allow allow (P )) o 9 Q. We define this as:

o 9 : Policy × Policy → Policy ∀ FW 1 ; P , Q : Policy • P o 9 Q = (Q (Allow + (allow (P ))
)) (Deny + (deny(P ))) Let Rule define the set of all firewall rules, where Rule ::= allow FC | deny FC . We define a rule interpretation function as:

I : Rule → Policy ∀ f : FC • I(allow f ) = Allow({f }) ∧ I(deny f ) = Deny({f })
A firewall policy is defined as a sequence of rules r 1 , r 2 , . ., r n , for r i ∈ Rule, and is encoded in the policy algebra as I(r 1 ) o 9 I(r 2 ) o 9 . . o 9 I(r n ).

Policy Negation

The policy negation of P ∈ Policy allows filter conditions explicitly denied by P and explicitly denies filter conditions allowed by P . We define:

not : Policy → Policy ∀ FW 1 ; P : Policy • not P = (Allow + (deny (P ))) (Deny (allow (P )))

From this definition it follows that (not P ) is simply (deny (P ), allow (P )) and thus not (Deny D) = (Allow D) and not (Allow A) = (Deny A). Note however, that in general policy negation does not define a complement operator in the algebra FW 1 , that is, it not necessarily the case that (P not P ) = and (P not P ) = ⊥.

Anomaly Analysis

A firewall policy is conventionally constructed as a sequence of order-dependent rules, and when a network packet matches with two or more policy rules, the policy is anomalous [START_REF] Al-Shaer | Firewall policy advisor for anomaly discovery and rule editing[END_REF][START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF][START_REF] Cuppens | Detection and removal of firewall misconfiguration[END_REF]. By definition, the adjacency-free allow and deny sets of some P ∈ Policy are disjoint, therefore P is anomaly-free by construction. We can however define anomalies using the algebra; by considering how a policy changes when composed with other policies.

Redundancy A policy P is redundant given policy Q if their composition results in no difference between the resulting policy and Q, in particular, if

P o 9 Q = Q.
Shadowing Some part of policy Q is shadowed by the entire policy P in the composition P o 9 Q if the filter condition constraints that are specified by P contradict the constraints that are specified by Q, in particular, if (not P ) o 9 Q = Q. This is a very general definition for shadowing. Perhaps a more familiar interpretation of this definition is one where the policy P is a specific allow/deny rule that shadows a part or all of the policy with which it is composed. Recall that (not(Allow A)) = (Deny A) and, for example, in (Allow A) o 9 Q all or part of policy Q is shadowed by the rule/primitive policy (Allow A) if Q denies the filter conditions specified in A, that is, (Deny A) o 9 Q = Q. Similarly, in (Deny D) o 9 Q part or all of policy Q is shadowed by the rule/primitive policy (Deny D) if (not (Deny D)) o 9 Q = Q. Further definitions for shadowing may be constructed using the algebra. For example, an initial interpretation of the generalisation anomaly [START_REF] Al-Shaer | Firewall policy advisor for anomaly discovery and rule editing[END_REF] in the composition P o 9 Q; is where Q is generalised by P if all of P shadows (specifically) part of Q. We are currently investigating how this and other anomalies can be reasoned about within the algebra.

Inter-policy Anomalies Anomalies can also occur between the different policies of distributed firewall configurations [START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF]. In the following, assume that P is a policy on an upstream firewall and Q is a policy on a downstream firewall.

An inter-redundancy anomaly exists between policies P and Q if some part of Q is redundant to some part of P , whereby the target action of the redundant filter conditions is deny. Given some set of filter conditions A denied by P , and some set of filter conditions B denied by Q, if (Deny A) o 9 (Deny B ) = (Deny A) then there exists an inter-redundancy between P and Q.

An inter-shadowing anomaly exists between policies P and Q if some part of Q's allows are shadowed by some part of P 's denies. Given some set of filter conditions A denied by P , and some set of filter conditions B allowed by Q, if (Deny A) o 9 (Allow B ) = (Deny A), then there is an inter-shadowing anomaly between P and Q.

An inter-spuriousness anomaly exists between policies P and Q if some part of Q's denies are shadowed by some part of P 's allows. Again, given some set of filter conditions A allowed by P , and some set of filter conditions B denied by Q, if (Allow A) o 9 (Deny B ) = (Allow A), then there exists an inter-spuriousness anomaly between P and Q.

Standards Compliance

RFC 5735 [START_REF] Cotton | Special Use IPv4 Addresses[END_REF], details fifteen IPv4 address blocks/ranges that have been assigned by the Internet Assigned Numbers Authority (IANA) for specialized/global purposes. Some of these address spaces may appear on the Internet, and may be used legitimately outside a single administrative domain, however, while the assigned values of the ranges do not directly raise security issues; unexpected use may indicate an attack [START_REF] Cotton | Special Use IPv4 Addresses[END_REF]. For example, packets with a source IP address from the private address space 172.16.0.0/12, arriving on the Wide Area Network interface of a network router, may be considered spoofed, and may be part of a Denial of Service (DoS), or Distributed DoS attack.

RFC 5735 Compliance An IP spoof-mitigation compliance policy RFC5735 is defined. Best practice recommendations are implemented for each of the fifteen specialized IP ranges in [START_REF] Cotton | Special Use IPv4 Addresses[END_REF], resulting in one hundred and twenty iptables deny rules. In [START_REF] Fitzgerald | MASON: Mobile autonomic security for network access controls[END_REF], we defined this deny ruleset for a firewall management tool, we do not give the definition here for reasons of space. The compliance policy terminates with a final iptables rule that specifies all other traffic be permitted. To model these iptables rules in the algebra, we define some additional filter condition attributes and provide a more formal definition of RFC5735.

An Extended Firewall Policy An attribute for the iptables filter table chains may be defined as Chain ::= input | output | forward. Direction-based filtering may be given as Dir ::= ingress | egress, and the set of all sets of interfaces on a machine may be given as P Iface, where for simplicity, we assume elements of Iface resemble eth0, wlan0, tun0, etc. Let AdditionalFC be the set of all duplets for additional filter condition attributes of interest for this paper, whereby:

AdditionalFC == δ[P Chain, δ[P Dir , P Iface]]
A revised definition for the set of all filter conditions FC I is given as:

FC I == δ[α[IPv 4], δ[α[Port], δ[α[IPv 4], δ[α[Port], δ[Protocol , AdditionalFC ]]]]]
A revised definition for the set of all policies Policy I is given as:

Policy I == {A, D : α[FC I ] | ∀ a : A; d : D • a | FC I d }
The compliance policy RFC5735 ∈ Policy I , defines the minimum requirement for what it means for some perimeter network firewall policy to mitigate the threat of IP spoofing for all traffic, in accordance with RFC 5735. Thus, we have for all P ∈ Policy I , if P RFC5735, then P complies with the best practice recommendations outlined in [START_REF] Cotton | Special Use IPv4 Addresses[END_REF] for IP spoof-mitigation.

Encoding and Evaluating iptables Policies

A prototype policy management toolkit has been implemented in Python for iptables. We reason over Policy I policies using ( o 9 , , ); time-based performanceanalysis tests were conducted. The test-bed for the experiments was a 64-Bit Ubuntu 14.04 LTS OS, running on a Dell Latitude E6430, with a quad-core Intel i5-3320M processor and 4GB of RAM. Every experiment was conducted three times; the median result chosen for inclusion in this paper. Overall, the results are promising.

Evaluating Sequential Policy Composition Two datasets were generated for experimentation. Each dataset consists of iptables policies of size 2 4 . . 2 11 . One dataset contains policies where no rule is adjacent to any other rule (other than itself), and the other dataset consists of policies where every new rule is adjacent to the previous rule; to ensure the maximum number of possible rules are generated as a result of composition. The rules all have a target action of allow. The implementation parses the system's currently enforced iptables ruleset r 1 , r 2 . . r n by chain, and then normalizes each rule to a primitive/singleton policy I(r 1 ), I(r 2 ) . . I(r n ) . The overall policy for the chain is evaluated as I(r 1 ) o 9 I(r 2 ) o 9 . . o 9 I(r n ). For reasons of space, we give the results for the sequential composition experiments as lists of tuples (P,T (P)), where P is the policy named by the number of iptables rules it was constructed from for the experiment, and T (P) is the time taken in seconds for the evaluation of the sequential composition of the rules in P. For the adjacent dataset we have [(2 4 , 0.80), (2 5 , 2.02), (2 6 , 5.13), (2 7 , 15.32), (2 8 , 51.18), (2 9 , 183.42), (2 10 , 707.15), (2 11 , 2792.81)]. We observe that the evaluation time for the sequential composition of 2 9 rules is around three minutes, and T (2 11 ) is approximately forty six minutes. For the non-adjacent dataset, we have [(2 4 , 0.07), (2 5 , 0.13), (2 6 , 0.29), (2 7 , 0.67), (2 8 , 1.73), (2 9 , 4.98), (2 10 , 16.09), (2 11 , 57.81)], and we see that for the largest ruleset, 2 11 , T (2 11 ) is approximately one minute.

Evaluating Policy Union Experiments were conducted to test policy lub, whereby each policy in the adjacent dataset was split into two policies, where the first policy contains the odd (index) rules from the original policy, and the second policy contains the even (index) rules from the original policy. Then for each P , Q ∈ Policy I in this split dataset, the time taken for the operation P Q is encoded in the matrix in Table 1. The times taken for composition of policies of equal size are approximately the same as (slightly less than) those for the results given in the adjacent sequential composition dataset. This is highlighted through the diagonal in the matrix, and is as expected; given that we used all allow rules.

Evaluating Policy Compliance A further dataset consisting of iptables policies of size 2 4 . . 2 11 was generated to test policy compliance. Each policy in this dataset was RFC 5735 compliant by construction. Results are again given as a list of tuples (P,T (P)), where P is the policy named by the number of iptables rules it was constructed from for the experiment, and T (P) is the time taken in seconds for the evaluation of P RFC5735. We have [(2 4 , 1.07 ×10 -3 ), (2 5 , 1.62 ×10 -3 ), (2 6 , 2.23 ×10 -3 ), (2 7 , 3.50 ×10 -3 ), (2 8 , 5.24 ×10 -3 ), (2 9 , 1.03 ×10 -2 ), (2 10 , 2.76 ×10 -2 ), (2 11 , 4.95 ×10 -2 )], and we see that for each P ∈ Policy I in this compliance-dataset T (P) is negligible.

Related Work

In [START_REF] Al-Shaer | Firewall policy advisor for anomaly discovery and rule editing[END_REF], a firewall policy is modelled as a single rooted tree, relations between rules are defined on a pairwise basis, and definitions for firewall configuration anomalies are provided. In [START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF], the work is extended to distributed firewall policies. In [START_REF] Cuppens | Detection and removal of firewall misconfiguration[END_REF], a firewall policy is modelled as a linked-list, and in [START_REF] Hari | Detecting and resolving packet filter conflicts[END_REF] rule relations within a policy are modelled in a directed graph. In [START_REF] Yuan | Fireman: A toolkit for firewall modeling and analysis[END_REF] Binary Decision Diagrams are used to model firewall rulesets. We model a firewall policy as an ordered pair of disjoint adjacency-free sets, where the set of policies Policy forms a lattice under , and each P ∈ Policy is anomaly-free by construction. In [START_REF] Al-Shaer | Firewall policy advisor for anomaly discovery and rule editing[END_REF][START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF][START_REF] Cuppens | Detection and removal of firewall misconfiguration[END_REF][START_REF] Hari | Detecting and resolving packet filter conflicts[END_REF][START_REF] Yuan | Fireman: A toolkit for firewall modeling and analysis[END_REF] an algorithmic approach is taken to detect/resolve anomalies. We follow an algebraic (as opposed to algorithmic) approach towards modelling anomalies in a single policy, and across a distributed policy configuration through policy composition. In earlier work [START_REF] Foley | A firewall algebra for openstack[END_REF], we developed the algebra FW 0 , and used it to reason over host-based and network access controls in OpenStack. In the FW 0 algebra, we focused on stateless firewall policies that are defined in terms of constraints on individual IPs, ports and protocols. In this paper, the algebra FW 1 is defined over stateful firewall policies constructed in terms of constraints on source/destination IP/port ranges, the TCP, UDP and ICMP protocols, and additional filter condition attributes. We argue that FW 1 gives a more expressive means for reasoning over OpenStack security group and perimeter firewall configurations. In [START_REF] Jarraya | Cloud calculus: Security verification in elastic cloud computing platform[END_REF], cloud calculus is used to capture the topology of cloud computing systems and the global firewall policy for a given configuration. This paper could extend the work in [START_REF] Jarraya | Cloud calculus: Security verification in elastic cloud computing platform[END_REF], given that FW 1 may be used in conjunction with cloud calculus to guarantee anomaly-free dynamic firewall policy reconfiguration, where the ordering relation may give a viable alternative for the given equivalence relation defined over 'cloud' terms for the formal verification of firewall policy preservation after a live migration. In [START_REF] Zhao | Policy algebras for hybrid firewalls[END_REF], a firewall policy algebra is proposed. However, the authors note that an anomaly-free composition is not guaranteed as a result of using their algebraic operators. Our work differs, in that policy composition under the , and o 9 operators defined in this paper all result in anomaly-free policies. In [START_REF] Adão | Mignis: A semantic based tool for firewall configuration[END_REF], an abstract model for Netfilter is proposed, and a language to specify firewall configurations is introduced that is similar to the XML-based access control language supported by Or-BAC presented in [START_REF] Cuppens | A formal approach to specify and deploy a network security policy[END_REF]. In [START_REF] Jeffrey | Model checking firewall policy configurations[END_REF], a formal model of Netfilter is defined, and the properties of reachability and cyclicity within firewall policy configurations are investigated. In [START_REF] Brucker | Formal firewall conformance testing: An application of test and proof techniques[END_REF], a theorem-proving approach is used to reason about firewall policies. The proposed algebra FW 1 is used to reason about and compose anomaly-free policies and therefore we do not have to worry about dealing with conflicts that may arise. Anomaly conflicts are dealt with in composition by computing anomalyfree policies, rather than using techniques such as [START_REF] Jajodia | Flexible support for multiple access control policies[END_REF] to resolve conflicts in policy decisions. Encoding a definition for Network Address Translation in FW 1 is a topic for research.

Conclusion

A policy algebra FW 1 is defined in which firewall policies can be specified and reasoned about. At the heart of this algebra is the notion of safe replacement, that is, whether it is secure to replace one firewall policy by another. The set of policies form a lattice under safe replacement and this enables consistent operators for safe composition to be defined. Policies in this lattice are anomaly-free by construction, and thus, composition under glb and lub operators preserves anomaly-freedom. A policy sequential composition operator is also proposed that can be used to interpret firewall policies defined more conventionally as sequences of rules. The algebra can be used to characterize anomalies, such as shadowing and redundancy, that arise from sequential composition. Best practice policy compliance may be defined using . The algebra FW 1 provides a formal interpretation of the network access controls for a partial mapping to the iptables filter table. FW 1 is a generic algebra and can also be used to model other firewall systems. The results in this paper are described in terms of the algebra FW 1 , for stateful firewall policies that are defined in terms of constraints on source/destination IP/port ranges, the TCP, UDP and ICMP protocols, and additional filter condition attributes.

. 3 ]

 3 are disjoint, thus [1. .2] | IV[1,3] [3. .3]. It follows for a, b ∈ N that a | N b ⇔ a = b, and given S , T ∈ P X then S | P X T ⇔ S ∩ T = ∅.

  3]}}, and α[IPv 4] defines the set of all closed subsets for the intervals of the IPv4 address range partitioned by adjacency.

Table 1 .

 1 Time taken to compute P Q (in seconds)

	P	Q 2 3	2 4	2 5	2 6	2 7	2 8	2 9	2 10
	2 3	0.65 0.79 0.81 0.99	1.40	2.51	5.73	16.93
	2 4	0.79 1.86 2.09 2.32	2.91	4.50	8.83	22.19
	2 5	0.81 2.09 4.97 5.45	6.78	9.17	15.50	32.89
	2 6	0.99 2.32 5.45 14.70 17.01 21.93	32.29	57.47
	2 7	1.40 2.91 6.78 17.01 48.85 58.44	76.94	119.28
	2 8	2.51 4.50 9.17 21.93 58.44 179.87 217.34 294.56
	2 9	5.73 8.83 15.50 32.29 76.94 217.34 699.11 839.49
	2 10 16.93 22.19 32.89 57.47 119.28 294.56 839.49 2722.63

Acknowledgement This work was supported, in part, by Science Foundation Ireland under grant SFI 10/CE/I1853 and Irish Research Council/Chist-ERA.