Yacine Boufkhad

Leonardo Linguaglossa

Fabien Mathieu

Diego Perino

Laurent Viennot

Efficient Loop Detection in Forwarding Networks and Representing Atoms in a Field of Sets

Keywords: Forwarding tables, Loop, Software-defined networking, Field of sets

The problem of detecting loops in a forwarding network is known to be NP-complete when general rules such as wildcard expressions are used. Yet, network analyzer tools such as Netplumber (Kazemian et al., NSDI'13) or Veriflow (Khurshid et al., NSDI'13) efficiently solve this problem in networks with thousands of forwarding rules. In this paper, we complement such experimental validation of practical heuristics with the first provably efficient algorithm in the context of general rules. Our main tool is a canonical representation of the atoms (i.e. the minimal non-empty sets) of the field of sets generated by a collection of sets. This tool is particularly suited when the intersection of two sets can be efficiently computed and represented. In the case of forwarding networks, each forwarding rule is associated with the set of packet headers it matches. The atoms then correspond to classes of headers with same behavior in the network. We propose an algorithm for atom computation and provide the first polynomial time algorithm for loop detection in terms of number of classes (which can be exponential in general). This contrasts with previous methods that can be exponential, even in simple cases with linear number of classes. Second, we introduce a notion of network dimension captured by the overlapping degree of forwarding rules. The values of this measure appear to be very low in practice and constant overlapping degree ensures polynomial number of header classes. Forwarding loop detection is thus polynomial in forwarding networks with constant overlapping degree.

Introduction

With the multiplication of network protocols, network analysis has become an important and challenging task. We focus on a key diagnosis task: detecting possible forwarding loops. Given a network and node forwarding tables, the problem consists in testing whether there exists a packet header h and a directed cycle in the network topology such that a packet with header h will indefinitely loop along the cycle. This problem is indeed NP-complete as noted in [START_REF] Mai | Debugging the Data Plane with Anteater[END_REF]. Its hardness comes from the use of compact representations for predicate filters: the set of headers that match a rule is classically represented by a prefix in IP forwarding, a general wildcard expression in Software-Defined Networking (SDN), value ranges in firewall rules, or even a mix of such representations if several header fields are considered.

We first give a toy example of forwarding loop problem where the predicate filter of each rule is given by a wildcard expression, that is an ℓ-letter string in {1, 0, * } ℓ . Such an expression represents the set all ℓ-bit headers obtained by replacing each * of the expression by either 0 or 1. A packet with header in that set is said to match the rule. Figure 1 illustrates a one node network with wildcard expressions of ℓ = 4 letters. Rules are tested from top to bottom. All rules indicate to drop packets except the last one that forwards packets to the node itself. This network contains a forwarding loop if there exists a header x 1 x 2 x 3 x 4 that matches no rule except the last one. Not matching a rule as 110 * corresponds to having x 1 = 0, x 2 = 0, or x 3 = 1. This one node network thus has a forwarding loop iff the formula (

x 1 ∨ x 2 ∨ x 3 ∨ x 4 ) ∧ (x 1 ∨ x 2 ∨ x 3 ∨ x 4 ) ∧ (x 1 ∨ x 2 ∨ x 3 ) ∧ (x 1 ∨ x 2 ) ∧ (x 1
) is satisfiable, which is not the case. This simple example can easily be generalized to reduce SAT to forwarding loop detection in networks with wildcard rules. It also points out a key problem: testing the emptiness of expressions such as r p \ ∪ i=1..p-1 r i where r 1 , . . . , r p are the sets associated to p rules. As packet headers in practical networks such as Internet typically have hundreds of bits, search of the header space is completely out of reach. The main challenge for solving such a problem thus resides in limiting the number of tests to perform. For that purpose, previous works [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF][START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] propose to consider sets of headers that match some predicate filters and do not match some others. Defining two headers as equivalent when they match exactly the same predicate filters, it then suffices to perform one test per equivalence class. These classes are indeed the atoms (the minimal non-empty sets) of the field of sets (the (finite) σ-algebra) generated by the sets associated to the rules.

A first challenge lies in efficiently identifying and representing these atoms. This would be fairly easy if both intersection and complement could be represented efficiently. In practice, most classical compact data-structures for sets of bit strings are closed under intersection but not under complement. For example, the intersection of two wildcard expressions, if not empty, can obviously be represented by a wildcard expression, but the complement of a wildcard expression is more problematic. Previous works overcome this difficulty by representing the complement of a ℓ-letter wildcard expression as the union of several wildcard expressions (up to ℓ). However, this can result in exponential blow-up and the tractability of these methods rely on various heuristics that do not offer rigorously proven guarantees.

A second challenge lies in understanding the tractability of practical networks. One can easily design a collection of 2ℓ wildcard expressions that generates all the 2 ℓ possible singletons as atoms (all the ℓ-letters strings with only one non- * letter). What does prevent such phenomenon in practice? Can we provide a property that intuitively fits with practical network and guarantees that the number of atoms does not blow up? This paper aims at addressing both challenges with provable guarantees.

Related work

The interest for network problem diagnosis has recently grown after the advent of Software-Defined Networking (SDN) [START_REF] Perešíni | CPP: Consistent Packet Processing for Openflow[END_REF][START_REF] Kotronis | Outsourcing the routing control logic: Better internet routing based on SDN principles[END_REF][START_REF] Monsanto | Composing software-defined networks[END_REF][START_REF] Naga Praveen Katta | Incremental consistent updates[END_REF]. SDN offers the opportunity to manage the forwarding tables of a network with a centralized controller where full knowledge is available for analysis. Previous works has led to a series of methods for network analysis, resulting in several tools [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF][START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF][START_REF] Mai | Debugging the Data Plane with Anteater[END_REF][START_REF] Zeng | Libra: Divide and conquer to verify forwarding tables in huge networks[END_REF]. The main approaches rely on computing classes of headers by combining rule predicate filters using intersection and set difference (that is intersection with complement). The idea of considering all header classes generated by the global collection of the sets associated to all forwarding rules in the network is due to Veriflow [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF]. However, the use of set differences results in computing a refined partition of the atoms of the field of sets generated by this collection that can be much larger than an exact representation. NetPlumber [START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF], which relies on the header space analysis introduced in [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF], refines this approach by considering the set of headers that can follow a given path of the network topology. This set is represented as a union of classes that match some rules (those that indicate to forward along the path) and not some others (those that have higher priority and deviate from the path): a similar problem of atom representation thus arises. The idea of avoiding complement operations is somehow approached in the optimization called "lazy subtraction" that consists in delaying as much as possible the computation of set differences. However, when a loop is detected, formal expressions with set differences have to be tested for emptiness. They are then actually developed, possibly resulting in the manipulation of expressions with exponentially many terms.

Concerning the tractability of the problem, the authors of NetPlumber observe a phenomenon called "linear fragmentation" [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF][START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] that allows to argue for the efficiency of the method. They introduce a parameter c measuring this linear fragmentation and claim a polynomial time bound for loop detection for low c [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] (when emptiness tests are not included in the analysis). However, the rigorous analysis provided in [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] includes a c DG factor where D G is the diameter of the network graph. While this factor appears to be largely overestimated in practice, the sole hypothesis of linear fragmentation does not suffice for explaining tractability and prove polynomial time guarantees. The alternative approach of Veriflow is specifically optimized for rules resulting from range matching within each field of the header. When the number of fields is constant, polynomial time execution can be guaranteed but this result does not extend to general wildcard matching.

A similar problem consists in conflict detection between rules and their resolution [START_REF] Adiseshu | Detecting and resolving packet filter conflicts[END_REF][START_REF] Eppstein | Internet packet filter management and rectangle geometry[END_REF][START_REF] Boutier | Source-specific routing[END_REF]. It has mainly been studied in the context of multi-range rules [START_REF] Adiseshu | Detecting and resolving packet filter conflicts[END_REF][START_REF] Eppstein | Internet packet filter management and rectangle geometry[END_REF], which can benefit from computational geometry algorithms. (A multi-range can be seen as a hyperrectangle in a ddimensional euclidean space where d is the number of fields composing headers.) Another similar problem, determining efficiently the rule that applies to a given packet, has been studied for multi-ranges [START_REF] Eppstein | Internet packet filter management and rectangle geometry[END_REF][START_REF] Feldmann | Tradeoffs for packet classification[END_REF][START_REF] Gupta | Algorithms for packet classification[END_REF]. In the case of wildcard matching, such problems are related to the old problem of partial matching [START_REF] Ronald | Partial-match retrieval algorithms[END_REF]. It is believed to suffer from the "curse of dimensionality" [START_REF] Borodin | Lower bounds for high dimensional nearest neighbor search and related problems[END_REF][START_REF] Patrascu | Unifying the landscape of cell-probe lower bounds[END_REF] and no method significantly faster than exhaustive search is expected to be found with near linear memory (although some tradeoffs are known for small number of * letters [START_REF] Charikar | New algorithms for subset query, partial match, orthogonal range searching, and related problems[END_REF]). However, efficient hardware-based implementations exist based on Ternary Content Addressable Memory (TCAMs) [START_REF] Bosshart | Forwarding metamorphosis: Fast programmable match-action processing in hardware for SDN[END_REF] or Graphics Processing Unit (GPU) [START_REF] Varvello | Multi-layer packet classification with graphics processing units[END_REF].

