Firewalls are efectively employed to protect network portions by blocking illegitimate traversing trafifc. However, during trafic 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 balance 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 technique 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.
Nowadays firewalls are pervasively deployed over the Internet to protect network portions (or single devices) against undesired/malicious trafic possibly threatening confidentiality, integrity and availability of the provided services. Firewalls implement security policies, which, operatively, translate in lists of rules, each consisting of a condition defined over some packet header fields ( filtering fields ), and an action. Firewalls operating according to the first matching strategy check incoming packets against rule conditions sequentially, until the matching rule (i.e., the first rule in the list whose condition is satisfied by the packet) is found, and then apply the corresponding action (i.e., typically or ).
Firewall operation also impacts the legitimate trafic and, especially during trafic load peaks
(when the average packet arrival rate exceeds the firewall average service rate), legitimate
packets may sufer high delays and even be lost before being processed because of overloads and
overflows [
This paper presents a technique which may be used as a building block towards the development of a cooperative solution, mitigating network performance degradation caused by ifrewalls during trafic 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.
Several techniques have been proposed to mitigate firewall impact on legitimate trafic. Some of
them aim at minimizing firewall cardinality without changing the implemented security policy
(e.g., policy analysis [
The technique we propose can be used in combination with all the previously mentioned
ones but follows a diferent approach, i.e., like [
A packet defined over fields , = 1, . . . , , is a -tuple = (1, 2, . . . , ), ∈ , = 1, . . . , (1) A packet is a point in N0, and the finite set of all possible packets defined over fields , = 1, . . . , , = 1 × 2 × . . . × ⊆ N0, is a hyperrectangle (the generalization of a rectangle in a -dimensional space) in N0. 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 where for = 1, . . . , , is a range such that ⊆ .
A rule over fields , = 1, . . . , , is defined as = (1, 2, . . . , ) = ⟨, ⟩ (2) (3) where is a condition over fields , = 1, . . . , and varies in the set of all possible ifrewall 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 N0.
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 diferent 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 diferent rule lists may define the same ifltering 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. (a) (c) fw r1 = h(C1r1; C2r1; : : : ; Cnr1); actionr1i r2 = h(C1r2; C2r2; : : : ; Cnr2); actionr2i . . . rjfwj = h( ; ; : : : ; ); actionrjfwji (b)
fwjfwsj r1 r2 r3 r4 r5
C1 * * * * *
C2 192.168.2.1-50 192.168.2.1-50 192.168.2.1-50 192.168.3.1-50 *
C3 * * * * *
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 trafic. Although an upstream ifrewall is typically traversed by more packets and thus more likely to sufer 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.
The proposed security policy migration technique is based on the observation that a packet whose matching rule in 1 is a rule, independently of its matching rule in 2, is dropped by and, for (6) to hold, should be dropped by as well. As a consequence, if we compute a set of rules, which discards all and only packets originally discarded by 1, we can move list these rules before those in 2 to obtain 2 required by Prob. 1. Formally: Theorem 1. Given Prob. 1, if a set of rules 1, 2, . . . , satisfies property ⋃︁ =1 = 1 = { ∈ | 1 () = −} , 2 = (1, . . . , , 12 , . . . , |22|) P2 8 6 4 2 0
Sr4fw1 = P Sr2fw1 Sr1fw1 Sr3fw1 fw1 allow deny r1fw1 = h([1; 5]; [4; 6]); denyi r2fw1 = h([2; 4]; [5; 8]); allowi r3fw1 = h([5; 7]; [1; 3]); allowi r4fw1 = h([0; 9]; [0; 9]); denyi where is packet set defined by rule and 1 is the set of packets discarded by 1, then 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 2 4 6 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, possibly empty, set ℛ of rules, with the same action as , such that ⋃︀ Definition 1.
A rule subtraction operator is any operator that given rules and , returns a, 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 ⋃︀ they result from sequences of rule subtractions from rules 1 .
ℓ
|ℓ| . As required by Thm. 1, they are all rules, as
= 1, . . . , 4, defined over = 2 filtering fields
= [
1, 1 , is represented in Fig. 2 through symbols and colors: dotted white points of N02 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 ∖ 1 . The required
4 2 3 ︁( ︁) ︁) 0 1 } and set of rules can be computed as ℛ1 ∪ ℛ43, where, based on (12), ℛ10 = {1 ℛ34 = ⋃︀∈ℛ42 sub_rule(, 31 ), with ℛ42 = sub_rule(41 , 21 ).
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 (line 6), executes rule subtractions between each rule in ℛ and 1 (lines 8-10). Routine sub_rule(, ) (line 9) implements the defined rule subtraction operator, and is described in detail in Subsect. 4.2. Rules resulting from rule subtractions having 1 as subtrahend are stored in ℛ and, subsequently, copied back in ℛ to be the new minuend. Once the process is repeated for each rule 1 preceding ℓ1 , ℛ is equal to ℛℓ|ℓ| and Alg. 1 lists the rules it contains in 2 (line 14).
In this subsection, we describe the defined rule subtraction operator, sub_rule(, ),
implemented 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 || ∈ [
Data: 1 = (11 , 21 , . . . , |11|) 2 = (12 , 22 , . . . , |22|)
Result: 2 = (12 , 22 , . . . , |22|) ad
Cd
bd (a) ad
Cd aa Ca ba ad aa Ca ba
bd Cd (b)
bd
rrrr12da [[[[1717C,,,,18968]]]] [[[[2124C,,,,27377]]]] aadddcleeetlnnnioowyyyn
rrda [[15C,,187]] [[24C,,276]] aadcletlnioowyn
rrda [[91C,,1181]] [[21C,,273]] aadcletlnioowyn
r1 [
P1 P1
P2 8 6 4 2 0 P2 8 6 4 2 0 2 4 6 8 10 (c) Four resulting rules. property ⋃︀∈ = ∖ . The range subtraction operator is implemented by Alg. 2, which distinguishes between the four cases in Fig. 3: if ranges and are non overlapping (cases captured by line 5 or 9, shown in Fig. 3a), = {}, if and partially overlap (cases captured by line 4 or 8, shown in Fig. 3b), contains a single range, portion of , if ⊂ (cases captured by both lines 4 and 8, shown in Fig. 3c), contains two ranges, portions of , and, finally, if ⊂ (none of the above, Fig. 3d), = ∅.
Alg. 3 iteratively computes a set 1 of conditions defined over filtering fields (lines
3-8), whose elements are used to compute rules of set ℛ (line 9). Set 1 is initialized to
sub_range(1 , 1 ) and is then updated in − 1 steps (lines 5-8). At each step ∈ [2, ],
1 is obtained as the union of two sets of conditions (line 6). The first set is recursively
computed as the Cartesian product of current 1 and set containing single range (the result
of the Cartesian product between sets of tuple of ranges is a set of tuple of ranges, i.e., of
conditions). The second set is computed as the Cartesian product of set containing single
condition (1 ∩ 1 , . . . , − 1 ∩ − 1), with set of ranges sub_range( , ). Fig. 4
shows examples of pairs of rules defined over = 2 filtering fields. Considering, e.g., case
in Fig. 4c, 1 = [
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), |ℛ| ∈ [
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 ifrewall. One way to mitigate this efect 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 , || ∈ [
fw2
C1 C2 C3 C4 C5 action r1 * * * * * allow
We presented a technique for migrating security policies along firewalls in a sequence, which is formally verified to preserve the overall security policy implemented by the sequence itself. The proposed technique can be extended to the case of more general topologies comprising firewallprotected domains and is the building block for the development of cooperative solutions balancing workload by distributing filtering responsibility among firewalls available within a protected network. Future work will analyze solutions to compress rule lists obtained after migration in the cooperating firewall, as the proposed technique may lead to rule proliferation. Techniques for suitably partitioning the packet space will also be investigated to split policies based on network/workload characteristics and further optimize network performance.
This work was supported in part by the EU H2020-SU-ICT-03-2018 Project No. 830929 CyberSec4Europe (cybersec4europe.eu).
Given = ( 1, 2), = (1 , 2 , . . . , ||), = 1, 2, and = ( 1, 2), where 1 = (⟨(* , * , . . . , * ), ⟩) and 2 = (1, . . . , , 12 , . . . , |22|), 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, respectively, 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 () = 2 (). Summarizing, ∀ ∈ 1 , () = () = − and ∀ ∈ 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 = (11 , 1 , . . . , 1 ), the set of packets discarded by the firewall, 2 |1| 1 = { ∈ | 1 () = −} , can be expressed as: ⎛
⎛ 1 = ℓ⋃∈︁ ⎝ℓ1 ∖ ⎝
⋃︁
⎞⎞ where , and are, respectively, is the set of indexes of and rules in 1. Proof. By definition of firewall operation, in 1 a rule, i.e., 1 is the set of packets having as a matching rule (13) (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 ∖ ︁( ⋃︀
︁) 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 ︁( ⋃︀ < ︁( 1 ︁) ∪ 1 ∪ , second (internal) set union in (14), i.e., = ℬ, it follows that term 1 can be neglected any time it appears in the 1 = ⋃︁ ℓ∈ ⎛
⎛ since ∖ = , equality (15) proves the thesis.
We consider a packet set 1 defined by 1 = ⋃︁ (︂ (︁ . . .
︁( ℓ∈
︁) ︁) ︂) is iteratively computed as: preceding ℓ. We then consider, rule set ℛ* = ⋃︀ 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 |ℓ| , where for each ℓ ∈ rule set ℛℓ |ℓ| ⋃︁ ∈ℛℓ 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 computed as defined in (17), is such that: We prove (18), by proving by induction over , that for each = 1, . . . , |ℓ|, rule set ℛℓ , subtraction operator, it holds that ⋃︀
Base case ( = 1): according to (17), ℛℓ Induction ( − 1 ⇒ ): ℛℓ − 1 is such that ∈ℛℓ 1 = 1 ∖ 11 , which proves the thesis.
ℓ 1 = sub_rule(ℓ1 , 11 ). By definition of rule ︁) ︁) ︁) ︁) ︁) ⋃︁ − 1 = . . . . . .)︁ ∖ −1 1 □ ︁) (15) (16) (17) (18) (19) (20) From (20), set ︂( (︁
∖ 1 can be expressed as: ⎟⎠ ∖ 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(, 1 ), by definition of rule subtraction operator, thesis holds true. (21) □ we obtain
A.3. Proof referenced in Subsect. 4.2 action as , satisfying property: ⋃︀
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 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 ⊆
N0, where is the projection of over N0:
= { ∈ | ∈ , = 1, . . . , } = 1 × 2 × · · · × − 1 − 1 − 1 − 1
− 1 have that = ( ∖ ) ∪ ( ∩ ), we obtain: Set , ≤ , is a hyperrectangle in N0. 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 = (( ∖ ) ∪ ( ∩ )) × = (( ∖ ) × ) ∪ (( ∩ ) × ) (23) − 1
− 1 − 1 − 1 − 1 (22) .
By set property ∖ ℬ = ∖ ( ∩ ℬ), we have ∖ = ∖ ( ∩ ) and by using (23) − 1
− 1 We can rewrite (( ∖ ) × ( ∩ ) × ( ∩ ), respectively. Since ( ∖ ( ∩ )) and ( ∩ ) are disjoint, − 1 − 1 − 1 − 1
− 1 ) and ( ∩ ) as (( ∖ ( ∩ )) × − 1 − 1 − 1 ) and − 1 − 1 − 1 − 1 − 1 − 1 − 1
− 1 ∖ = ((( ∖ ) × ) ∪ (( ∩ ) × )) ∖ ( ∩ ) = ((( ∖ ) × )∖( ∩ )) ∪ ((( ∩ ) × ) ∖ ( ∩ )) (24) − 1 − 1
− 1 − 1 − 1 − 1 ∖ = (( ∖ ) × ) ∪ ((( ∩ ) × ) ∖ ( ∩ ))
Since sets , ≤ are hyperrectangles, it holds that (25) − 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 N01).
− 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( , )) 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. □ (29)