Introduction

Nowadays firewalls are pervasively deployed over the Internet to protect network portions (or single devices) against undesired/malicious traffic possibly threatening confidentiality, integrity and availability of the provided services. Firewalls implement security policies, which, operatively, translate in lists of rules, each consisting of a condition defined over some packet header fields (filtering fields), and an action. Firewalls operating according to the first matching strategy check incoming packets against rule conditions sequentially, until the matching rule (i.e., the first rule in the list whose condition is satisfied by the packet) is found, and then apply the corresponding action (i.e., typically 𝑎𝑙𝑙𝑜𝑤 or 𝑑𝑒𝑛𝑦).

Firewall operation also impacts the legitimate traffic and, especially during traffic load peaks (when the average packet arrival rate exceeds the firewall average service rate), legitimate packets may suffer high delays and even be lost before being processed because of overloads and overflows [1,2]. The time necessary to a firewall for processing a packet is mainly determined by the packet matching time, which is proportional to the number of rules against which the packet is checked before finding the matching one. In general, the higher the firewall cardinality (i.e., the number of rules in the list), the higher the firewall average service time. This criticality is exploited, for example, by DoF (Denial of Firewalling) attacks which generate traffic targeting the last rules in firewall lists [3].

Related works

Several techniques have been proposed to mitigate firewall impact on legitimate traffic. Some of them aim at minimizing firewall cardinality without changing the implemented security policy (e.g., policy analysis [4,5,6,7], firewall compression [8,9]), and are typically run offline, before actual firewall configuration. Others, lean on the observation that traffic characteristics remain constant for long periods of time and aim at ordering firewall rules so that those with higher matching probability are at the top of the list, allowing the majority of packets to be checked against a small number of rules (rule ordering [10,11,12,13]). The latter are run online, any time a change in the traffic profile is detected. Although effective, these techniques may not be sufficient to avoid firewall overloads and overflows, especially during traffic load peaks. Indeed, complex security policies may result in hundreds of rules even after analysis/compression. Moreover, compression often leads to lists of highly dependent rules which cannot easily be reordered, limiting the improvements achievable by compression and ordering combined. Finally, if the packet arrival rate increases but the distribution of matching probability among firewall rules does not change consistently, rule ordering is not helpful.

The technique we propose can be used in combination with all the previously mentioned ones but follows a different approach, i.e., like [14,15,16], exploits the presence of multiple firewalls within the protected network. In [14] a technique to balance workload by dynamically distributing rules among firewalls in a network is described. However, to increase the degrees of freedom in rule deployment, the technique relies on some unused IP header fields, written and checked by firewalls, allowing packets only to be filtered by a fraction of the firewalls they traverse. In [15], a solution for migrating rules from a central firewall to decentralized microfirewalls in cloud/cloudlets architectures is presented. However, to preserve the overall security policy implemented in the network, the solution requires a rearrangement of traffic paths after rule migration. Differently from [14] and [15], the technique described in this paper does not imply any modification to firewall or network behavior. The proposed solution resembles the one in [16], in that it allows to migrate (part of) the security policy originally implemented by a firewall to downstream ones in the protected network, preserving the overall network security policy. Solution in [16], however, relies on the go to action, which allows packets to jump among firewall rules instead of being checked against their conditions sequentially. This paper extends [16], as the proposed technique does not rely on the go to construct, and can thus be used in combination with policy analysis, rule ordering and compression algorithms, which are traditionally developed for security policies not including jumps.

Notation and problem definition

In this section, we define the notation used through the paper, which partially relies on the ones in [8,16], and formalize the tackled problem.

Firewalls and firewall sequences

We call range any non-empty, finite set of consecutive non-negative integers, [𝑎, 𝑏] ⊆ N 0 (with N 0 set of natural numbers including zero). Note that [𝑎, 𝑎] is range only consisting of 𝑎 ∈ N 0 . Firewalls operating a the IP layer filter packets based on the content of five header fields, i.e., source and destination IP address, source and destination port address and protocol number. Formally, a filtering field 𝑃 𝑖 is a range, and source and destination IP address, source and destination port address and protocol number are defined, respectively, as ranges

𝑃 1,2 = [0, 2 32 − 1], 𝑃 3,4 = [0, 2 16 − 1], and 𝑃 5 = [0, 2 8 − 1]

. Even if we focus on IP-layer firewalls, in the following, we refer to a generic number 𝑛 of filtering fields.