Regarding the manipulation of set collections, recent work [START_REF] Mary | Efficient enumeration of solutions produced by closure operations[END_REF] shows how to enumerate all sets obtained by closure under given set operations with polynomial delay. In particular, this allows to produce the field of sets generated by the collection. However, this setting requires a set representation which explicitly lists all elements and does not apply here. Another issue comes from the fact that the field set can be exponentially larger than its number of atoms.

Rule repr.

Trivial

NetPlumber [START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF] Veriflow [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF] This paper Our contributions First, we make a key algorithmic step by providing an efficient algorithm for computing an exact representation of the atoms of the field of sets generated by a collection of sets. The representation obtained is linear in the number of atoms and allows to test efficiently if an atom is included in a given set of the collection. The main idea is to represent an atom by the intersection of the sets that contain it. We avoid complement computations by using cardinality computations for testing emptiness. Our algorithm is generic and supports any data-structure for representing sets of ℓ-bit strings that supports intersection and cardinality computation in bounded time O(T ℓ ) for some value T ℓ . It runs in polynomial time with respect to n, m, the number of sets and atoms respectively. Beyond combinations of wildcard and range expressions, we believe that it could be extended to support expressions on hashed values (for a fixed hash function) or bloom filters by defining auxiliary cardinality measures. Second, we provide a dimension parameter, the overlapping degree k, that captures the complexity of a collection of rule sets considered in a forwarding network. It is defined as the maximum number of distinct rules (i.e. with pairwise distinct associated sets) that match a given header. This parameter constitutes a measure of complexity for the field of sets generated by a given collection of sets. In the context of practical hierarchical networks, we have the following intuitive reason to believe that this parameter is low: in such networks, more specific rules are used at lower levels of the hierarchy. We can thus expect that the overlapping degree is bounded by the number of layers of the hierarchy. Empirically, we observed a value within 5-15 for datasets with hundreds to thousands of distinct multi-field rules, and k = 8 for the collection of IPv4 prefixes advertised in BGP. A constant overlapping degree implies that the number of header classes is polynomially bounded, giving a hint on why practical networks are tractable despite the NP-completeness of the problem. In addition, the algorithm we propose is tailored to take advantage of low overlapping degree k, even without knowledge of k. Table 1 provides a summary of the complexity results obtained for loop detection depending on how the sets associated to rules are represented. Our techniques can be extended to handle write actions (partial writes of fixed values such as field replacement) while maintaining polynomial guarantees.

Tℓ-bounded O(TℓnnG2 ℓ ) - - O(Tℓnm 2 + nnGm) " ov. deg. O(log n) " - - Tℓn O(1) m + O(nGm log n) " ov. deg. k " - - O((Tℓn + Tℓk 2 2 k log n + knG)n k ) ℓ-wildcard O(ℓnnG2 ℓ ) Ω(ℓnG2 min(ℓ,n) ) Ω(nG2 min(ℓ/2,n) ) O(ℓnm 2 + nnGm) " ov. deg. k " Ω(ℓnG2 min(ℓ,n) ) Ω(nG2 min(ℓ/2,n) ) O((ℓn + ℓk2 k + knG)n k ) d-multi-rng. O(ℓnnG(2n) d ) - Ω( n d d-1 nG m d ) O(dnm 2 + nnGm) " ov. deg. k " - Ω( n d d-1 nG m d ) O((ℓk d+1 log d n + ℓk2 k + knG)n k )
Our algorithm for atom computation solves two difficult technical issues. First, it manages to remain polynomial in the number m of atoms even though the number of sets generated by intersection solely can be exponential in m with general rules. Second, the use of cardinality computations allows to avoid exponential blow-up (in contrast with previous work) but naturally induces a quadratic O(m 2 ) term in the complexity. However, we manage to reduce it to O(m) in the case of collections with logarithmic overlapping degree (i.e. k = O(log n)). Indeed, our algorithm then becomes linear in m and polynomial in n, providing an algorithmic breakthrough towards efficient atom enumeration.

Roadmap: Section 2 introduces the model. Section 3 describes how to represent the atoms of a field of sets. We state in Section 4 our main result concerning atom computation and its implications for forwarding loop detection that give the upper bounds listed in Table 1. Section 5 gives more insight about the comparison of our results with previous works and justifies the lower bounds presented in Table 1. Finally, Section 6 discusses some perspectives.

Model

Problem

We consider a general model of network where a network instance N is characterized by:

• a graph G = (V, E) where each node u ∈ V is a router and has a forwarding table T (u).

• a natural number ℓ representing the (fixed) bit-length of packet headers.

Let H denote the set of all 2 ℓ possible headers (all ℓ-bit strings). Each forwarding table T (u) is an ordered list of forwarding rules (r 1 , a 1 ), . . . , (r p , a p ). Each forwarding rule (r, a), is made of a predicate filter r and an action a to apply on any packet whose header matches the predicate. We say that a header h matches rule (r, a) when it matches predicate r (we may equivalently say that (r, a) matches h). We then write h ∈ r to emphasize the fact that r can be viewed as a compact data-structure encoding the set of headers that match it. This set is called the rule set associated to (r, a). For the ease of notation, we thus let r denote both the predicated filter of rule (r, a) and the associated set.

We consider three possible actions for a packet: forward to a neighbor, drop, or deliver (when the packet has reached destination). The priority of rules is given by their ordering: when a packet with header h arrives at node u, the first rule matched by h is applied. Equivalently, the rule

(r i , a i ) is applied when h ∈ r i ∩ r 1 ∩ • • • ∩ r i-1 , where r denotes the complement of r. When no match is found (i.e. h ∈ r 1 ∩ • • • ∩ r p ), the packet is dropped.
Given a header h, the forwarding graph G h = (V, E h ) of h represents the forwarding actions taken on a packet with header h: uv ∈ E h when the first rule that matches h in T (u) indicates to forward to v. The forwarding loop detection problem consists in deciding whether there exists a header h ∈ H such that G h has a directed cycle.

Note that we make the simplifying assumption that the input port of an incoming packet is not taken into account in the forwarding decision of a node. In a more general setting, a node has a forwarding table for each incoming link. This is essentially the same model except that we consider the line-graph of G instead of G.

Header Classes

A natural relation of equivalency exists between headers with respect to rules: two headers are equivalent if they match exactly the same rules, that is if they belong to the same rule sets. Trivially, two equivalent headers let the corresponding packets have exactly the same behavior in the network. The resulting equivalence classes partitions the header set H into nonempty disjoint subsets called header classes. To check any property of the network, it suffices to do it on a class-by-class basis instead of a header-by-header basis. The number m of header classes is thus a natural parameter when considering the difficulty of forwarding loop detection (or other similar network analysis problems). A more accurate definition of classes could take into account the order of rules and the topology (see Appendix E) but this does not allows us to obtain complexity gain in general.

The header classes can be defined according to the collection R of rule sets of N (i.e. R = {r | ∃u, a s.t. (r, a) ∈ T (u)}). If R(h) ⊆ R denotes the set of all rule sets associated to the rules matched by a given header h, then its header class is clearly equal to ∩ r∈R(h) r ∩ ∩ r∈R\R(h) r (with the convention ∩ r∈∅ r = H). Such sets are the atoms of the field of sets generated by R. Their computation is the main topic of this paper and is detailed in the next section.

Set representation

As we focus on the collection R of rule sets, we now detail our hypothesis on their representation. We assume that a data-structure D allows to represent some of the subsets of a space H. For the ease of notation, D ⊆ P(H) also denotes the collection of subsets that can be represented with D. We assume that D is closed under intersection: if s and s ′ are in D, so is s ∩ s ′ . We say that

⊆ s ′ is equivalent to |s ∩ s ′ | = |s|).
Two typical examples of data-structures meeting the above requirements are wildcard expressions and multi-ranges. In a forwarding network, we consider the header space H = {0, 1} ℓ of all ℓ-bit strings, which may be decomposed in several fields. A rule set is typically represented by a wildcard expression or a range of integers. In both cases, they can be represented within 2ℓ bits and both representation are O(ℓ)-bounded. We call ℓ-wildcard a string

