=Paper=
{{Paper
|id=Vol-2940/paper29
|storemode=property
|title=An Algorithm for Security Policy Migration in Multiple Firewall Networks
|pdfUrl=https://ceur-ws.org/Vol-2940/paper29.pdf
|volume=Vol-2940
|authors=Manuel Cheminod,Luca Durante,Lucia Seno,Adriano Valenzano,Mario Ciampi,Fabrizio Marangio,Giovanni Schmid,Mario Sicuranza,Marco Zuppelli,Giuseppe Manco,Luca Caviglione,Massimo Guarascio,Marzio Di Feo,Simone Raponi,Maurantonio Caprolu,Roberto Di Pietro,Paolo Spagnoletti,Federica Ceci,Andrea Salvi,Vincenzo Carletti,Antonio Greco,Alessia Saggese,Mario Vento,Gabriele Costa,Enrico Russo,Andrea Valenza,Giuseppe Amato,Simone Ciccarone,Pasquale Digregorio,Giuseppe Natalucci,Giovanni Lagorio,Marina Ribaudo,Alessandro Armando,Francesco Benvenuto,Francesco Palmarini,Riccardo Focardi,Flaminia Luccio,Edoardo Di Paolo,Enrico Bassetti,Angelo Spognardi,Anna Pagnacco,Vita Santa Barletta,Paolo Buono,Danilo Caivano,Giovanni Dimauro,Antonio Pontrelli,Chinmay Siwach,Gabriele Costa,Rocco De Nicola,Carmelo Ardito,Yashar Deldjoo,Eugenio Di Sciascio,Fatemeh Nazary,Vishnu Ramesh,Sara Abraham,Vinod P,Isham Mohamed,Corrado A. Visaggio,Sonia Laudanna
|dblpUrl=https://dblp.org/rec/conf/itasec/CheminodDSV21
}}
==An Algorithm for Security Policy Migration in Multiple Firewall Networks==
https://ceur-ws.org/Vol-2940/paper29.pdf
An algorithm for security policy migration in
multiple firewall networks
Manuel Cheminod, Luca Durante, Lucia Seno and Adriano Valenzano
National Research Council of Italy, CNR-IEIIT, C.so Duca degli Abruzzi 24, 10129 Torino, Italy
Abstract
Firewalls are effectively employed to protect network portions by blocking illegitimate traversing traf-
fic. However, during traffic load peaks, possibly due to DoS-like attacks, they may become performance
bottlenecks, introducing consistent delays/losses on legitimate packets. In multiple firewall networks,
a cooperative approach to mitigate performance degradation caused by firewall overloads consists in
suitably distributing responsibility for security policy implementation among available devices to bal-
ance workload. We present a technique for migrating security policies among firewalls in a sequence,
formally verified to preserve the overall security policy implemented by the sequence itself. The tech-
nique can be used as building block in the development of cooperative solutions allowing to balance
workload in networks where firewalls are arbitrarily placed to guard specific domains.
Keywords
Firewalls, Network security, Policy migration, Formal methods
1. Introduction
Nowadays firewalls are pervasively deployed over the Internet to protect network portions
(or single devices) against undesired/malicious traffic possibly threatening confidentiality, in-
tegrity 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].
ITASEC 2021, Italian Conference on CyberSecurity, April 07-09, 2021
" manuel.cheminod@ieiit.cnr.it (M. Cheminod); luca.durante@ieiit.cnr.it (L. Durante); lucia.seno@ieiit.cnr.it
(L. Seno); adriano.valenzano@ieiit.cnr.it (A. Valenzano)
ยฉ 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
This paper presents a technique which may be used as a building block towards the de-
velopment of a cooperative solution, mitigating network performance degradation caused by
firewalls during traffic load peaks (either naturally arising or caused by cyber-attacks). The
idea is, when a firewall is overloaded, to split the security policy it implements so that part of
it is cooperatively implemented by other, less loaded, firewalls within the protected network.
Reducing the cardinality of the overloaded firewall, at the expense of that of the cooperating
ones, allows to balance the workload among the available devices. The presented technique
allows to migrate security policies along firewalls in a sequence, without altering the overall
security policy implemented by the sequence itself, by translating them in lists of only ๐๐๐๐ฆ
rules. The technique can be extended to more general configurations, where firewalls are not
connected in sequences but arbitrarily placed to guard specific network domains. Note that,
security administrators are only supposed to act (maintain/modify) on firewall configurations
in their original form, while the proposed technique operates independently, ensuring that the
overall network security policy is not changed in any way.
The paper is organized as follows: Sect. 2 provides an overview of state of the art techniques
for firewall performance optimization, Sect. 3 formalizes notation and considered problem,
while Sect. 4 describes the proposed technique for security policy migration. Sect. 5 concludes
the paper and, finally, App. A collects proofs.
2. 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 micro-
firewalls 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.
3. 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.
3.1. Firewalls and firewall sequences
We call range any non-empty, finite set of consecutive non-negative integers, [๐, ๐] โ N0
(with N0 set of natural numbers including zero). Note that [๐, ๐] is range only consisting
of ๐ โ N0 . 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, 232 โ 1], ๐3,4 = [0, 216 โ 1], and ๐5 = [0, 28 โ 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, . . . , ๐ and ๐๐๐ก๐๐๐ varies in the set of all possible
firewall actions, i.e., ๐๐๐ก๐๐๐ โ {๐๐๐๐๐ค, ๐๐๐๐ฆ}. From now on, we assume all packets, conditions
and rules to be defined over the same filtering fields ๐๐ , ๐ = 1, . . . , ๐. We use symbol * as
a possible value for condition components, i.e., ๐ถ๐ = * means ๐ถ๐ = ๐๐ , and the traditional
dotted decimal notation for single or ranges of IP addresses. Note, however, that statements like
192.168. * .1 do not define single ranges and are not admissible values for condition components.
A packet ๐ = (๐1 , ๐2 , . . . , ๐๐ ) is said to match a rule ๐ = โจ(๐ถ1 , ๐ถ2 , . . . , ๐ถ๐ ), ๐๐๐ก๐๐๐โฉ if and
only if ๐๐ โ ๐ถ๐ , ๐ = 1, . . . , ๐, i.e., ๐๐ โ ๐ฎ๐ = ๐ถ1 ร ๐ถ2 ร . . . ร ๐ถ๐ โ ๐ซ. Packet set ๐ฎ๐ , defined
by rule ๐, is also a hyperrectangle in N๐0 .
A firewall ๐ ๐ค (see Fig. 1a, where, as in other examples in the paper, condition/action-rule
correspondence has been made explicit through superscripts) is a tuple of rules
๐ ๐ค = (๐1 , ๐2 , . . . , ๐|๐ ๐ค| ) (4)
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.
r1 = h(C1r1 , C2r1 , . . . , Cnr1
), actionr1 i
r2 = h(C1r2 , C2r2 , . . . , Cnr2
), actionr2 i
(a) fw .. (b) f w1 f w2 ... f w|f ws|
.
r|f w| = h(โ, โ, . . . , โ), actionr|f w| i
(c) f w1 f w2
C1 C2 C3 C4 C5 action C1 C2 C3 C4 C5 action
r1 * 192.168.2.1-50 * 22 TCP allow r1 * 192.168.2.40 * 80 TCP allow
r2 * 192.168.2.1-50 * 80 TCP allow r2 * 192.168.2.35-45 * 80 TCP deny
r3 * 192.168.2.1-50 * * TCP deny r3 * * * * * deny
r4 * 192.168.3.1-50 * 20-23 TCP allow
r5 * * * * * deny
Figure 1: Examples of firewalls and firewall sequences.
3.2. 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).
4. Security policy migration technique
In this section, we describe the proposed technique to solve Prob. 1, and the algorithms defined
to implement it.
4.1. 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 (๐) = โ}, (7)
๐=1
where ๐ฎ๐๐ is packet set defined by rule ๐๐ and ๐๐ ๐ค1 is the set of packets discarded by ๐ ๐ค1 , then
๐ ๐ค2
๐ ๐ค2 = (๐1 , . . . , ๐๐ , ๐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
P2
Srf w1 = P r1f w1 = h([1, 5], [4, 6]), denyi
8 4
r2f w1 = h([2, 4], [5, 8]), allowi
Srf w1 f w1 r3f w1 = h([5, 7], [1, 3]), allowi
2
6 r4f w1 = h([0, 9], [0, 9]), denyi
Srf w1
1
4
allow
Srf w1
3
2
deny
0 2 4 6 8 P1
Figure 2: Hint on security policy migration for ๐ = 2.
rules in ๐ ๐ค1 as (proof in App. A.2)
โ โ โโ
โ๏ธ โ๏ธ
๐๐ ๐ค1 = โ๐ฎ ๐ ๐ค1 โ โ
๐
๐ฎ๐๐ ๐ค1 โ โ (10)
โ ๐
โโ๐ฟ ๐โ๐,๐<โ
โ๏ธ (๏ธ(๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ )๏ธ
= ... ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 (11)
โ ๐1 ๐2 ๐|๐ |
โโ๐ฟ โ
where, ๐ = ๐ผ โ ๐ฟ is the set of indexes of ๐๐๐๐๐ค rules in ๐ ๐ค1 and, for each โ โ ๐ฟ, ๐โ =
{๐1 , ๐2 , . . . , ๐|๐โ | } = {๐ โ ๐, ๐ < โ} is the set of indexes of ๐๐๐๐๐ค rules preceding ๐๐๐๐ฆ
rule ๐โ๐ ๐ค1 in ๐ ๐ค1 . Set ๐๐ ๐ค1 is expressed in (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 ๐โโ ๐ฎ๐ = ๐ฎ๐๐ โ ๐ฎ๐๐ .
๐|๐ |
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):
๐ ๐ค1
โ๏ธ
โ๐
โ = {๐โ
0
}, โ๐๐ก
โ =
๐ ๐ค1
sub_rule(๐, ๐๐ ๐ก
) ๐ก = 1, . . . , ๐|๐โ | (12)
๐
๐โโโ ๐กโ1
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 shows a simple clarifying example. Rectangles in the figure correspond to rules ๐๐๐ ๐ค1 ,
๐ = 1, . . . , 4, defined over ๐ = 2 filtering fields ๐๐ = [0, 9], ๐ = 1, 2 and listed in firewall
๐ ๐ค1 . The filtering function defined by ๐ ๐ค1 , ๐๐ ๐ค1 , is represented in Fig. 2 through symbols
and colors: dotted white points of N20 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 โ ๐ฎ๐๐ ๐ค1 . The required
1 4 2 3
set of ๐๐๐๐ฆ rules can be computed as โ01 โช โ34 , where, based on (12), โ01 = {๐1๐ ๐ค1 } and
โ34 = ๐โโ2 sub_rule(๐, ๐3๐ ๐ค1 ), with โ24 = sub_rule(๐4๐ ๐ค1 , ๐2๐ ๐ค1 ).
โ๏ธ
4
Alg. 1, implements the described procedure. The algorithm takes as inputs firewalls ๐ ๐ค๐ =
(๐1๐ ๐ค๐ , ๐2๐ ๐ค๐ , . . . , ๐|๐
๐ ๐ค๐
๐ค๐ | ), ๐ = 1, 2, and returns ๐ ๐ค 2 , solution to Prob. 1, by computing ๐๐๐๐ฆ
rules ๐1 , ๐2 , . . . , ๐๐ satisfying (7) and listing them, before rules in ๐ ๐ค2 , in ๐ ๐ค2 , as in (8). Alg.
1 sequentially checks rules in ๐ ๐ค1 (line 2), and any time it finds a ๐๐๐๐ฆ rule ๐โ๐ ๐ค1 (line 3),
๐|๐ |
computes rule set ๐
โ โ 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
๐ ๐ค1
(line 6), executes rule subtractions between each rule in โ๐๐๐ and ๐๐ (lines 8-10). Routine
sub_rule(๐๐ , ๐๐ ) (line 9) implements the defined rule subtraction operator, and is described
๐ ๐ค1
in detail in Subsect. 4.2. Rules resulting from rule subtractions having ๐๐ as subtrahend
are stored in โ๐ก๐๐ and, subsequently, copied back in โ๐๐๐ to be the new minuend. Once the
๐ ๐ค1 ๐|๐ |
process is repeated for each ๐๐๐๐๐ค rule ๐๐ preceding ๐โ๐ ๐ค1 , โ๐๐๐ is equal to โโ โ and Alg.
1 lists the rules it contains in ๐ ๐ค2 (line 14).
4.2. A rule subtraction operator
In this subsection, we describe the defined rule subtraction operator, sub_rule(๐๐ , ๐๐ ), imple-
mented by Alg. 3, employed by Alg. 1. Alg. 3 takes as inputs rules ๐๐ = โจ(๐ถ1๐๐ , ๐ถ2๐๐ , . . . , ๐ถ๐๐๐ ),
๐๐๐ก๐๐๐๐๐ โฉ and ๐๐ = โจ(๐ถ1๐๐ , ๐ถ2๐๐ , . . . , ๐ถ๐๐โ๏ธ
๐ ), ๐๐๐ก๐๐๐๐๐ โฉ, and returns a set โ, |โ| โ [0, 2๐], of rules
with the same action as ๐๐ , such that ๐โโ ๐ฎ๐ = ๐ฎ๐๐ โ ๐ฎ๐๐ (proof in App. A.3). Alg. 3 relies
on the range subtraction operator, sub_range(๐ถ๐ , ๐ถ๐ ), which, given two ranges ๐ถ๐ = [๐๐ , ๐๐ ]
and ๐ถ๐ = [๐๐ , ๐๐ ], returns the set of ranges ๐, of minimal cardinality |๐| โ [0, 2], satisfying
Algorithm 1: Security policy migration algorithm
Data: ๐ ๐ค1 = (๐1๐ ๐ค1 , ๐2๐ ๐ค1 , . . . , ๐|๐
๐ ๐ค1 ๐ ๐ค2
๐ค1 | ) ๐ ๐ค2 = (๐1 , ๐2๐ ๐ค2 , . . . , ๐|๐
๐ ๐ค2
๐ค2 | )
๐ ๐ค2 ๐ ๐ค2 ๐๐ค
Result: ๐ ๐ค2 = (๐1 , ๐2 , . . . , ๐|๐ ๐ค2 | )
2
1 ๐ ๐ค2 โ โ ; /* initialization, firewall with no rules */
2 for (โ = 1; โ โค |๐ ๐ค1 |; โ + +) do
3 if (๐โ๐ ๐ค1 is a ๐๐๐๐ฆ rule) then
4 โ๐๐๐ โ {๐โ๐ ๐ค1 };
5 for (๐ = 1; ๐ < โ; ๐ + +) do
6 if (๐๐๐ ๐ค1
is an ๐๐๐๐๐ค rule) then
7 โ๐ก๐๐ โ โ
;
8 forall ๐ โ โ๐๐๐ do
๐ ๐ค1
9 โ๐ก๐๐ โ โ๐ก๐๐ โช sub_rule(๐, ๐๐ );
10 end
11 โ๐๐๐ โ โ๐ก๐๐ ;
12 end
13 end
14 append all ๐ โ โ๐๐๐ to ๐ ๐ค2 in any order;
15 end
16 end
17 append rules in ๐ ๐ค2 to ๐ ๐ค 2 ;
aa Ca ba aa Ca ba
ad Cd bd ad Cd bd aa Ca ba aa Ca ba
aa Ca ba aa Ca ba ad Cd bd ad Cd bd
ad Cd bd ad Cd bd
(a) (b) (c) (d)
Figure 3: Range subtraction.
P2
P2
8
C1 C2 action 8 C1 C2 action
ra [9,11] [1,3] allow ra [7,9] [1,3] allow
6 rd [1,8] [2,7] deny rd [1,8] [2,7] deny
6
r1 [1,8] [2,7] deny r1 [1,6] [2,7] deny
r2 [7,8] [4,7] deny
4
4
2 2
P1 P1
0 2 4 6 8 10 0 2 4 6 8 10
(a) Resulting rule is ๐1 = ๐๐ . (b) Two resulting rules.
P2 P2
8 8
C1 C2 action C1 C2 action
ra [4,6] [4,6] allow ra [1,8] [2,7] allow
6 rd [1,8] [2,7] deny 6 rd [5,7] [4,6] deny
r1 [1,3] [2,7] deny
r2 [7,8] [2,7] deny
4 4
r3 [4,6] [2,3] deny
r4 [4,6] [7,7] deny
2 2
P1 P1
0 2 4 6 8 10 0 2 4 6 8 10
(c) Four resulting rules. (d) No resulting rules.
Figure 4: Examples of rule subtraction for ๐ = 2.
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 com-
puted 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, ๐ถ1๐๐ = [1, 8], ๐ถ2๐๐ = [2, 7], ๐ถ1๐๐ = [4, 6], and ๐ถ2๐๐ = [4, 6]. Initially, Alg. 3 sets
๐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 ๐1 ร ๐ถ2๐๐ = {[1, 3], [7, 8]} ร {[2, 7]} = {([1, 3], [2, 7]), ([7, 8], [2, 7])}, the second is ๐2 ร
๐ ๐
sub_range(๐ถ2 ๐ , ๐ถ2 ๐ ) = {[4, 6]} ร sub_range([2, 7], [4, 6]) = {[4, 6]} ร {[2, 3], [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]), ๐๐๐๐ฆโฉ}.
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.
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 ๐ โ ๐ โช {[๐๐ , ๐๐ ]} ;
10 end
11 return ๐
Algorithm 3: Algorithm for rule subtraction in N๐0 .
๐ ๐ ๐
Data: ๐๐ = โจ(๐ถ1 ๐ , ๐ถ2 ๐ , . . . , ๐ถ๐๐ ), ๐๐๐ก๐๐๐๐๐ โฉ, ๐๐ = โจ(๐ถ1๐๐ , ๐ถ2๐๐ , . . . , ๐ถ๐๐๐ ), ๐๐๐ก๐๐๐๐๐ โฉ
Result: A set โ of rules with the same action as ๐๐ , |โ| โ [0, 2๐].
1 Function sub_rule(๐๐ ,๐๐ ):
2 โ โ โ
; /* initialization */
๐
3 ๐1 โ sub_range(๐ถ1 ๐ , ๐ถ1๐๐ );
๐
4 ๐2 โ {๐ถ1 ๐ โฉ ๐ถ1๐๐ }; /* the intersection of two ranges is always a single range */
5 for (๐ = 2; ๐ โค ๐; ๐ + +) do
๐ ๐
6 ๐1 โ (๐1 ร {๐ถ๐๐ }) โช (๐2 ร sub_range(๐ถ๐๐ , ๐ถ๐๐๐ ));
๐
7 ๐2 โ ๐2 ร {๐ถ๐๐ โฉ ๐ถ๐๐๐ };
8 end
9 forall ๐ โ ๐1 do โ โ โ โช {๐ = โจ๐, ๐๐๐ก๐๐๐๐๐ โฉ} ;
10 return โ
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.
f w1 f w2
C1 C2 C3 C4 C5 action
r1 * * * * * allow
C1 C2 C3 C4 C5 action C1 C2 C3 C4 C5 action
r1 * 192.168.3.1-50 * 0-19 * deny r9 * 0.0.0.0-192.168.2.0 * * * deny
r2 * 192.168.2.1-50 * 0-21 6-6 deny r10 * 192.168.2.51-3.0 * * * deny
r3 * 192.168.3.1-50 * 20-23 0-5 deny r11 * 192.168.3.51-255.255.255.255 * * * deny
r4 * 192.168.3.1-50 * 20-23 7-255 deny r12 * 192.168.3.1-50 * 24-65535 * deny
r5 * 192.168.2.1-50 * * 0-5 deny r13 * 192.168.2.40 * 80 6-6 allow
r6 * 192.168.2.1-50 * * 7-255 deny r14 * 192.168.2.35-45 * 80 6-6 deny
r7 * 192.168.2.1-50 * 23-79 6-6 deny r15 * * * * * deny
r8 * 192.168.2.1-50 * 81-65535 6-6 deny
Figure 5: Sequence ๐ ๐ค๐ obtained from example in Fig. 1c after security policy migration.
5. 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 firewall-
protected 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.
6. Acknowledgments
This work was supported in part by the EU H2020-SU-ICT-03-2018 Project No. 830929 Cyber-
Sec4Europe (cybersec4europe.eu).
References
[1] M. Cheminod, L. Durante, L. Seno, A. Valenzano, Performance evaluation and modeling of
an industrial application-layer firewall, IEEE Trans. Ind. Informat. 14 (2018) 2159โ2170.
[2] K. Salah, K. Elbadawi, R. Boutaba, Performance modeling and analysis of network firewalls,
IEEE Trans. Netw. Service Manag. 9 (2012) 12โ21.
[3] K. Salah, K. Sattar, Z. Baig, M. Sqalli, P. Calyam, Resiliency of open-source firewalls against
remote discovery of last-matching rules, in: Proc. Int. Conf. on Security of Information
and Networks (SIN), 2009, p. 186โ192.
[4] C. Bodei, L. Ceragioli, P. Degano, R. Focardi, L. Galletta, F. Luccio, M. Tempesta, L. Veronese,
FWS: Analyzing, maintaining and transcompiling firewalls, J. Comp. Sec. 29 (2021) 77โ134.
[5] A. A. Jabal, M. Davari, E. Bertino, C. Makaya, S. Calo, D. Verma, A. Russo, C. Williams,
Methods and tools for policy analysis, ACM Comput. Surv. 51 (2019).
[6] F. Valenza, S. Spinoso, C. Basile, R. Sisto, A. Lioy, A formal model of network policy
analysis, in: Proc. IEEE Int. Forum on Research and Technologies for Society and Industry
Leveraging a better tomorrow (RTSI), 2015, pp. 516โ522.
[7] E. Al-Shaer, H. Hamed, R. Boutaba, M. Z. Hasan, Conflict Classification and Analysis of
Distributed Firewall Policies, IEEE J. Sel. Areas Commun. 23 (2005) 2069โ2084.
[8] A. X. Liu, E. Torng, C. R. Meiners, Firewall Compressor: An Algorithm for Minimizing
Firewall Policies, in: Proc. IEEE Conf. on Comp. Comm. (INFOCOM), 2008, pp. 176โ180.
[9] Y. Cheng, W. Wang, J. Wang, H. Wang, FPC: A new approach to firewall policies compres-
sion, Tsinghua Science and Technology 24 (2019) 65โ76.
[10] E. W. Fulp, Optimization of network firewall policies using ordered sets and directed
acyclical graphs, in: Proc. of IEEE Internet Management Conference, 2005, pp. 1โ4.
[11] H. Hamed, E. Al-Shaer, Dynamic rule-ordering optimization for high-speed firewall
filtering, in: Proc. ACM Symp. on Inf. Comp. and Comm. Sec. (ASIACCS), 2006, p. 332โ342.
[12] R. Mohan, A. Yazidi, B. Feng, J. Oommen, On optimizing firewall performance in dynamic
networks by invoking a novel swapping windowโbased paradigm, Int. J. Commun. Syst.
31 (2018) e3773.
[13] T. Harada, K. Tanaka, K. Mikawa, A heuristic algorithm for relaxed optimal rule ordering
problem, in: Proc. of Cyber Security in Networking Conference (CSNet), 2018, pp. 1โ8.
[14] G. Yan, S. Chen, S. Eidenbenz, Dynamic balancing of packet filtering workloads on
distributed firewalls, in: Proc. of IEEE Int. Workshop on QoS (IWQoS), 2008, pp. 209โ218.
[15] S. Bagheri, A. Shameli-Sendi, Dynamic firewall decomposition and composition in the
cloud, IEEE Trans. Inf. Forensics Security 15 (2020) 3526โ3539.
[16] L. Durante, L. Seno, A. Valenzano, A formal model and technique to redistribute the packet
filtering load in multiple firewall networks, IEEE Trans. Inf. Forensics Security 16 (2021)
2637โ2651.
A. Appendix
A.1. Proof of Thm. 1
Given ๐ ๐ค๐ = (๐ ๐ค1 , ๐ ๐ค2 ), ๐ ๐ค๐ = (๐1๐ ๐ค๐ , ๐2๐ ๐ค๐ , . . . , ๐|๐
๐ ๐ค๐
๐ค๐ | ), ๐ = 1, 2, and ๐ ๐ค๐ = (๐ ๐ค 1 , ๐ ๐ค 2 ),
๐ ๐ค2
where ๐ ๐ค1 = (โจ(*, *, . . . , *), ๐๐๐๐๐คโฉ) and ๐ ๐ค2 = (๐1 , . . . , ๐๐ , ๐1๐ ๐ค2 , . . . , ๐|๐ ๐ค2 | ), if ๐1 , . . . , ๐๐
โ๏ธ๐
are ๐๐๐๐ฆ rules such that ๐=1 ๐ฎ๐๐ = ๐๐ ๐ค1 = {๐ โ ๐ซ | ๐๐ ๐ค1 (๐) = โ}, then ๐ ๐ค๐ โก ๐ ๐ค๐ .
Proof. By firewall completeness, a partition of ๐ซ is {๐๐ ๐ค1 , ๐๐ ๐ค1 }, where ๐๐ ๐ค1 = {๐ โ
๐ซ | ๐๐ ๐ค1 (๐) = โ} and ๐๐ ๐ค1 = {๐ โ ๐ซ | ๐๐ ๐ค1 (๐) = ๐} are the sets of packets, respec-
tively, discarded and forwarded by ๐ ๐ค1 . By hypothesis, packets in ๐๐ ๐ค1 match at least one
rule in ๐1 , . . . , ๐๐ . Conversely, since ๐๐ ๐ค1 and ๐๐ ๐ค1 are disjoint sets, packets in ๐๐ ๐ค1 do not
match any of rules ๐1 , . . . , ๐๐ . Packets in ๐๐ ๐ค1 are discarded by ๐ ๐ค๐ as, by definition of ๐๐ ๐ค1 ,
they are discarded by ๐ ๐ค1 . Equivalently, packets in ๐๐ ๐ค1 are discarded by ๐ ๐ค๐ , as they are
forwarded by the trivial firewall ๐ ๐ค1 , but discarded by ๐ ๐ค2 , as they match at least one of the
๐๐๐๐ฆ rules ๐1 , . . . , ๐๐ placed at the top of ๐ ๐ค2 .
Packets in ๐๐ ๐ค1 are forwarded by ๐ ๐ค1 by definition of ๐๐ ๐ค1 , thus their fate in ๐ ๐ค๐ is
determined by ๐ ๐ค2 . In ๐ ๐ค๐ , packets in ๐๐ ๐ค1 are forwarded by the trivial firewall ๐ ๐ค1 and
their fate is determined by ๐ ๐ค2 . However, since packets in ๐๐ ๐ค1 do not match any of rules
๐1 , . . . , ๐๐ , they have as a matching rule in ๐ ๐ค2 the same (๐๐๐๐๐ค or ๐๐๐๐ฆ) matching rule they
have in ๐ ๐ค2 , i.e., ๐๐ ๐ค2 (๐) = ๐๐ ๐ค (๐). Summarizing, โ๐ โ ๐๐ ๐ค1 , ๐๐ ๐ค๐ (๐) = ๐๐ ๐ค๐ (๐) = โ and
2
โ๐ โ ๐๐ ๐ค1 , ๐๐ ๐ค๐ (๐) = ๐๐ ๐ค๐ (๐) = ๐๐ ๐ค2 (๐). Since {๐๐ ๐ค1 , ๐๐ ๐ค1 } is a partition of ๐ซ, it follows
that โ๐ โ ๐ซ, ๐๐ ๐ค๐ (๐) = ๐๐ ๐ค (๐), i.e., ๐ ๐ค๐ โก ๐ ๐ค๐ , which proves the thesis. โก
A.2. Proofs referenced in Subsect. 4.1
Given a firewall ๐ ๐ค1 = (๐1๐ ๐ค1 , ๐2๐ ๐ค1 , . . . , ๐|๐
๐ ๐ค1
๐ค1 | ), the set of packets discarded by the firewall,
๐๐ ๐ค1 = {๐ โ ๐ซ | ๐๐ ๐ค1 (๐) = โ}, can be expressed as:
โ โ โโ
โ๏ธ โ๏ธ
๐๐ ๐ค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 . In (14), each set ๐ฎ๐๐ ๐ค1 , defined by a ๐๐๐๐ฆ
๐
rule in ๐ ๐ค1 (i.e., ๐ โ ๐ฟ), appearing at least once in the second (internal) set union, also appears
(๏ธโ๏ธ (๏ธ )๏ธ )๏ธ
once in the first (external) set union. That is, for any term ๐ โ ๐<๐ ๐ฎ๐๐๐ ๐ค1 โช ๐ฎ๐๐ ๐ค1 โช ๐ ,
๐
where ๐ โ ๐ฟ, and ๐ and ๐ have (๏ธโ๏ธ been used)๏ธto indicate unions of sets defined by rules in ๐ ๐ค1 ,
there is also a term ๐ฎ๐๐ ๐ค1 โ ๐<๐ ๐ฎ๐๐ ๐ค1 . By set property (๐ โ โฌ) โช (๐ โ (๐ โช โฌ โช ๐)) =
๐ ๐
(๐ โ โฌ) โช (๐ถ โ (โฌ โช ๐)), which holds for generic sets ๐, โฌ, ๐, ๐, considering ๐ฎ๐๐ ๐ค1 = ๐ and
(๏ธ )๏ธ ๐
it follows that term can be neglected any time it appears in the
โ๏ธ
๐<๐ ๐ฎ ๐ ๐ค
๐๐ 1
= โฌ, ๐ฎ ๐ ๐ค
๐๐ 1
second (internal) set union in (14), i.e.,
โ โ โโ
โ๏ธ โ๏ธ
๐๐ ๐ค1 = โ๐ฎ ๐ ๐ค1 โ โ
๐
๐ฎ๐๐ ๐ค1 โ โ (15)
โ ๐
โโ๐ฟ ๐โ๐ผโ๐ฟ,๐<โ
since ๐ผ โ ๐ฟ = ๐ , equality (15) proves the thesis. โก
We consider a packet set ๐๐ ๐ค1 defined by
โ๏ธ (๏ธ(๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ )๏ธ
๐๐ ๐ค 1 = . . . ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 (16)
โ ๐1 ๐2 ๐|๐ |
โโ๐ฟ โ
where, in general ๐ฎ๐ is the packet set defined by a rule ๐ and where ๐ฟ and ๐ are sets of indexes
and, for each โ โ ๐ฟ, ๐โ = {๐1 , ๐2 , . . . , ๐|๐โ | } = {๐ โ ๐, ๐ < โ} is the set of indexes in ๐
๐|๐ | ๐|๐ |
preceding โ. We then consider, rule set โ* = โโ๐ฟ โโ โ , where for each โ โ ๐ฟ rule set โโ โ
โ๏ธ
is iteratively computed as:
๐ ๐ค1
โ๏ธ
โ๐โ
0
= {๐โ }, โ ๐๐ก
โ = sub_rule(๐, ๐๐๐ ๐ค1
๐ก
) ๐ก = 1, . . . , ๐|๐โ | (17)
๐
๐โโโ ๐กโ1
โ๏ธ
where sub_rule(๐๐ , ๐๐ ) is a rule subtraction operator, want to prove that ๐โโ* ๐ฎ๐ = ๐๐ ๐ค1
๐|๐ |
Proof. We prove that for each โ โ ๐ฟ, rule set โโ โ , computed as defined in (17), is such that:
โ๏ธ (๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ
๐ฎ๐ = . . . ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 (18)
โ ๐1 ๐2 ๐|๐ |
๐|๐ | โ
๐โโโ โ
We prove (18), by proving by induction over ๐ก, that for each ๐ก = 1, . . . , |๐โ |, rule set โ๐โ ,
๐ก
computed as defined in (17), is such that:
โ๏ธ (๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ
๐ฎ๐ = . . . ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 (19)
โ ๐1 ๐2 ๐๐ก
๐
๐โโโ ๐ก
(17), โ๐
Base case (๐ก = 1): according to โ๏ธ โ
1
= sub_rule(๐โ๐ ๐ค1 , ๐๐
๐ ๐ค1
1 ). By definition of rule
subtraction operator, it holds that ๐โโ๐1 ๐ฎ๐ = ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 , which proves the thesis.
โ โ ๐1
๐
Induction (๐ก โ 1 โ ๐ก): โโ ๐กโ1 is such that
โ๏ธ (๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ
๐ฎ๐ = . . . ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 (20)
โ ๐1 ๐2 ๐๐กโ1
๐
๐โโโ ๐กโ1
(๏ธ(๏ธ (๏ธ(๏ธ )๏ธ )๏ธ )๏ธ )๏ธ
From (20), set ... ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 . . . โ ๐ฎ๐๐ ๐ค1 โ ๐ฎ๐๐ ๐ค1 can be expressed as:
โ ๐1 ๐2 ๐๐กโ1 ๐๐ก
โ โ
โ๏ธ โ๏ธ (๏ธ )๏ธ
๐ฎ๐ โ โ ๐ฎ๐๐ ๐ค1 = ๐ฎ๐ โ ๐ฎ๐๐ ๐ค1 (21)
โ โ
โ ๐๐ก ๐๐ก
๐ ๐
๐โโโ ๐กโ1 ๐โโโ ๐กโ1
where the second
โ๏ธ๐ equality in (21) derivesโ๏ธfrom set property, valid for generic sets ๐, โฌ
๐
and ๐๐ , ๐ = ๐=1 ๐๐ โ ๐ โ ๐ต = ๐=1 (๐๐ โ โฌ). Since, according to (17), โ๐ โ
๐ก
=
๐ ๐ค1
sub_rule(๐, ๐๐๐ก ), by definition of rule subtraction operator, thesis holds true. โก
โ๏ธ
๐
๐โโ ๐กโ1 โ
A.3. Proof referenced in Subsect. 4.2
Alg. 3 implements a rule subtraction operator, i.e., given two rules ๐๐ = โจ(๐ถ1๐๐ , ๐ถ2๐๐ , . . . , , ๐ถ๐๐๐ ),
๐๐๐ก๐๐๐๐๐ โฉ and ๐๐ = โจ(๐ถ1๐๐ , ๐ถ2๐๐ , .โ๏ธ. . , , ๐ถ๐๐๐ ), ๐๐๐ก๐๐๐๐๐ โฉ, it returns a set of rules โ, with the same
action as ๐๐ , satisfying property: ๐โโ ๐ฎ๐ = ๐ฎ๐๐ โ ๐ฎ๐๐ .
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
๐ ๐ ๐
call ๐ฎ๐ , ๐ โค ๐, the projection of ๐ฎ๐ over set ๐ซ โ N๐0 , where ๐ซ is the projection of ๐ซ over N๐0 :
๐ ๐
๐ฎ๐ = {๐ โ ๐ซ | ๐๐ โ ๐ถ๐ , ๐ = 1, . . . , ๐} = ๐ถ1 ร ๐ถ2 ร ยท ยท ยท ร ๐ถ๐ (22)
๐ ๐ ๐โ1
Set ๐ฎ๐ , ๐ โค ๐, is a hyperrectangle in N๐0 . Given a rule ๐๐ , from (22) it holds that ๐ฎ๐๐ = ๐ฎ๐๐ ร ๐ถ๐๐๐ .
Since by set property ๐ = (๐ โ โฌ) โช (๐ โฉ โฌ), which holds for any pair of sets ๐ and โฌ, we
๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1
have that ๐ฎ๐๐ = (๐ฎ๐๐ โ ๐ฎ๐๐ ) โช (๐ฎ๐๐ โฉ ๐ฎ๐๐ ), we obtain:
๐ ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1
๐ฎ๐๐ = ((๐ฎ๐๐ โ ๐ฎ๐๐ ) โช (๐ฎ๐๐ โฉ ๐ฎ๐๐ )) ร ๐ถ๐๐๐ = ((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โช ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) (23)
๐ ๐ ๐ ๐ ๐
By set property ๐ โ โฌ = ๐ โ (๐ โฉ โฌ), we have ๐ฎ๐๐ โ ๐ฎ๐๐ = ๐ฎ๐๐ โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) and by using (23)
we obtain
๐ ๐ ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐ ๐
๐ฎ๐๐ โ ๐ฎ๐๐ = (((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โช ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ )) โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ )
๐โ1 ๐โ1 ๐ ๐ ๐โ1 ๐โ1 ๐ ๐
= (((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ )โ(๐ฎ๐๐ โฉ ๐ฎ๐๐ )) โช (((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ )) (24)
๐โ1 ๐โ1 ๐ ๐ ๐โ1 ๐โ1 ๐โ1
We can rewrite ((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) and (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) as ((๐ฎ๐๐ โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ )) ร ๐ถ๐๐๐ ) and
๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐โ1
(๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โฉ ๐ถ๐๐๐ ), respectively. Since (๐ฎ๐๐ โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ )) and (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) are disjoint,
๐โ1 ๐โ1 ๐ ๐
((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) and (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) are disjoint and (24) becomes:
๐ ๐ ๐โ1 ๐โ1 ๐โ1 ๐โ1 ๐ ๐
๐ฎ๐๐ โ ๐ฎ๐๐ = ((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โช (((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ )) (25)
๐
Since sets ๐ฎ๐ , ๐ โค ๐ are hyperrectangles, it holds that
๐ ๐ ๐โ1 ๐โ1
๐ฎ๐๐ โฉ ๐ฎ๐๐ = (๐ถ1๐๐ โฉ ๐ถ1๐๐ ) ร (๐ถ2๐๐ โฉ ๐ถ2๐๐ ) ร . . . ร (๐ถ๐๐๐ โฉ ๐ถ๐๐๐ ) = (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โฉ ๐ถ๐๐๐ ) (26)
From (26), we can rewrite the second term in union (25) as:
๐โ1 ๐โ1 ๐ ๐ ๐โ1 ๐โ1 ๐โ1 ๐โ1
((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โ (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) = ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โ ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โฉ ๐ถ๐๐๐ ))
๐โ1 ๐โ1
= (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โ (๐ถ๐๐๐ โฉ ๐ถ๐๐๐ ))
๐โ1 ๐โ1
= (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โ ๐ถ๐๐๐ ) (27)
where the last equality is obtained by using again set property ๐ โ โฌ = ๐ โ (๐ โฉ โฌ).
Summarizing, from (25) and (27) we have that:
๐ ๐ ๐โ1 ๐โ1 ๐โ1 ๐โ1
๐ฎ๐๐ โ ๐ฎ๐๐ = ((๐ฎ๐๐ โ ๐ฎ๐๐ ) ร ๐ถ๐๐๐ ) โช ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โ ๐ถ๐๐๐ )) (28)
To translate set (28) into a set of rules defining it, we prove, by induction over ๐, that (28) can
be expressed as a set of sets of the kind ๐ถ1 ร ๐ถ2 ร . . . ๐ถ๐ (i.e., of hyperrectangles).
1 1
Base case (๐ = 1): ๐ฎ๐๐ โ ๐ฎ๐๐ = (๐ถ1๐๐ โ ๐ถ1๐๐ ). (๐ถ1๐๐ โ ๐ถ1๐๐ ) can be computed by
๐
sub_range(๐ถ1 ๐ , ๐ถ1 ๐ ), which returns a set of ranges (i.e., of hyperrectangles in N10 ).
๐
๐โ1 ๐โ1
Induction step (๐ โ 1 โ ๐): We assume ๐ฎ๐๐ โ ๐ฎ๐๐ to be expressed as a set of hyperrectangles.
The first term in union (28), is then a hyperrectangle. The second term in union in union (28) is
๐โ1 ๐โ1 ๐โ1 ๐โ1
((๐ฎ๐๐ โฉ ๐ฎ๐๐ )ร(๐ถ๐๐๐ โ๐ถ๐๐๐ )). By (26), (๐ฎ๐๐ โฉ ๐ฎ๐๐ ) is a hyperrectangle, and since (๐ถ๐๐๐ โ๐ถ๐๐๐ ) can be
๐โ1 ๐โ1
computed by sub_range(๐ถ๐๐๐ , ๐ถ๐๐๐ ) which returns a set of ranges, ((๐ฎ๐๐ โฉ ๐ฎ๐๐ ) ร (๐ถ๐๐๐ โ ๐ถ๐๐๐ ))
returns a set of hyperrectangles, which proves the thesis.
Now we prove that Alg. 3 computes conditions (๐ถ1 , ๐ถ2 , . . . , ๐ถ๐ ) defining the just described
๐ ๐
hyperrectangles (28), from which it generates rules of โ. In (28) set ๐ฎ๐๐ โ ๐ฎ๐๐ is incrementally
๐โ1 ๐โ1 ๐
built by set ๐ฎ๐๐ โ ๐ฎ๐๐ , ๐ โค ๐, we call the set of conditions defining the first set ๐1 . We compute
๐โ1 ๐โ1
๐ถ๐๐๐ โ ๐ถ๐๐๐ as sub_range(๐ถ๐๐๐ , ๐ถ๐๐๐ ). Moreover, we call the set of conditions defining ๐ฎ๐๐ โฉ ๐ฎ๐๐
๐โ1
as ๐2 . We can now rewrite (28) in terms of set of conditions as:
๐ ๐โ1 ๐โ1
๐1 = ( ๐1 ร ๐ถ๐๐๐ ) โช ( ๐2 ร sub_range(๐ถ๐๐๐ , ๐ถ๐๐๐ )) (29)
In Alg. 3, two set ๐1 and ๐2 are initialized (lines 3-4) respectively to sub_range(๐ถ1๐๐ , ๐ถ1๐๐ ) and
1 1
๐ฎ๐๐ โฉ ๐ฎ๐๐ . Both are then updated in ๐ step (loop in lines 5-8), in particular line 6 implements
๐
(29). At the end, ๐1 = ๐1 , and the set of conditions is used to build rule set โ, which proves the
thesis. โก