A packet 𝑝 defined over fields 𝑃 𝑖 , 𝑖 = 1, . . . , 𝑛, is a 𝑛-tuple

𝑝 = (𝑝 1 , 𝑝 2 , . . . , 𝑝 𝑛 ), 𝑝 𝑖 ∈ 𝑃 𝑖 , 𝑖 = 1, . . . , 𝑛(1)

A packet 𝑝 is a point in N 𝑛 0 , and the finite set of all possible packets defined over fields 𝑃 𝑖 , 𝑖 = 1, . . . , 𝑛, 𝒫 = 𝑃 1 × 𝑃 2 × . . . × 𝑃 𝑛 ⊆ N 𝑛 0 , is a hyperrectangle (the generalization of a rectangle in a 𝑛-dimensional space) in N 𝑛 0 . Note that, the Cartesian product of 𝑛 ranges is a set of 𝑛-tuple of integers, i.e., of packets defined over 𝑛 filtering fields.

A condition defined over fields 𝑃 𝑖 , 𝑖 = 1, . . . , 𝑛, is a 𝑛-tuple

𝑐 = (𝐶 1 , 𝐶 2 , . . . , 𝐶 𝑛 )(2)

where for 𝑖 = 1, . . . , 𝑛, 𝐶 𝑖 is a range such that 𝐶 𝑖 ⊆ 𝑃 𝑖 .

A rule 𝑟 over fields 𝑃 𝑖 , 𝑖 = 1, . . . , 𝑛, is defined as

𝑟 = ⟨𝑐, 𝑎𝑐𝑡𝑖𝑜𝑛⟩(3)

where 𝑐 is a condition over fields 𝑃 𝑖 , 𝑖 = 1, . .

where |𝑓 𝑤| is the firewall cardinality. The operation performed by a firewall acting according to the first matching strategy, consists in checking any incoming packet against its rule conditions, sequentially, until the matching rule is found. Then, the matching rule action is applied to the packet, that can be either forwarded (𝑎𝑙𝑙𝑜𝑤), or discarded (𝑑𝑒𝑛𝑦). A packet may match multiple, possibly conflicting (i.e., characterized by different actions), rules within a firewall (dependent rules), in this case the packet fate is determined by the rule order. Note that, we currently focus only on filtering operation, while we do not model other possible firewall functions, e.g., NAT (Network Address Translation).

A firewall 𝑓 𝑤 is said to be complete if any packet 𝑝 ∈ 𝒫 matches at least one rule in 𝑓 𝑤. We only consider complete firewalls and, to make sure of this, we assume a firewall last rule to be always 𝑟 |𝑓 𝑤| = ⟨(*, *, . . . , *), 𝑎𝑐𝑡𝑖𝑜𝑛⟩, matched by any packet 𝑝 ∈ 𝒫. Under the completeness hypothesis, any firewall 𝑓 𝑤 defines a filtering function 𝑓 𝑓 𝑤 : 𝒫 ∪ {−} → 𝒫 ∪ {−}, that maps any packet 𝑝 ∈ 𝒫 either in itself, if the packet is forwarded, or in −, the null packet, if it is discarded by 𝑓 𝑤. Note that, the domain of 𝑓 𝑓 𝑤 has been extended to the null packet, defining 𝑓 𝑓 𝑤 (−) = − for any firewall. Firewalls characterized by different rule lists may define the same filtering function. In particular, two firewalls 𝑓 𝑤 1 and 𝑓 𝑤 2 are said to be equivalent over 𝒫, or just equivalent (𝑓 𝑤 1 ≡ 𝑓 𝑤 2 ), if they equally map all packets, i.e., if ∀𝑝 ∈ 𝒫, 𝑓 𝑓 𝑤 1 (𝑝) = 𝑓 𝑓 𝑤 2 (𝑝).

A firewall sequence (see Fig. 1b) is a tuple of firewalls:

𝑓 𝑤𝑠 = (𝑓 𝑤 1 , 𝑓 𝑤 2 , . . . , 𝑓 𝑤 |𝑓 𝑤𝑠| )(5)

where the number of firewalls |𝑓 𝑤𝑠| is called sequence cardinality. The cumulative filtering operation performed by a firewall sequence (i.e., that defining whether a traversing packet is forwarded at the end of the sequence or discarded by one of the firewall within) can be equated to that of a single firewall. For this reason, analogously to single firewalls, any firewall sequence 𝑓 𝑤𝑠 defines a filtering function 𝑓 𝑓 𝑤𝑠 : 𝒫 ∪ {−} → 𝒫 ∪ {−}, which corresponds to the inverted order composition of the filtering functions defined by the firewalls of the sequence, i.e., which maps any packet