e 1 • • • e ℓ ∈ {0, 1, * } ℓ . It represents the set {x 1 • • • x ℓ ∈ {0, 1} ℓ | ∀i, x i = e i or e i = * }.
If rules are decomposed into fields, any combinations of wildcard expressions and ranges can be used (either one for each field) and represented within O(ℓ) bits. However cardinality computations can take Θ(ℓ log ℓ) time as multiplications of big integers are required. Such representation is thus O(ℓ log ℓ)-bounded. Given d field lengths ℓ 1 , . . . , ℓ d with sum ℓ, we call (d, ℓ)-multi-range

a cartesian product [a 1 , b 1 ] × • • • × [a d , b d ] of d integer ranges with 0 ≤ a i ≤ b i < 2 ℓi for i in 1..d. It represents the set {bin(x 1 , ℓ 1 ) • • • bin(x d , ℓ d ) | (x 1 , . . . , x d ) ∈ [a 1 , b 1 ] × • • • × [a d , b d ]}
where bin(x i , ℓ i ) is the binary representation of x i within ℓ i bits.

When manipulating a collection of p sets in D, we assume that their representations are stored in a balanced binary search tree, allowing to dynamically add, remove or test membership of a set in O(T H log p) time. More efficient data-structures (tries and segment trees) can be used for wildcard expressions and multi-ranges as detailed in Appendix A.1.

Atoms and combinations generated by a collection of sets

Given a space of elements H, a collection is a finite set of subsets of H. The field of sets σ(R) generated by a collection R is the (finite) σ-algebra generated by R, that is the smallest collection closed under intersection, union and complement that contains R ∪ {∅, H}.

The atoms of σ(R) are classically defined as the non-empty elements that are minimal for inclusion. For brevity, we call them the atoms generated by R. Let A(R) denote their collection. Note that for a ∈ A(R) and r ∈ R, we have either a ⊆ r or a ⊆ r (otherwise a ∩ r and a ∩ r would be non-empty elements of σ(R) strictly included in a). This gives a characterization of the atoms that matches our definition of header classes when R is the collection of rule sets of a network (see Section 2.2):

A(R) = a = ∅ | ∃R ⊆ R, a = (∩ r∈R r) ∩ ∩ r∈R\R r . ( 1
)
For example, the collection R pictured in Figure 2 generates 7 atoms:

{0} = r 1 ∩ r2 ∩ r3 ∩ r4 , {1} = r 1 ∩ r 2 ∩ r3 ∩ r4 , {2, 4} = r 1 ∩ r 2 ∩ r 3 ∩ r4 , {3} = r 1 ∩ r 2 ∩ r 3 ∩ r 4 , {5} = r1 ∩ r 2 ∩ r 3 ∩ r4 , {6} = r1 ∩ r2 ∩ r 3 ∩ r4 , and {7} = r1 ∩ r2 ∩ r3 ∩ r4 .
Due to the complement operations, the atoms can be harder to represent than the rules they are generated from. In Figure 2, all rules are ranges, but the atom {2, 4} is not. When the intersection operation can be computed and represented efficiently (see Section 2.3), it is natural to consider the collection C(R) ⊆ σ(R) of combinations defined as sets that can obtain by intersection from sets in R:

C(R) := {c = ∅ | ∃R ⊆ R, c = ∩ r∈R r} . ( 2
)
In Figure 2, there are 8 combinations:

r 1 , r 1 ∩ r 2 , r 1 ∩ r 3 , r 4 , r 2 ∩ r 3 , r 3 , H and r 2 .
Given a collection R and a subset s ∈ H, we let R(s) := {r ∈ R | s ⊆ r} denote the containers of s, that is the sets in R that contain s. We associate each combination c ∈ C(R) with the set a(c) := c∩ ∩ r∈R\R(c) r . The function a(•) (with parenthesis) should not be confused with an atom a (without parenthesis). A combination c is said to be covered if a(c) = ∅ (the union of its noncontainers covers it), otherwise it is uncovered. Similarly, we associate each atom a ∈ A(R) with the combination c(a) := ∩ r∈R(a) r (this corresponds to the "positive" part of the characterization from Equation 1). The following proposition states that atoms can be represented by uncovered combinations. Based on Proposition 1, we say that an uncovered combination c represents atom a(c). UC(R) can be seen as a canonical representation of A(R) by a collection of combinations. In Figure Figure 2, atom {2, 4} is represented by combination r 1 ∩ r 3 = r 1 ∩ r 2 ∩ r 3 . Similarly, atoms {0}, {1}, {3}, {5}, {6} and {7} are represented by (uncovered) combinations r 1 , r 1 ∩ r 2 , r 4 , r 2 ∩ r 3 , r 3 , and H respectively. Combination r 2 is covered:

a(r 2 ) = r1 ∩ r 2 ∩ r3 ∩ r4 = ∅.
The proof of Proposition 1 is straightforward. First, we verify that if c is an uncovered combination, a(c) is an atom: it suffices to observe that c = ∩ r∈R(c) r and to match a(c) = c ∩ ∩ r∈R\R(c) r with the atom characterization given by Equation 1 using R = R(c). Similarly, if a = (∩ r∈R r) ∩ ∩ r∈R\R r is an atom for some R ⊆ R, the combination c(a) satisfies R(c(a)) = R which implies a(c(a)) = a. In particular, as a = ∅, c(a) is uncovered.

A nice property of the characterization of Proposition 1 is that it allows to efficiently test whether a set r ∈ R contains an atom a ∈ A(R): given a combination c that represents a, a ⊆ r is equivalent to c ⊆ r. This comes from the fact that every uncovered combination c has same containers as a(c). (If it was not the case, a(c) = ∅ and c is covered.) This explains the importance of determining UC(R), and in particular to separate covered combinations from uncovered ones. This is the subject of the next section, but we first formally introduce the notion of overlapping degree.

Overlapping degree of a collection Our representation is naturally associated to the following measure of complexity of a collection R. We define the overlapping degree k of R as the maximum number of containers of an element, that is k = max h∈H |R({h})|. Note that all elements within an atom have same containers in R and that a set cannot have more containers than any of its elements. We thus have:

k = max s⊆H |R(s)| = max a∈A(R)

|R(a)|

As any atom a can be expressed as a = (∩ r∈R r) ∩ ∩ r∈R\R r where R = R(a) is the set of containers of a, the number of atoms is obviously bounded by n k where n = |R| denotes the number of sets in R. The overlapping degree of a collection thus measures its complexity in terms of number of atoms it may generate.

We similarly define the average overlapping degree k as the average number of containers of an atom:

k = a∈A(R) |R(a)| |A(R)|
. We obviously have k ≤ k. Given a collection R, we will also consider the average overlapping degree K of combinations, that is the average overlapping degree of C(R). Note that C(R) has the same collection of atoms as R and that a combination c = ∩ r∈R(c) r containing an atom a must satisfy R(c) ⊆ R(a). The overlapping degree of C(R) is thus at most 2 k and we always have K ≤ 2 k .

In the example from Figure 2, one can verify that we have k = 4, k = 13/7 and K = 4. In real datasets we observe that both k and K are in the range [START_REF] Mark De Berg | Computational Geometry: Algorithms and Applications[END_REF][START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] while k is in the range [1.5, 5] (these include Inria firewall rules, Stanford forwarding tables provided by Kazemian et al. [START_REF] Peyman | HSA/NetPlumber source code repository[END_REF] and IPv4 prefixes announced at BGP level from Route Views [START_REF]Route Views Project[END_REF]).

Incremental computation of atoms

We can now state our main result concerning the computation of the atoms generated by a collection of sets.

Theorem 1. Given a space set H and a collection R of n subsets of H, the collection UC(R) of combinations that canonically represent the atoms A(R) can be incrementally computed with O(min(n+kK log m, nm)m) elementary set operations where: m is the number of atoms generated by R; k is the overlapping degree of R; K is the average overlapping degree of C(R); k is the average overlapping degree of R. Within this computation, each combination c ∈ UC(R) can be associated to the list R(c) of sets in R that contain c. This result can be extended to handle write actions as explained in Appendix F due to the lack of space. The upper-bounds for forwarding loop detection listed in Table 1 follow from Corollary 1 which is proved in Appendix A.3. A key ingredient consists in maintaining for each rule set a list that describes its presence, priority and action for each node. Detecting a loop for a header class a then consists in merging the lists associated to the rule sets containing a (as provided by our atom representation) for obtaining the forwarding graph G a = G h for all h ∈ a. Directed cycle detection is finally performed on each such graph.

