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. โ–ก