𝑝 ∈ 𝒫 in 𝑓 𝑓 𝑤 |𝑓 𝑤𝑠| ∘ . . . ∘ 𝑓 𝑓 𝑤 2 ∘ 𝑓 𝑓 𝑤 1 (𝑝).

The definitions of equivalence provided for single firewalls can then be extended to the firewall sequence domain, i.e., two firewall sequences 𝑓 𝑤𝑠 1 and 𝑓 𝑤𝑠 2 are said to be equivalent (𝑓

𝑤𝑠 1 ≡ 𝑓 𝑤𝑠 2 ) if ∀𝑝 ∈ 𝒫, 𝑓 𝑓 𝑤𝑠 1 (𝑝) = 𝑓 𝑓 𝑤𝑠 2 (𝑝).

Note that a single firewall can be seen as a firewall sequence with only one component. Moreover, as described in detail later, in general, a firewall sequence is not equivalent to a single firewall orderly listing the rules of all firewalls in the sequence.

f w r1 = (C r 1 1 , C r 1 2 , . . . , C r 1 n ), action r 1 r2 = (C r 2 1 , C r 2 2 , . . . , C r 2 n ), action r 2 . . . r |f w| = ( * , * , . . . , * ), action r |f w| (a) f w 1 f w 2 f w |f ws| . . . (b) f w 2 (c) f w 1 C1 C2 C3 C4 C5

Problem statement

We consider the problem of moving the security policy implemented by a firewall, so that it is implemented by a downstream firewall in the same sequence, without changing the overall security policy implemented by the sequence itself. Specifically, we focus on network configurations like the one in Fig. 1c, and consider the following problem:

Problem 1. Given a firewall sequence 𝑓 𝑤𝑠 = (𝑓 𝑤 1 , 𝑓 𝑤 2 ), where 𝑓 𝑤 𝑖 = (𝑟 𝑓 𝑤 𝑖 1 , 𝑟 𝑓 𝑤 𝑖 2 , . . . , 𝑟 𝑓 𝑤 𝑖 |𝑓 𝑤 𝑖 | ), 𝑖 = 1, 2, how to compute a firewall 𝑓 𝑤 2 such that sequence 𝑓 𝑤𝑠 = (𝑓 𝑤 1 , 𝑓 𝑤 2 )

, where 𝑓 𝑤 1 is the trivial firewall (i.e., the firewall that forwards every packet, 𝑓 𝑤 1 = (⟨(*, *, . . . , *), 𝑎𝑙𝑙𝑜𝑤⟩)), satisfies the following property:

𝑓 𝑤𝑠 ≡ 𝑓 𝑤𝑠(6)

Prob. 1 is a simplified version of the problem we are actually interested in, and allows for an easier technique description. I.e., the ultimate goal is to make 𝑓 𝑤 2 (and/or other firewalls within the protected network) responsible for implementing only part of the security policy originally implemented by 𝑓 𝑤 1 , to balance workload among available devices. Also, we are interested in realistic configurations, where firewalls are not connected in sequences but arbitrarily placed to guard specific network domains. Finally, Prob. 1 only considers downstream policy migration, where the overloaded firewall is the one firstly traversed by traffic. Although an upstream firewall is typically traversed by more packets and thus more likely to suffer from overloads, it is not always so. Situations described above are variations to Prob. 1, and can be solved by extending its solution, i.e., the significance of the proposed technique goes beyond Prob. 1.

Note that Prob. 1 is not trivial, e.g., defining 𝑓 𝑤 2 by moving rules in 𝑓 𝑤 1 to the top of 𝑓 𝑤 2 is not an admissible solution. Indeed, migrating 𝑎𝑙𝑙𝑜𝑤 rules, in general, makes (6) not satisfied. In 𝑓 𝑤𝑠, a packet matching an 𝑎𝑙𝑙𝑜𝑤 rule in 𝑓 𝑤 1 , is forwarded by the first firewall, but is still subjected to the filtering operation of (i.e., can still be dropped by) 𝑓 𝑤 2 . In 𝑓 𝑤𝑠, where 𝑓 𝑤 2 is defined by listing rules in 𝑓 𝑤 1 before those in 𝑓 𝑤 2 , the same packet is surely forwarded, as the trivial firewall 𝑓 𝑤 1 forwards every packet and the matching rule of the packet in 𝑓 𝑤 2 is the same migrated 𝑎𝑙𝑙𝑜𝑤 rule matched by the packet in 𝑓 𝑤 1 . Thus, the packet is not checked against rules originally in 𝑓 𝑤 2 , possibly violating (6).