In the rest of this Section, we prove Theorem 1 by introducing two incremental algorithms for atom computation and analyzing their performance. The incremental approach allows to avoid exponential blow-up even in cases where the number of combinations can be exponential in the number m of atoms (an example is given in Appendix B.2).

Algorithms for updating atoms

We first propose a basic algorithm for updating the collection UC of uncovered combinations of a collection R when a set r is added to R. The main idea is that after adding r to R, the only new uncovered combinations that can be created are intersections of pre-existing uncovered combinations with r (see Lemma 1 in Appendix A. The correctness of Algorithm 1 follows from the two above remarks (that is Lemma 1 and Lemma 2 in Appendix A.2). Its main complexity cost comes from intersecting r with each combination and computing the inclusion relation between combinations, that is O(nm) and O(m 2 ) elementary set operations respectively. Starting from UC = {H} and incrementally applying Algorithm 1 to each set in R thus allows to obtain UC(R) with O(nm 2 ) elementary set operations, yielding the general bound of Theorem 1.

To derive better bounds for low overlapping degree k, we propose a more involved algorithm that maintains c.sup and c.atsize from one iteration to another and makes only the necessary updates. This requires to handle several subtleties to enable lower complexity.

We similarly start by computing the collection Inter = {c ∈ UC | c ∩ r = ∅} of combinations intersecting r. A first subtlety comes from the fact that several combinations c may result in the same c ′ = c ∩ r. However, we are only interested in the combination c which is minimal for inclusion that we call the parent of c ′ . The reason is that c ′ .sup can then be computed from c.sup. The parent is unique unless c ′ is covered in which case c ′ is marked as covered and discarded (see the argument for c ′ .sup computation later on). To obtain right parent information, we thus process all c ∈ Inter by non-decreasing cardinality. The produced combinations c ′ = c ∩ r such c ′ were not in UC are called new combinations. Their atom size is initialized to c ′ .atsize = |c ′ |. See the "Parent computation" part of Algorithm 2.

We then remark that we only need to compute (or update) c.sup for combinations that include r, which we store in a set Incl. We also note that c.atsize needs to be computed when c is new and updated when c is the parent of a new combination. A second subtlety resides in computing (or updating) c.sup only when c is not covered that is when c.atsize (after computation) appears to be non-zero. As the computation of c.sup lists is the most heavy part of the computation, this is necessary to enable our complexity analysis. For that purpose, we scan Incl by nondecreasing cardinality so that the correct value of c.atsize is known when c is scanned similarly as in Algorithm 1. However, we avoid any useless computation when c.atsize is zero. Otherwise, we compute (or update) c.sup and decrease d.atsize by c.atsize from d ∈ c.sup for adequate d: if c and d where both in UC, this computation has already been made; it is only necessary when d is new or when d is the parent of c. We optionally maintain for each combination c a list c.cont that contain the list of sets r ∈ R that contain c (Such lists are not necessary for the computation but they are useful for loop detection as detailed in Appendix A.3). See the "Atom size computation" part of Algorithm 2.

A last critical point resides in the computation of c ′ .sup for each new combination c ′ . The c ′ .sup list can be obtained from c ′ .parent.sup by copying and also intersecting elements of c ′ .parent.sup with r. This is sufficient: for d ∈ UC such that c all sets r 0 , . . . , r ℓ are pairwise disjoint, the overlapping degree of the collection is k = 2 and this justifies the two lower-bounds indicated for NetPlumber in Table 1.

Future work

Our approach could be naturally integrated in the Veriflow [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF] framework both for speed-up and performance-guarantee considerations. Our ideas can also be integrated in the NetPlumber [START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF] framework (see the similar approach proposed in Appendix E). This would allow to enhance the emptiness tests performed within NetPlumber to guarantee polynomial time execution when the number of header classes is polynomially bounded. In the context of multi-ranges, the emptiness test of expressions is equivalent to the Klee measure problem which consists in computing the volume of a union of boxes. Indeed, expression r p \ ∪ i=1..p-1 r i is empty when the volume of the union of the boxes r 1 ∩ r p , . . . , r p-1 ∩ r p equals that of r p . According to recent work [START_REF] Chan | Klee's measure problem made easy[END_REF], the complexity of this problem is believed to be Θ(n d/2 ). It would be interesting to determine if such low complexity bounds extend to atom computation in the case of multi-ranges rules. R ′ (c ′ ) ⊆ R(c) ∪ {r}: the non-containers of c in R are also non-containers of c ′ in R ′ and if c was covered, so would be c ′ .

The following Lemma, which expresses any combination as a disjoint union of atoms justify the computation of atom cardinalities in Algorithm 2 by scanning c.sup lists for c ∈ UC. We can now state the following proposition about the guarantees of Algorithm 2. For a new combination c, the c.sup list is obtained from c.parent.sup and c.sup is updated similarly for c ∈ UC such that c ⊆ r. The correctness of this approach has already been discussed in Subsection 4. We develop here the key argument for ignoring a combination c ′ = c ∩ r when it is produced by several minimal elements c 1 , . . . , c i ∈ UC such that c j ∩ r = c ′ for j in 1..i. If this happens, we know that ∩ j∈1..i c j is not in UC, meaning that it is covered in R and so is c ′ ⊆ ∩ j∈1..i c j in R ∪ {r}. We can thus safely eliminate c ′ in the first phase of the algorithm. For the remaining new combinations c ′ , the parent c of c ′ is the unique combination c ∈ UC such that c ∩ r = c ′ and which is minimal for inclusion.

The correctness of the atom cardinality computation follows by induction on the number combinations in Incl processed so far in the corresponding for loop. It should be noted that in the case of (d, ℓ)-multi-ranges, we can distinguish in the analysis, the computation of |c| for new c that costs O(ℓ log ℓ) from other cardinality manipulations (subtractions and comparisons) that take O(ℓ). This allows to obtain the bound claimed in Theorem 1.

Theorem 2 results from iteratively applying Algorithm 2 (or Algorithm 1) for each set of R = {r 1 , . . . , r n }.

Proof of Theorem 2. From Proposition 2, the overall complexity of atom computation is O( i=1..n m i + a∈Ai |UC i (a)| log m) set operations where m i denotes the number of atoms in A({r 1 , . . . , r i-1 }) and A i denotes the atoms of A({r 1 , . . . , r i }) included in r i and UC i = UC({r 1 , . . . , r i }). We first consider the case where K is unbounded (it is possible to construct examples with m = n and K = Ω(2 n )). As we add a set to R, the number of atoms can only increase (each atom remains unchanged or is eventually split into two). We thus have

m i ≤ m and |A i | ≤ |{a ∈ A(R) | a ⊆ r i }|. Using |UC i (a)| ≤ m i+1 ≤ m, the overall complexity is O(nm + m log m i a∈A(r) |{r ∈ R | a ⊆ r}|) = O(nm + km 2 log
m) by definition of average overlap. The O(nm 2 ) bound is obtained by using Algortihm 1 instead of Algorithm 2.

We now derive a bound depending on the average overlapping degree K of combinations. Consider an atom a ∈ A i and an uncovered combination c ∈ UC i (a). We can associate a to an atom a.desc ⊆ a in A(R). As c is also a combination in C(R), we have c ∈ C(a.desc) where C(s) denotes the combinations of R containing s. As the atoms in A i are disjoint, the atoms a.desc for a ∈ A R are pairwise distinct. We thus have a∈Ai

A.3 Application to forwarding loop detection (Corollary 1)

Corollary 1 directly follows from the following claim and Theorem 1.

Claim 1. Given the collection R of rule sets of a network N , and for each atom a ∈ A(R) the list R(a) of sets in R that contain a, forwarding loop detection can be solved in O(kn G m) time where m = |A(R)| is the number of header classes, k is the average overlapping degree of R and n G is the number of nodes in N .

Proof. For that, we assume that each rule set r ∈ R is associated with the list L r of forwarding rules (r, a) that have rule set r. Each such rule is also supposed to be associated to the node u whose table contains it and the index i of the rule in T (u). Each list L s is additionally supposed to be sorted according to associated nodes. Such lists can easily be obtained by sorting the collection of all forwarding tables according to the predicate filters of rules.

The claim comes from the fact that uncovered combination in UC(R) represent atoms of A(R). It follows from testing for each header class a ∈ A(R) whether the graph G a = G h for all h ∈ a has a directed cycle. where ∞ i denotes the maximum possible value in field i, and H i..j = [0, ∞ i ] × • • • × [0, ∞ j ] denotes the multi-range of all possible values for fields i, . . . , j for 1 ≤ i ≤ j ≤ d.

The difficult input for Veriflow consists in a network with n = dp + 1 rules associated to the following multi-ranges: ) time for Veriflow. As this example has overlappingd degree 2, this justifies the two lower-bounds indicated for Veriflow in Table 1 for d-multi-ranges.