Security policy migration technique

In this section, we describe the proposed technique to solve Prob. 1, and the algorithms defined to implement it.

A solution to Problem 1

The proposed security policy migration technique is based on the observation that a packet whose matching rule in 𝑓 𝑤 1 is a 𝑑𝑒𝑛𝑦 rule, independently of its matching rule in 𝑓 𝑤 2 , is dropped by 𝑓 𝑤𝑠 and, for (6) to hold, should be dropped by 𝑓 𝑤𝑠 as well. As a consequence, if we compute a set of 𝑑𝑒𝑛𝑦 rules, which discards all and only packets originally discarded by 𝑓 𝑤 1 , we can move list these rules before those in 𝑓 𝑤 2 to obtain 𝑓 𝑤 2 required by Prob. 1. Formally:

Theorem 1. Given Prob. 1, if a set of 𝑑𝑒𝑛𝑦 rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 satisfies property 𝑘 ⋃︁ 𝑗=1 𝒮 𝑟 𝑗 = 𝒟 𝑓 𝑤 1 = {𝑝 ∈ 𝒫 | 𝑓 𝑓 𝑤 1 (𝑝) = −}, (7)

where 𝒮 𝑟 𝑗 is packet set defined by rule 𝑟 𝑗 and 𝒟 𝑓 𝑤 1 is the set of packets discarded by 𝑓 𝑤 1 , then

𝑓 𝑤 2 = (𝑟 1 , . . . , 𝑟 𝑘 , 𝑟 𝑓 𝑤 2 1 , . . . , 𝑟 𝑓 𝑤 2 |𝑓 𝑤 2 | ) (8) is a solution to Prob. 1. (Proof of Thm. 1 is provided in App. A.1.)

Note that, in Thm. 1, we refer to a set of rules, instead of a list, as rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 all have the same action (𝑑𝑒𝑛𝑦) and thus their relative order in (8) does not matter.

We now address how to compute a set of 𝑑𝑒𝑛𝑦 rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 satisfying (7). By definition of firewall operation, 𝒟 𝑓 𝑤 1 consists of packets having as matching rule in 𝑓 𝑤 1 a 𝑑𝑒𝑛𝑦 rule, i.e.,

𝒟 𝑓 𝑤 1 = {𝑝 ∈ 𝒫 | ∃ ℓ ∈ 𝐿, 𝑝 ∈ 𝒮 𝑟 𝑓 𝑤 1 ℓ , ∀𝑚 ∈ 𝐼, 𝑚 < ℓ, 𝑝 / ∈ 𝒮 𝑟 𝑓 𝑤 1 𝑚 }(9)

where 𝐼 and 𝐿 are the sets of indexes, respectively, of all rules and 𝑑𝑒𝑛𝑦 rules in 𝑓 𝑤 1 . From (9), by applying generic set properties, 𝒟 𝑓 𝑤 1 can be expressed in term of packet sets defined by rules in 𝑓 𝑤 1 as (proof in App. A.2)

𝒟 𝑓 𝑤 1 = ⋃︁ ℓ∈𝐿 ⎛ ⎝ 𝒮 𝑟 𝑓 𝑤 1 ℓ ∖ ⎛ ⎝ ⋃︁ 𝑚∈𝑀,𝑚<ℓ 𝒮 𝑟 𝑓 𝑤 1 𝑚 ⎞ ⎠ ⎞ ⎠ (10) = ⋃︁ ℓ∈𝐿 (︂ (︁ . . . (︁(︁ 𝒮 𝑟 𝑓 𝑤 1 ℓ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 1 )︁ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 2 )︁ . . . )︁ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 |𝑀 ℓ | )︂(11)

where, 𝑀 = 𝐼 ∖ 𝐿 is the set of indexes of 𝑎𝑙𝑙𝑜𝑤 rules in 𝑓 𝑤 1 and, for each (11) as a union of sets, one for each 𝑑𝑒𝑛𝑦 rule 𝑟 𝑓 𝑤 1 ℓ , resulting from sequences of set subtractions, where the result of a subtraction is the minuend of the next one. We want to compute a set of 𝑑𝑒𝑛𝑦 rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 such that (7) holds for 𝒟 𝑓 𝑤 1 described by (11). Note that, while a packet set defined by a rule (or a union of packet sets defined by rules), can be directly translated into the rule (or set of rules) defining it, the set resulting from the subtraction between two packet set defined by rules (although can be always expressed as a union of hyperrectangles) is not necessarily a single hyperrectangle and cannot directly be translated into a rule set defining it. We thus define a rule subtraction operator, sub_rule(𝑟 𝑑 , 𝑟 𝑎 ), which allows to compute the set of rules defining a set expressed by a subtraction between two packet sets defined by rules. In general, Definition 1. A rule subtraction operator is any operator that given rules 𝑟 𝑑 and 𝑟 𝑎 , returns a, possibly empty, set ℛ of rules, with the same action as 𝑟 𝑑 , such that

ℓ ∈ 𝐿, 𝑀 ℓ = {𝑚 1 , 𝑚 2 , . . . , 𝑚 |𝑀 ℓ | } = {𝑚 ∈ 𝑀, 𝑚 < ℓ} is the set of indexes of 𝑎𝑙𝑙𝑜𝑤 rules preceding 𝑑𝑒𝑛𝑦 rule 𝑟 𝑓 𝑤 1 ℓ in 𝑓 𝑤 1 . Set 𝒟 𝑓 𝑤 1 is expressed in⋃︀ 𝑟∈ℛ 𝒮 𝑟 = 𝒮 𝑟 𝑑 ∖ 𝒮 𝑟𝑎 .

Once defined sub_rule(𝑟 𝑑 , 𝑟 𝑎 ), for each ℓ ∈ 𝐿, rule set ℛ

𝑚 |𝑀 ℓ | ℓ

defining the packet set resulting from the sequence of set subtractions from 𝒮 𝑟 𝑓 𝑤 1 ℓ in (11), can be iteratively computed as (proof in App. A.2):

ℛ 𝑚 0 ℓ = {𝑟 𝑓 𝑤 1 ℓ }, ℛ 𝑚𝑡 ℓ = ⋃︁ 𝑟∈ℛ 𝑚 𝑡−1 ℓ sub_rule(𝑟, 𝑟 𝑓 𝑤 1 𝑚𝑡 ) 𝑡 = 1, . . . , 𝑚 |𝑀 ℓ |(12)

Note that, in (11), for each ℓ ∈ 𝐿, only the first set subtraction in the sequence is among packet sets defined by rules and (as described in ( 12)) the set of rules defining it can be computed by using sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) once. The next set subtractions in the sequence require the execution of a rule subtraction for each rule resulting from the previous rule subtraction(s). Rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 satisfying (7) are then those in

⋃︀ ℓ∈𝐿 ℛ 𝑚 |𝑀 ℓ | ℓ

. As required by Thm. 1, they are all 𝑑𝑒𝑛𝑦 rules, as they result from sequences of rule subtractions from 𝑑𝑒𝑛𝑦 rules 𝑟 𝑓 𝑤 1 ℓ . Fig. 2 0 correspond to packets forwarded by 𝑓 𝑤 1 , while crossed grey ones to packets dropped by the firewall. Computing a set of 𝑑𝑒𝑛𝑦 rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 satisfying (7) means finding a set of rectangles covering all and only crossed grey points in Fig. 2, which, by (11), are those in set

𝒟 𝑓 𝑤 1 = 𝒮 𝑟 𝑓 𝑤 1 1 ∪ (︁(︁ 𝒮 𝑟 𝑓 𝑤 1 4 ∖ 𝒮 𝑟 𝑓 𝑤 1 2 )︁ ∖ 𝒮 𝑟 𝑓 𝑤 1 3

)︁ . The required set of 𝑑𝑒𝑛𝑦 rules can be computed as ℛ 0 1 ∪ ℛ as described in (12). In detail, Alg. 1 initializes a rule set ℛ 𝑚𝑖𝑛 to {𝑟 𝑓 𝑤 1 ℓ } (line 4), checks rules preceding 𝑟 𝑓 𝑤 1 ℓ (line 5), and any time finds an 𝑎𝑙𝑙𝑜𝑤 rule 𝑟 𝑓 𝑤 1 𝑚 (line 6), executes rule subtractions between each rule in ℛ 𝑚𝑖𝑛 and 𝑟 𝑓 𝑤 1 𝑚 (lines 8-10). Routine sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) (line 9) implements the defined rule subtraction operator, and is described in detail in Subsect. 4.2. Rules resulting from rule subtractions having 𝑟 𝑓 𝑤 1 𝑚 as subtrahend are stored in ℛ 𝑡𝑚𝑝 and, subsequently, copied back in ℛ 𝑚𝑖𝑛 to be the new minuend. Once the process is repeated for each 𝑎𝑙𝑙𝑜𝑤 rule