• r 0 = H 1..d , • r j i = H 1..i-1 × [a j ,
It is possible to adapt Veriflow to support general wildcard matching by considering each field bit as a field. The wildcard expressions r 0 = * ℓ , r 1 = 01 ℓ-1 , . . . , r ℓ = 0 ℓ-1 1 will then similarly generate all 2 ℓ/2 sub-classes obtained by concatenation of words 10 and 11. This justifies the two lower-bounds indicated for Veriflow in Table 1 for ℓ-wildcards.

the smallest collection of combinations of R that contains R ∪ {H} and that is weakly complete. Our work thus also provides an algorithm for computing such an optimal "weak completion". update a the global write pattern in the contexts of wildcard expressions and multi-ranges). We then recompute the inclusion relations between them and atom sizes in O(m 2 ) elementary set operations as in Algorithm 1. Combinations that are detected as covered are removed (or just saved apart for efficient backtracking). We finally obtain a valid representation of {p w (r) | r ∈ R P } since p w preserves intersection.

Note that write operations can only reduce the number of atoms. Forwarding loop detection can thus be performed within a factor n G p compared to the search procedure of Appendix E, that is in O(n 2 G nm 3 p) elementary set operations. This is again polynomial in terms of number of rules n, number of atoms m generated by the collection of rule sets, and the number p of write patterns that can be generated by write operations.

Figure 1 :

 1 Figure 1: Does this one node network have a forwarding loop ?

4 Figure 2 :

 42 Figure 2: Toy example of an 8-elements space H with a collection R = {r 1 , r 2 , r 3 , r 4 }.

Proposition 1 .

 1 The collection UC(R) := {c ∈ C(R) | a(c) = ∅} of uncovered combinations is in one-to-one correspondence with the atom collection A(R): each c ∈ UC(R) corresponds to the atom a(c). Reciprocally, each atom a is mapped to combination c(a).

Corollary 1 .

 1 If sets are represented by ℓ-wildcard expressions (resp. (d, ℓ)-multi-ranges), the representation can be computed in O(ℓ min(n + kK, nm)m) (resp. O(ℓ min(k log d m + kK, nm)m)) time. Application to forwarding loop detection Theorem 1 has the following consequences for forwarding loop detection. Given a network N with collection R of n rule sets with T ℓ -bounded representation, forwarding loop detection can be performed in O(T ℓ min(n+ kK log m, nm)m+ kn G m) time where m is the number of atoms in A(R), k is the overlapping degree of R and k (resp. K) is the average overlapping degree of R (resp. C(R)). If sets are represented by ℓ-wildcard expressions (resp. (d, ℓ)-multi-ranges), the representation can be computed in O(ℓ min(n+kK, nm)m+kn G m) (resp. O(ℓ min(k log d m + kK, nm)m + kn G m)) time.

Algorithm 1 :

 1 2). We thus first add to UC the combinations c ∩ r for c ∈ UC. As this may introduce covered combinations, we then compute the atom size c.atsize = |a(c)| for each combination c. It is then sufficient to remove any combination c with c.atsize = 0 to finally obtain UC(R ∪ {r}). This atom size computation is possible because we have d = ∪ c∈U C|c⊆d a(c) for all d ∈ UC. (see Lemma 2 in Appendix A.2). As this union is disjoint, we have |a(d)| = |d| -c∈U C|c d |a(c)|. We thus compute the inclusion relation between combinations and store in c.sup the combinations that strictly contain c. Initializing c.atsize to |c| for all c, we then scan all combinations c by nondecreasing cardinality (or any topological order for inclusion) and subtract c.atsize from d.atsize for each d ∈ c.sup. A simple proof by induction allows to prove that c.atsize = |a(c)| when c is scanned. The whole process in summarized in Algorithm 1. Procedure basicAdd(r, R, UC) UC ′ := UC ∪ {c ∩ r | c ∈ UC} For each c ∈ UC ′ do c.atsize := |c| c.sup := d ∈ UC ′ | c d For each c ∈ UC ′ in non-decreasing cardinality order do For each d ∈ c.sup do d.atsize := d.atsizec.atsize UC := UC ′ \ c ∈ UC ′ | c.atsize = 0 Add a set r to a collection R and update the collection UC = UC(R) of its uncovered combinations accordingly.

2 :

 2 ′ d ∩ r, we can consider c = c ′ .parent ∩ d. If c ∈ UC, c ′ .parent = c by minimality of c ′ .parent and we thus have d ∈ c ′ .parent.sup. The case where c / ∈ UC and d / ∈ c ′ .parent.sup cannot happen as it would imply that two different combinations c 1 = c ′ .parent and c 2 ⊆ c generate c ′ by intersection with r (c 1 ∩ r = c 2 ∩ r = c ′ ) and are both minimal for inclusion. In such case, c 1 ∩ c 2 was covered in R and so would be c ′ in Procedure add(r, R, UC = UC(R)) New := ∅; Incl := ∅; /* ----------------------Parent computation ----------------------*/ Inter := {c ∈ UC | c ∩ r = ∅} Sort Inter by non-decreasing cardinality. For each c ∈ Inter do c ′ := c ∩ r If c ′ / ∈ Incl then If c ′ / ∈ UC then UC := UC ∪ {c ′ }; New := New ∪ {c ′ }; c ′ .atsize := |c ′ |; c ′ .sup := {}; c ′ .cont := {} /* Updated later. */ c ′ .parent := c; c ′ .covered := f alse; Incl := Incl ∪ {c ′ }; else If c ′ .parent ⊆ c then c ′ .covered := true Remove from Incl, New and UC all c such that c.covered = true. /* ----------------------Atom size computation ----------------------*/ Sort Incl by non-decreasing cardinality. For each c ∈ Incl do If c.atsize > 0 then /* Adjust c.sup, c.cont and update d.atsize for impacted d c: */ If c ∈ New then c.parent.atsize := c.parent.atsizec.atsize c.sup := {c.parent} ∪ c.parent.sup c.cont := c.parent.cont c.sup := c.sup ∪ {d ∩ r | d ∈ c.sup and d ∩ r ∈ Incl \ {c}} c.cont := c.cont ∪ {r} For each d ∈ c.sup s.t. d ∈ New do d.atsize := d.atsizec.atsize /* ----------------------Remove covered combinations ----------------------*/ For each c ∈ Incl do Remove from c.sup any d such that d.atsize = 0. If c.atsize = 0 then UC := UC \ {c}; Incl := Incl \ {c}; If c ∈ New and c.parent.atsize = 0 then UC := UC \ {c.parent} Algorithm Add a set r to a collection R and update the collection UC of its uncovered combinations accordingly. R (and also in R ∪ {r}). That is why such combination c ′ are already discarded during parent computation. On the other hand, the list c.sup of a combination c ∈ UC can be updated by intersecting elements of c.sup with r: when c d ∩ r for c ⊆ r, we have c d. Finally, combinations c with c.atsize = 0 are discarded and removed from b.sup list of remaining combinations as detailed in the "Remove covered combinations" part of Algorithm 2. The main argument in the complexity analyzis of Algorithm 2 comes from bounding the size of each c.sup list by |UC(a(c))| (this is where the overlapping degree of C(R) is used). The number of elementary set operations performed is indeed O(m + a∈Ar UC ′ (a) log m) where m denotes the number of atoms of R, A r = {a ∈ A(R ′ ) | a ⊆ r} denotes the atoms of R ′ = R ∪ {r} included in r, and UC ′ (a) denotes the uncovered combinations of R ′ that contain a. A key step consists in proving |Inter| ≤ a∈Ar UC ′ (a) . The log m accounts for membership tests and add/remove operations on collections of combinations. In the case of ℓ-wildcard and (d, ℓ)-multi-ranges, this factor can be saved by storing collections of sets in tries rather than balanced binary search trees. With (d, ℓ)-multi-ranges, a segment tree allows to retrieve Inter in O(|Inter| + log d m) elementary set operations [2, 8].

Lemma 2 .

 2 Given a combination collection C ′ ⊆ C(R) containing UC(R), we have d = ∪ c∈C ′ |c⊆d a(c) for all d ∈ C ′ . This union is disjoint and we have |a(d)| = |d| -c∈C ′ |c d |a(c)|. Proof. Reminding that any combination d includes a(d) = d∩ ∩ r∈R\R(d) r , we have ∪ c∈C ′ |c⊆d a(c) ⊂ d. Conversely, consider h ∈ d. The sets of R containing h are R({h}), and we have h ∈ a(c) for c = ∩ r∈R({h}) r. As R(d) ⊆ R({h}) (the sets that contain d also contain h) and d = ∩ r∈R(d) r, we have c ⊆ d. Hence d ⊂ ∪ c∈C ′ |c⊆d a(c). This union is disjoint as each a(c) is either an atom or is empty.