𝑟 𝑓 𝑤 1 𝑚 preceding 𝑟 𝑓 𝑤 1 ℓ , ℛ 𝑚𝑖𝑛 is equal to ℛ 𝑚 |𝑀 ℓ | ℓ

and Alg. 1 lists the rules it contains in 𝑓 𝑤 2 (line 14).

A rule subtraction operator

In this subsection, we describe the defined rule subtraction operator, sub_rule(𝑟 𝑑 , 𝑟 𝑎 ), implemented by Alg. property 𝐶∈𝒞 𝐶 = 𝐶 𝑑 ∖ 𝐶 𝑎 . The range subtraction operator is implemented by Alg. 2, which distinguishes between the four cases in Fig. 3: if ranges 𝐶 𝑑 and 𝐶 𝑎 are non overlapping (cases captured by line 5 or 9, shown in Fig. 3a), 𝒞 = {𝐶 𝑑 }, if 𝐶 𝑑 and 𝐶 𝑎 partially overlap (cases captured by line 4 or 8, shown in Fig. 3b), 𝒞 contains a single range, portion of 𝐶 𝑑 , if 𝐶 𝑎 ⊂ 𝐶 𝑑 (cases captured by both lines 4 and 8, shown in Fig. 3c), 𝒞 contains two ranges, portions of 𝐶 𝑑 , and, finally, if 𝐶 𝑑 ⊂ 𝐶 𝑎 (none of the above, Fig. 3d), 𝒞 = ∅.

Alg. 3 iteratively computes a set 𝒞 1 of conditions defined over 𝑛 filtering fields (lines 3-8), whose elements are used to compute rules of set ℛ (line 9). Set 𝒞 1 is initialized to sub_range(𝐶

𝑟 𝑑 1 , 𝐶 𝑟𝑎 1 )

and is then updated in 𝑛 − 1 steps (lines 5-8). At each step 𝑘 ∈ [2, 𝑛], 𝒞 1 is obtained as the union of two sets of conditions (line 6). The first set is recursively computed as the Cartesian product of current 𝒞 1 and set containing single range 𝐶 𝑟 𝑑 𝑘 (the result of the Cartesian product between sets of tuple of ranges is a set of tuple of ranges, i.e., of conditions). The second set is computed as the Cartesian product of set containing single condition (𝐶 𝑟 𝑑 1 ∩ 𝐶 𝑟𝑎 1 , . . . , 𝐶 𝑟 𝑑 𝑘−1 ∩ 𝐶 𝑟𝑎 𝑘−1 ), with set of ranges sub_range(𝐶 𝑟 𝑑 𝑛 , 𝐶 𝑟𝑎 𝑛 ). Fig. 4 shows examples of pairs of rules defined over 𝑛 = 2 filtering fields. Considering, e.g., case in Fig. 4c, 4,6], and 𝐶 𝑟𝑎 2 = [4,6]. Initially, Alg. 3 sets

𝐶 𝑟 𝑑 1 = [1, 8], 𝐶 𝑟 𝑑 2 = [2, 7], 𝐶 𝑟𝑎 1 = [𝒞 1 = sub_range(𝐶 𝑟 𝑑 1 , 𝐶 𝑟𝑎 1 ) = {[1, 3], [7, 8]} and 𝒞 2 = {𝐶 𝑟 𝑑 1 ∩ 𝐶 𝑟𝑎 1 } = {[4, 6

]}, at step 𝑘 = 2 (the only step since 𝑛 = 2), 𝒞 1 is computed as the union of two sets of conditions. The first is [2,7]), ( [7,8], [2,7])}, the second is 𝒞 2 × sub_range(𝐶 [7,7])} = {( [4,6], [2,3]), ([4, 6], [7,7])}. Then 𝒞 1 := {( [1,3], [2,7]), ( [7,8], [2,7]), ([4, 6], [2,3]), ([4, 6], [7,7])}, from which, since 𝑟 𝑑 is a 𝑑𝑒𝑛𝑦 rule, ℛ = {𝑟 1 = ⟨( [1,3], [2,7]), 𝑑𝑒𝑛𝑦⟩, 𝑟 2 = ⟨( [7,8], [2,7]), 𝑑𝑒𝑛𝑦⟩, 𝑟 3 = ⟨( [4,6], [2,3]), 𝑑𝑒𝑛𝑦⟩, 𝑟 4 = ⟨( [4,6], [7,7]), 𝑑𝑒𝑛𝑦⟩}.

𝒞 1 × 𝐶 𝑟 𝑑 2 = {[1, 3], [7, 8]} × {[2, 7]} = {([1, 3],𝑟 𝑑 2 , 𝐶 𝑟𝑎 2 ) = {[4, 6]} × sub_range([2, 7], [4, 6]) = {[4, 6]} × {[2, 3],

In Fig. 4, rules returned by sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) are listed in the bottom part of tables and shown in red in the plots. The number |ℛ| of resulting rules depends on 𝑟 𝑑 and 𝑟 𝑎 . In particular, when 𝑟 𝑑 and 𝑟 𝑎 are independent, i.e., 𝒮 𝑟 𝑑 and 𝒮 𝑟𝑎 are disjoint (e.g., Fig. 4a), the result is a single rule equal to 𝑟 𝑑 , if 𝑟 𝑑 and 𝑟 𝑎 are dependent and the corresponding rectangles partially overlap (e.g., Fig. 4b), |ℛ| ∈ [1,3], if 𝑆 𝑟𝑎 ⊂ 𝑆 𝑟 𝑑 (e.g., Fig. 4c), |ℛ| = 4, and, finally if 𝑟 𝑑 is shadowed by 𝑟 𝑎 , i.e., 𝑆 𝑟 𝑑 ⊂ 𝑆 𝑟𝑎 (e.g., Fig. 4d), there are no resulting rules, i.e., |ℛ| = 0. In Figs. 4b and 4c, rules returned by sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) are not contiguous as conditions are defined as tuple of ranges including their extremes and sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) returns independent rules. Other rule subtraction operators can be defined, however sub_rule(𝑟 𝑑 , 𝑟 𝑎 ) guarantees that the number of resulting rules, |ℛ|, is kept to the minimum.

Fig 5 shows result obtained when security policy migration, implemented by Alg. 1, is applied to example in Fig. 1c. As can be seen, 𝑓 𝑤 1 is the trivial firewall, while 𝑓 𝑤 2 has been obtained by placing 12 𝑑𝑒𝑛𝑦 rules before those originally in 𝑓 𝑤 2 . Actually, 𝑑𝑒𝑛𝑦 rules at the top of 𝑓 𝑤 2 are the result of a further optimization, as often subsets of rules returned by Alg. 3 can be unified in single rules. As a first observation, expressing the security policy implemented by 𝑓 𝑤 1 with only 𝑑𝑒𝑛𝑦 rules, requires a higher number of rules, which penalizes the cooperating firewall. One way to mitigate this effect is to use compression algorithms on 𝑓 𝑤 2 . As a second observation, the proposed technique can be, in principle, used to move only part of the security policy implemented by 𝑓 𝑤 1 , as by migrating any subset of 𝑑𝑒𝑛𝑦 rules 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑘 to 𝑓 𝑤 2 , ( 7) is still satisfied. However, from the performance point of view, a better solution would be to split Algorithm 2: Algorithm for range subtraction. the security policy of 𝑓 𝑤 1 before translating it into 𝑑𝑒𝑛𝑦 rules, so as to minimize the number of rules added to 𝑓 𝑤 2 . This can be done by suitably partitioning 𝒫 and, accordingly, rules in 𝑓 𝑤 1 [16], so that a new firewall ̂︁ 𝑓 𝑤 1 is given as a input to Alg. 3. The same approach, as detailed in [16], allows to extend the technique to the case of more complex topologies, where firewalls are arbitrarily placed to guard specific domains. Note that, in this case, additional constraints deriving from network topology should be considered in security policy migration.