Proposition 2 .

 2 Algorithm 2 allow to dynamically update the collection UC of uncovered combinations of a collection R using O(m + a∈Ar UC ′ (a) log m) elementary set operations when a rule r is added to R, where m denotes the number of atoms of R, A r = {a ∈ A(R ′ ) | a ⊆ r} denotes the atoms of R ′ included in r, and UC ′ (a) denotes the uncovered combinations of R ′ that contain a. More precisely, if the data-structures used for representing sets and collections of sets enable elementary set operations within time T set , p-collection operations within time T coll (p) and pintersection queries with overhead (T inter (p), T updt (m)), then the update of UC can be performed in O(T inter (m) + |A r | T updt (m) + (T set + T coll (m)) a∈Ar UC ′ (a) ) time. Proof. As discussed before the correctness of Algorithm 2 for obtaining uncovered combinations after adding set r to a collection R from UC = UC(R) and {c ∩ r | c ∈ UC} results from Lemma 1.

  Consider a newly created combination c. The initial value of c.atsize is |c|. Assuming that the correct value b.atsize has been obtained for b processed before c and c ∈ b.sup, |a(b)| has been subtracted from c.atsize and Lemma 2 implies that c.atsize = |a(c)| when we consider c in the for loop. For c already in UC before adding r and for b ⊆ c processed before c, b.atsize has been subtracted from c.atsize only for newly created b. For b ∈ UC, |a(b)| may have decreased but this difference is compensated by b ′ ∈New|b ′ b |a(b ′ )|. This is the reason why Algoritihm 2 updates only c.parent.atsize besides d ∈ c.sup such that d ∈ New. The correctness of the atom cardinality computation implies that all covered combinations are removed and the correctness of Algorithm 2 follows.We now analyze the complexity of Algorithm 2. The bound in terms of elementary set operations is obtained when balanced binary search tree (BST for short) are used to store the various collections of sets (i.e. UC, Incl, New and c.sup for c ∈ UC). When adding a set r, finding the combinations in UC that intersect r is a m-intersection query and can be performed in O(T inter (m) + |Inter|T set ) time or O(m log m) set operations using BST (sorting is only necessary in that case). The collection Incl is then constructed in O(|Inter| log m) operations with BST or O(|Inter|(T set + T coll (m))) with appropriate data-structures. Removing combinations c such that c.covered = true is just a matter of scanning Incl again and can be done within the same complexity. Let I denote the combinations included in Incl at that point (just before cardinality computations). The computation of c.sup for c ∈ I is done only when c.atsize > 0, i.e. only if c represents one of the atoms in A r . we thus have |I| ≤ |A r |. This requires at most O(|c.parent.sup|) operations. Note that for each uncovered combination d ∈ c.parent.sup yields at least one uncovered combination in c.sup (d itself or d ∩ r or both). We thus have |c.parent.sup| ≤ UC ′ (a(c)) . The overall computation of sup lists can thus be performed within O( a∈Ar UC ′ (a) log m) set operations with BST and O((T set +T coll (m)) a∈Ar UC ′ (a) ) time with appropriate data-structures. The computation of class cardinalities and the removal of covered combinations from the sup lists have same complexity. Removal of covered combinations from UC and Incl takes O(|A r |) collection operations and fits within the same complexity bound. Additional cost of |A r | T updt (m) is necessary when maintaining data-structures enabling efficient m-intersection queries. The whole algorithm can thus be performed in O(T inter (m) + |A r | T updt (m) + |Inter|(T set + T coll (m)) + (T set + T coll (m)) a∈Ar UC ′ (a) ) time or using O(m + |Inter| log m + a∈Ar UC ′ (a) log m) elementary set operations with BST. To achieve the proof of complexity of Algorithm 2, we show |Inter| ≤ a∈Ar UC ′ (a) . Consider a combination c ∈ UC that intersects r. Then c can be associated to an atom c.atm of A r included in c ∩ r (such atoms exist according to Lemma 2). For any atom a ∈ A r , let a.par denote the atom in A(R) that contains a (we have a = a.par or a = a.par ∩ r). Now for c ∈ Inter, consider the atom a = c.atm ∈ A r . As a.par ∈ A(R) is an atom and c ∈ C(R) is a combination intersecting a.par, we have a.par ⊆ c and c ∈ UC(a.par) is one of the combinations in UC(R) that contains a.par. For each such combination c, a(c) intersects r or r (or both), and c or c ∩ r is uncovered in R ′ = R ∪ {r}. Both contain a and we have |UC(a.par)| ≤ UC ′ (a) . We can thus write |Inter| = a∈Ar |{c ∈ Inter | c.atm = a}| ≤ a∈Ar |UC(a.par)| ≤ a∈Ar UC ′ (a) .

  |UC i (a)| ≤ a∈A(R)|a⊆ri |C(a)|. The overall complexity of atom computation is O(nm + log m a∈A(R) c∈C(a) |{i | a ⊆ r i }|) = O(nm + k log m a∈A(R) |C(a)|) = O(nm + kKm log m) by definition of overlapping degree and average overlapping degree respectively. The refined bound in terms of T set , T coll (m), T inter (m), T updt (m) is obtained similarly.

  G a is computed by merging the lists L s for s ∈ R(a) in time O(|R(a)| n G ). This graph has at most n G edges and cycle detection can be performed in O(n G ) time. The overall complexity follows from km = a∈A(R) |R(a)| by definition of k.Appendix B : Difficult inputs for previous works B.1 VeriflowVerfilow[START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF] represents the complementary of a multi-range r= [a 1 , b 1 ] × • • • × [a d , b d ]as the union of 2d -1 multi-ranges (at most):• [0, a 1 -1] × H 2..d and [b 1 + 1, ∞ 1 ] × H 2..d , • [a 1 , b 1 ] × [0, a 2 -1] × H 3..d and [a 1 , b 1 ] × [b 2 + 1, ∞ 2 ] × H 3..d , • • • • , • [a 1 , b 1 ] × • • • × [a d-1 , b d-1 ] × [0, a d -1] and [a 1 , b 1 ] × • • • × [a d-1 , b d-1 ] × [b d + 1, ∞ d ],

  a j ] × [b, b] d-i for i, j ∈ [1..d] × [1..p].Consider the sub-classes generated while computingr 0 ∩ ∩ i,j∈[1..d]×[1..p] r j i . The union of multi-ranges representing r j i contains in particular H 1..i-1 × [0, a j -1] × H i+1..d and H 1..i-1 × [a j + 1, ∞ i ] × H i+1..d .This implies that Veriflow generates on such an input all p d sub-classes of the formI 1 × • • • × I d with I i = [a j + 1, a j+1 -1]for some j ∈ [0, d] (we set a 0 = -1). Forwarding loop detection of an n G -node network thus requires Ω(p d n G ) = Ω(

Table 1 :

 1 Worst-case complexity of forwarding loop detection with n rules that generate m header classes in an n G -node network, for various rule set representations: T ℓ -bounded for intersection and cardinality computations in O(T ℓ ) time; ℓ-wildcard for wildcard expressions with ℓ letters; d-multi-rng. for multi-ranges in dimension d (with ℓ = O(d)). Additional hypothesis "ov. deg. k" stands for overlapping degree of rule sets bounded by k.

  such a data-structure D for subsets of H is T H -bounded when intersection and cardinality can be computed in time T H at most: given the representation of s, s ′ ∈ D, the representation of s∩s ′ ∈ D and the size |s| of s (as a binary big integer) can be computed within time T H . As big integers computed within time T H have O(T H ) bits, this implies |H| = 2 O(TH ) : the bound T H obviously depends on H. Intersection, inclusion test (s ⊆ s ′ ), cardinality computation (|s|) and cardinality operations (addition, subtraction and comparison) are called elementary set operations. Under the T

H -bounded hypothesis, all these operations can be performed in O(T H ) time (s

The various bounds for low overlapping degree of Theorem 1 results from applying iteratively Algorithm 2 for each set of R and by carefully bounding the sums of UC ′ (a) terms. Intuitively, each atom a generated by the collection R i of the first i sets of R can be associated to an atom a ′ of R such that UC ′ (a) ≤ |C(a ′ )| where C = C(R). As each atom is included in k sets of R at most, this allows to bound the overall sum of UC ′ (a) terms by kKm. Details are given in Appendix A.2.

Comparison with previous works

We give in Appendix C more details about "linear fragmentation", a phenomenon observed by Kazemian et al. [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF], and propose small overlap degree as a plausible cause. The notion of uncovered combination is linked to that of weak completion introduced by [START_REF] Boutier | Source-specific routing[END_REF] in the context of rule-conflict resolution as detailed in Appendix D. We now provide examples where use of set complement computation can lead to exponential blow-up in previous work.

Veriflow

Veriflow [START_REF] Khurshid | VeriFlow : Verifying Network-Wide Invariants in Real Time[END_REF] incrementally computes a partition into sub-classes that forms a refinement of the header classes: when a rule r is added, each sub-class c is replaced by c ∩ r and a partition of c \ r. Veriflow benefits from the hypothesis that headers can be decomposed into d fixed fields and that each rule set can be represented by a multi-range r

The intersection of two multi-ranges is obviously a multi-range. However, set difference is obtained by intersection with the complement which is represented as the union of up to 2d -1 multi-ranges. We prove in Appendix B.1 that successive difference with rules of the form [O, ∞] i-1 × [a j , a j ] × [b, b] d-i with 0 < a 1 , . . . , a p < b can generate Ω( n d d m d ) multi-ranges in the computations of Veriflow as indicated in Table 1.

HSA / NetPlumber

HSA/NetPlumber [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF][START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF] use clever heuristics to efficiently compute the set of headers H P than can traverse a given path P . An important one consists in lazy subtraction: set difference computations are postponed until the end of the path. For that purpose, this set H P is represented as a union of terms of the form s = c 0 \ ∪ i=1..p c i where the elementary sets c 0 , . . . , c p are represented with wildcards. The emptiness of such terms is regularly tested. A simple heuristic is used during the construction of the path: s is obviously empty if c 0 is included in c i for some i ≥ 1. But if the path loops, HSA has to develop the corresponding terms into a union of wildcards to determine if one of them may produce a forwarding loop. We now provide an example where this emptiness test can take exponential time. Consider a node whose forwarding table consists in ℓ + 1 rules with following rule sets:

.ℓ, and r ℓ+1 = * ℓ .

All rules are associated with the drop action except the last rule (with rule set r ℓ+1 ) whose action is to forward to the node itself. Such a forwarding table is depicted in Figure 1 for ℓ = 4. Starting a loop detection from that node, HSA detects a loop for headers in r ℓ+1 \ ∪ i=0..ℓ r i . The emptiness of this term is thus tested. For that purpose, HSA represents the complement of r i with 0

. Note that each of the ℓi wildcard expressions in that union have only one non- * letter. Distributivity is then used to compute r ℓ+1 \ ∪ i=0..ℓ r i as r 0 ∩ • • • ∩ r ℓ . After expanding the first j -1 intersections, HSA thus obtains a union of wildcards with j letters in {0, 1} and ℓj letters equal to * that has to be intersected with

In particular, this unions contains all strings with j letters equal to 0 and ℓj equal to * . All ℓ-letter strings with alphabet { * , 0} are produced during the computation which thus requires Ω(ℓ2 ℓ ) time. For testing a network with n G similar nodes, HSA thus requires time Ω(ℓn G 2 ℓ ). As

Appendix A : Proof details of Theorem 1 and Corollary 1

We present here a refined version of Theorem 1 with more hypothesis about the data-structure used to store a collection of sets. We first review these hypothesis and then the proof details of both versions.

A.1 Collection of sets representation

When manipulating a collection of p sets in D, we assume that their representations are stored in a collection data-structure allowing to dynamically add, remove or test membership of a set. Such operation are called p-collection operations. We can use a balanced binary search tree when comparisons according to a total order can be performed. Such comparison can usually be obtained by comparing directly the binary representations themselves of the set in linear time (and thus O(T H ) for sets with T H -bounded representation). It is considered as an elementary set operation.

In the case of wildcard expressions, the complexity of these operations can be reduced to O(ℓ) time by using a trie or a Patricia tree. Our algorithms will also make use of an operation similar to stabbing query that we call p-intersection query. It consists in producing the list L s of sets in a collection R of p sets that intersect a given query set s (L s = {r ∈ R | s ∩ r = ∅}). We additionally require that the list L s is topologically sorted according to inclusion. We say that p-intersection queries can be answered with overhead (T inter (p), T updt (p)) when dynamically adding or removing a set from the collection takes time T updt (p) at most and the p-intersection query for any set s ∈ D takes time T inter (p) + |L s |T H at most. In the case of d-dimensional multi-ranges, a segment tree allows to answer p-intersection queries with overhead (O(log d p), O(log d p)) [START_REF] Mark De Berg | Computational Geometry: Algorithms and Applications[END_REF][START_REF] Edelsbrunner | On the intersection of orthogonal objects[END_REF]. In the case of wildcard expressions, a trie or a Patricia tree allows to answer p-intersection queries with overhead (O(ℓp), O(ℓ)) (the whole tree has to be traversed in the worse case, but no sorting is necessary as the result is naturally obtained according to lexicographic order).

A.2 Incremental computation of atoms (Theorem 1)

The following is a refinement of Theorem 1 with respect to data-structures that provide time bounds on p-collection operations and p-intersection queries. For the sake of simplicity of asymptotic expressions, we make the very loose assumption that ℓ = o(m) and n ≤ m. (We are mainly interested in the case where m is large. Note also that examples with m < n would be very peculiar.)

Theorem 2. Given a space set H and a collection R of n subsets of H, the collection UC(R) of combinations that canonically represent the atoms generated by R can be incrementally computed with O(min(n+kK log m, km log m, nm)m) elementary set operations where m denotes the number of atoms generated by R, k denotes the overlapping degree of R, k denotes the average overlapping degree of R and K denotes the average overlapping degree of C(R).

More precisely, if the data-structures used for representing sets and collections of sets enable elementary set operations within time T set , p-collection operations within time T coll (p) and pintersection queries with overhead (T inter (p), T updt (m)), then the representation of the atoms generated by R can be computed in O(nT inter (m) + kmT updt (m) + min(kK, km)m(T set + T coll (m))) time.

The following lemma formally states that uncovered combinations of R ∪ {r} can be obtained from UC(R) and justifies the overall approach of Algorithm 2.

Lemma 1. Given a new rule r ⊆ H, the collection UC(R ′ ) of uncovered combinations of R ′ = R ∪ {r} can be obtained by intersecting uncovered combinations in UC(R) with r. More precisely, we have

To conclude, it is thus sufficient to show that c is uncovered in R. This follows from c ′ ⊆ c and

Appendix B.2 : HSA/NetPlumber approach

The NetPlumber approach could be generalized to more general types of rules. However, we show that the simple heuristic for emptiness tests described in Section 5.2 is not sufficient. We provide an example where the HSA/NetPlumber approach generates an exponential number of paths while the number of classes is linear if it relies solely on this heuristic. Consider header space H = {1..n} and the following n + 1 rule sets: r 1 = {1}, . . . , r n = {n} and r n+1 = H. Consider a network N with n G = n(n + 1) nodes. Each node u i,j for 0 ≤ i ≤ n and 1 ≤ j ≤ n has table T (u i,j ) = (r i+1 , F wdD i+1,1 ), . . . , (r n , F wdD i+1,n ), (r n+1 , F wdD i+1,n ) where action F wdD i,j indicates to forward packets to node u i,j for i ≤ n and to drop packets for i = n + 1. Starting from u 0,1 , the HSA approach generates a path for each combination

This path goes through u 0,1 , u 1,i1 , . . . , u p,ip and then through u p+1,n , . . . , u n,n . It is constructed at least for term r i1 ∩ • • • ∩ r ip \ ∪ j / ∈{i1,...,ip} r j . The heuristical emptiness test of NetPlumber does not detect that it is empty since r i1 ∩ • • • ∩ r ip contains j for j / ∈ {i 1 , . . . , i p } and it is not included in r j . The number of paths generated is thus at least 1≤p≤n n p = 2 n -1. However, the header classes are all singletons of H and their number is m = n. Note the high overlapping degree k = n of this collection of rule sets.

Appendix C : Linear fragmentation versus overlapping degree

Interestingly, a complexity analysis of HSA loop detection is given in the technical report [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] under an assumption called "linear fragmentation". This assumption, which is based on empirical observations, basically states that there exists a constant c such that a given routing path P will branch at most c times. More precisely it states that a term s = c 0 \ ∪ i=1..p c i in the expression representing H P , the set of headers that can follow P , intersects at most c of the rule sets in the table of the end node of P . A simple induction allows to bound the number of terms generated by all paths of p hops from a given source by c p n. Under linear-fragmentation, the time complexity of HSA loop detection (excluding emptiness tests) is thus proved to be O(c DG D G n 2 m G ) in [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] where D G is the diameter of network graph G, n the number of rules, and m G the number of ports in G (in our simplified model each node has a single input port and m G = n G the number of nodes in G). It is then argued that in practice the constant c gets smaller as the length p of the path considered increases and that practical loop detection has complexity O(D G n 2 m G ) as claimed in [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF]. However, it is not rigorous to neglect the (exponential) c DG factor under the sole linear-fragmentation hypothesis.

Additionally, we think that low overlapping degree provides a simple explanation for the phenomenon observed by Kazemian et al.: as the path length increases, the terms representing the header that can traverse the path result from the intersection of more rules and become less likely to intersect other rules when overlapping degree is limited. Moreover, bounded overlapping degree k implies that the number of terms generated by HSA within p hops is bounded by O(n min(p,k) ). The total number of terms generated is thus bounded by O(n G n k ). This guarantees that all HSA computations besides emptiness tests remain polynomial for constant k. In contrast, with the example provided in Appendix B.2 (which has unbounded overlapping degree), the HSA approach can generate exponentially many paths compared to the number of header classes in the context of general rules.

Appendix D : Related notion of weak completeness

In the context of resolution of conflicts between rules, Boutier and Chroboczek [START_REF] Boutier | Source-specific routing[END_REF] introduce the concept of weak completeness: a collection R is weakly complete iff for any sets r, r ′ ∈ R, we have r ∩ r ′ = ∪ r ′′ ⊆r∩r ′ r ′′ . They show that this is a minimal necessary and sufficient condition for all rule conflicts to be solved when priority of rules extends inclusion (i.e. r has priority over r ′ when r r ′ ). Interestingly, we can make the following connection with this work: given a combination collection

) This allows to show that UC(R) is weakly complete. It is indeed

Appendix E : Topological header classes

Inspired by the HSA/NetPlumber [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF][START_REF] Kazemian | Real Time Network Policy Checking using Header Space Analysis[END_REF] approach, we can refine the definition of header classes. We fix a source node s. A forwarding path P originating from s is a sequence (u 0 , i 0 ), . . . , (u p , i p ) where u 0 , . . . , u p are the nodes encountered along the path and i 0 , . . . , i p are the indexes of the forwarding rules followed: rule i 0 is applied at node u 0 = s, then rule i 1 at node u 1 and so on. We then define two headers as topologically equivalent from s if they follow the same forwarding paths. Note that each topological class for that relation corresponds to a unique path (if some headers match two distinct rules at a node, the first one is followed).

We now show that the topological classes (from s) are indeed certain atoms of partial collections of rule sets. Given a forwarding path P = (u 0 , i 0 ), . . . , (u p , i p ). Let R j = {r j 1 , . . . , r j nj } denote the collection of rule sets of node u j where r j 1 , . . . , r j nj corresponds to the order of the n j rules in T (u j ). Let also R j i = {r j 1 , . . . , r j i } denote the partial collection of the i first rule sets. The set of headers that can follow rule i in node u j is

As the only positive terms of this intersection are r i0 , . . . , r ip , cl(P ) is indeed the atom a(c P ) associated to the combination c P = r i0 , . . . , r ip in

for each path. Our framework can thus be applied to test whether the combination c P associated to any path P does correspond to a topological class by testing the emptiness of a(c P ). We detect a forwarding loop (starting from s) as soon as a path P reaches a former node of P .

Our incremental algorithm is well suited for incrementally augmenting the collection of rules as we progress along the path. Using a persistent style implementation for the data structure storing collections (as classically done when implementing binary search trees in functional languages), we can step back at a branching node v and follow a different branch without having to recompute the collection of atoms generated by the path up to v. The collection is also incrementally augmenting as we progress in routing table of a branching node v and explore different paths. This allows to efficiently perform a search of the graph in a depth first search manner.

It is important to note that two different explored paths P and Q are associated to different combinations c P = c Q . To see this, suppose that P and Q branch at node u: P follows rule r i of T (u) while Q follows r j with i < j. After (u, i), path Q cannot follow any rule associated with set r i due to emptiness tests. This ensures that the number of paths generated is bounded. Similarly to the proof of Proposition 2 and Theorem 2, each combination c P generated by a path P can be associated to an atom of A(R) where R denotes the collection of all rule sets in the network. The number of topological classes is thus always bounded by m = |A(R)|. However, for a given collection R of rule sets generating m atoms, one can easily produce a network topology with m topological classes.

When performing the search from source s, the number of paths (and prefixes of paths) generated is at most a∈A(R) |UC(a)| = Km ≤ nm where UC = UC(A) are the uncovered combinations generated by R. As each path prefix accounts for one call of Algorithm 1, this search thus costs O(nm 3 ) elementary set operations. Repeating this for all possible source nodes, we get an overall complexity of O(n G nm 3 ) operations for forwarding loop detection. (This complexity analysis can be refined in terms of overlapping degree and optimized by using potentially Algorithm 2 instead of Algorithm 1.)

Note that the number of paths explored could grow exponentially without appropriate emptiness tests as exemplified in Appendix B.2. Although this approach remains polynomial in terms of n and m, its complexity guaranties are less interesting than what we propose in Section 4. However, it allows to extend our framework with write actions as detailed in the next appendix.

Appendix F : Write actions

First note that allowing any write operations and variable header length (by allowing to push subheaders) make the forwarding loop detection problem undecidable as we can then easily simulate a pushdown automaton with several stacks. However, in the context of MPLS, it is natural to allow to push and pop MPLS headers (and only that type). In the classical functioning of MPLS, each push or swap action always writes a fixed label value, rules taking into account the MPLS header always have higher priority and base their decisions on the outermost label only (and no other field). In that case, paths with MPLS forwarding can be factored out by adding shortcut edges (from the first push action to last pop action) in a preliminary step which should also include loop detection for each label value pushed somewhere in the network. This can clearly be performed in polynomial time. We reserve the study of more general write action with push and pop actions for future work. However, we now sketch how to handle write actions in the context of fixed length headers.

We suppose that a forwarding rule applied to a packet can perform a write action before forwarding the packet. We typically think of write actions that write some fixed values at fixed positions. We then see a write action as a projection of the header space in a smaller sub-space. More generally, we assume that each write action w is associated with a function p w : H → H with the following properties (we set p w (s) = {p w (h) | h ∈ s} for s ⊆ H) :

• intersection preservation: for s ∩ s ′ = ∅, we have p w (s ∩ s ′ ) = p w (s) ∩ p w (s ′ );

• two consecutive write operations w and w ′ are equivalent to a single write operation w ′′ with p w ′′ = p w ′ • p w , w ′′ is then called a write pattern assumed to be efficiently computable.

We do not need to formally assume that p w is a projection (i.e. p w • p w = p w ) although this is typically the case. We additionally make the following assumption with respect the data-structure D used for sets:

• p w (s) is in D and can be computed in O(T ℓ ) time.

All the above requirements are clearly met for any write action (of fixed bits at fixed positions) in the context of wildcard expressions. In the context of prefix matching we can only allow to write a prefix of bits to ensure that a set represented by a prefix is always mapped to a set that can be represented by a prefix. We can generalize this to the context of interval matching when low order bits are ordered first (little-endian order). We still represent a set s with an interval [a, b] but we additionally consider a write pattern w and the number i of bits of w written so far. The write pattern w is simply an integer with same bit representation as a and b. To test whether a header h is in s, we first check that its i lowest bits are identical to those of w, then shift a, b, and h by i bits to erase low order bits, obtaining a ′ , b ′ , h ′ respectively and test whether a ′ ≤ h ′ ≤ b ′ . Other set operations are handled similarly. Note that the computation of p w ′ ([a, b]) just requires to update the write pattern which can be globally shared for a collection of sets. A similar trick can be used with wildcard expressions. In the context of multi-ranges, our model thus enables prefix writes on one or several fields. (This includes in particular writing of exact values in one or several fields.)

Forwarding loop detection can then be performed using the approach detailed in Appendix E by additionally decorating each node of an explored path with a write pattern w equivalent to the sequence of write actions performed so far along the path. A forwarding loop is detected when a former node u associated to write pattern w is reached again with same write pattern w ′ = w while growing a path P containing u. If the number the of write patterns that can be generated by combining various write actions is bounded by p, then the length of each path is at most n G p.

Our algorithms for incremental atom computation can easily be extended in that context: when a write action w is performed when growing a path P , we update the collection of uncovered combinations representing the atoms of the current collection R P of rule sets encountered along P as follows. Each combination c is replaced by p w (c) (which typically amounts to a single