Data: 𝐶 𝑑 = [𝑎 𝑑 , 𝑏 𝑑 ], 𝐶𝑎 = [𝑎𝑎, 𝑏𝑎], 𝐶 𝑑 , 𝐶𝑎 ⊆ N0. Result: A set of ranges 𝒞, |𝒞| ∈ [0, 2]. 1 Function sub_range(𝐶 𝑑 ,𝐶𝑎): 2 𝒞 ← ∅; /* initialization */ 3 if (𝑎𝑎 > 𝑎 𝑑 ) then 4 if (𝑎𝑎 ≤ 𝑏 𝑑 ) then 𝒞 ← 𝒞 ∪ {[𝑎 𝑑 , 𝑎𝑎 − 1]} ; 5 else 𝒞 ← 𝒞 ∪ {[𝑎 𝑑 , 𝑏 𝑑 ]} ; 6 end 7 if (𝑏𝑎 < 𝑏 𝑑 ) then 8 if (𝑏𝑎 ≥ 𝑎 𝑑 ) then 𝒞 ← 𝒞 ∪ {[𝑏𝑎 + 1, 𝑏 𝑑 ]} ; 9 else 𝒞 ← 𝒞 ∪ {[𝑎 𝑑 , 𝑏 𝑑 ]} ;

Conclusions

We presented a technique for migrating security policies along firewalls in a sequence, which is formally verified to preserve the overall security policy implemented by the sequence itself. The proposed technique can be extended to the case of more general topologies comprising firewallprotected domains and is the building block for the development of cooperative solutions balancing workload by distributing filtering responsibility among firewalls available within a protected network. Future work will analyze solutions to compress rule lists obtained after migration in the cooperating firewall, as the proposed technique may lead to rule proliferation. Techniques for suitably partitioning the packet space will also be investigated to split policies based on network/workload characteristics and further optimize network performance.

A. Appendix𝒟 𝑓 𝑤 1 = ⋃︁ ℓ∈𝐿 ⎛ ⎝ 𝒮 𝑟 𝑓 𝑤 1 ℓ ∖ ⎛ ⎝ ⋃︁ 𝑚∈𝑀,𝑚<ℓ 𝒮 𝑟 𝑓 𝑤 1 𝑚 ⎞ ⎠ ⎞ ⎠ (13)

where 𝐿, and 𝑀 are, respectively, is the set of indexes of 𝑑𝑒𝑛𝑦 and 𝑎𝑙𝑙𝑜𝑤 rules in 𝑓 𝑤 1 .

Proof. By definition of firewall operation, 𝒟 𝑓 𝑤 1 is the set of packets having as a matching rule in 𝑓 𝑤 1 a 𝑑𝑒𝑛𝑦 rule, i.e.,

𝒟 1 = {𝑝 ∈ 𝒫 | ∃ ℓ ∈ 𝐿, 𝑝 ∈ 𝒮 𝑟 𝑓 𝑤 1 ℓ , ∀𝑚 ∈ 𝐼, 𝑚 < ℓ, 𝑝 / ∈ 𝒮 𝑟 𝑓 𝑤 1 𝑚 } = ⋃︁ ℓ∈𝐿 ⎛ ⎝ 𝒮 𝑟 𝑓 𝑤 1 ℓ ∖ ⎛ ⎝ ⋃︁ 𝑚∈𝐼,𝑚<ℓ 𝒮 𝑟 𝑓 𝑤 1 𝑚 ⎞ ⎠ ⎞ ⎠(14)

where 𝐼 = 𝐿∪𝑀 is the set of indexes of all rules in 𝑓 𝑤

𝒮 𝑟 𝑓 𝑤 1 𝑚 ⎞ ⎠ ⎞ ⎠(15)

since 𝐼 ∖ 𝐿 = 𝑀 , equality (15) proves the thesis. □

We consider a packet set 𝒟 𝑓 𝑤 1 defined by Proof. Firstly, we prove that 𝒮 𝑟 𝑑 ∖ 𝒮 𝑟𝑎 can be expressed in terms of a union of hyperrectangles, that can be translated in a set ℛ of rules. Then we show that Alg. 3 computes ℛ this way. Given a rule 𝑟 = ⟨(𝐶 1 , 𝐶 2 , . . . , 𝐶 𝑛 ), 𝑎𝑐𝑡𝑖𝑜𝑛⟩, the set of packets matching the rule is 𝒮 𝑟 = 𝐶 1 × 𝐶 2 × . . . × 𝐶 𝑛 ⊆ 𝒫. Note that, any packet set that can be expressed as the Cartesian product of 𝑛 ranges can be defined by a rule having as a condition the 𝑛-tuple of ranges. We

𝒟 𝑓 𝑤 1 = ⋃︁ ℓ∈𝐿 (︂ (︁ . . . (︁(︁ 𝒮 𝑟 𝑓 𝑤 1 ℓ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 1 )︁ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 2 )︁ . . . )︁ ∖ 𝒮 𝑟 𝑓 𝑤 1 𝑚 |𝑀 ℓ | )︂(