Efficient Verification of Network Fault Tolerance via CounterexampleGuided Refinement
Abstract
We show how to verify that large data center networks satisfy key properties such as allpairs reachability under a bounded number of faults. To scale the analysis, we develop algorithms that identify network symmetries and compute small abstract networks from large concrete ones. Using counterexample guided abstraction refinement, we successively refine the computed abstractions until the given property may be verified. The soundness of our approach relies on a novel notion of network approximation: routing paths in the concrete network are not precisely simulated by those in the abstract network but are guaranteed to be “at least as good.” We implement our algorithms in a tool called Origami and use them to verify reachability under faults for standard data center topologies. We find that Origami computes abstract networks with 1–3 orders of magnitude fewer edges, which makes it possible to verify large networks that are out of reach of existing techniques.
1 Introduction
Most networks decide how to route packets from point A to B by executing one or more distributed routing protocols such as the Border Gateway Protocol (BGP) and Open Shortest Path First (OSPF). To achieve endtoend policy objectives related to cost, load balancing, security, etc., network operators author configurations for each router. These configurations control various aspects of the route computation such as filtering and ranking route information received from neighbors, information injection from one protocol to another, and so on.
This flexibility, however, comes at a cost: Configuring individual routers to enforce the desired policies of the distributed system is complex and errorprone [15, 21]. The problem of configuration is further compounded by three challenges. The first is network scale. Large networks such as those of cloud providers can consist of millions of lines of configuration spread across thousands of devices. The second is that operators must account for the interaction with external neighbors who may sent arbitrary routing messages. Finally one has to deal with failures. Hardware failures are common [14] and lead to a combinatorial explosion of different possible network behaviors.
To combat the complexity of distributed routing configurations, researchers have suggested a wide range of network verification [2, 13, 25] and simulation [11, 12, 23] techniques. These techniques are effective on small and mediumsized networks, but they cannot analyze data centers with 1000 s of routers and all their possible failures. To enable scalable analyses, it seems necessary to exploit the symmetries that exist in most large real networks. Indeed, other researchers have exploited symmetries to scale verification in the past [3, 22]. However, it has never been possible to account for failures, as they introduce asymmetries that change routing behaviors in unpredictable ways.
To address this challenge, we develop a new algorithm for verifying reachability in networks in the presence of faults, based on the idea of counterexampleguided abstraction refinement (CEGAR) [5]. The algorithm starts by factoring out symmetries using techniques developed in prior work [3] and then attempts verification of the abstract network using an SMT solver. If verification succeeds, we are done. However, if verification fails, we examine the counterexample to decide whether we have a true failure or we must refine the network further and attempt verification anew. By focusing on reachability, the refinement procedure can be accelerated by using efficient graph algorithms, such as min cut, to rule out invalid abstractions in the middle of the CEGAR loop.
We prove the correctness of our algorithm using a new theory of faulty networks that accounts for the impact of all combinations of k failures. Our key insight is that, while routes computed in the abstract network may not simulate those of the concrete network exactly, under the right conditions they are guaranteed to approximate them. The approximation relation between concrete and abstract networks suffices to verify key properties such as reachability.
We implemented our algorithms in a tool called Origami and measured their performance on common data center network topologies. We find that Origami computes abstract networks with 1–3 orders of magnitude fewer edges. This reduction speeds verification dramatically and enables verification of networks that are out of reach of current stateoftheart tools [2].
2 Key Ideas
The goal of Origami is to speed up network verification in the presence of faults, and it does so by computing small, abstract networks with similar behavior to a given concrete network.
Unfortunately, we run into two significant problems when defining abstractions in this manner in the presence of faults. First, the concrete nodes of Fig. 1a have at least 2 disjoint paths to the destination whereas abstract nodes of Fig. 1b have just one path to the destination, so the abstract network does not preserve the desired fault tolerance properties. Second, consider Fig. 1c, which illustrates how the routing decisions change when a failure occurs. Here, the nodes (\(b_1\) in particular) no longer route “in the same direction” as the original network or its abstraction. Hence the invariant connecting concrete and abstract networks is violated.
Lossy Compression. To achieve compression given a bounded number of link failures, we relax the notion of similarity between concrete and abstract nodes: A node in the abstract network may merely approximate the behavior of concrete nodes. This makes it possible to compress nodes that, in the presence of failures, may route differently. In general, when we fail a single link in the abstract network, we are overapproximating the failures in the concrete network by failing multiple concrete links, possibly more than desired. Nevertheless, the paths taken in the concrete network can only deviate so much from the paths found in the abstract network:
Property 1
If a node has a route to the destination in the presence of k link failures then it has a route that is “at least as good” (as prescribed by the routing protocol) in the presence of \(k'\) link failures for \(k' < k\).
This relation suffices to verify important network reliability properties, such as reachability, in the presence of faults. Just as importantly, it allows us to achieve effective network compression to scale verification.
Revisiting our example, consider the new abstract network of Fig. 1d. When the link between \(\widehat{b}_{12}\) and \(\widehat{d}\) has failed, \(\widehat{b}_{12}\) still captures the behavior of \(b_1\) precisely. However, \(b_2\) has a better (in this case better means shorter) path to d. Despite this difference, if the operator’s goal was to prove reachability to the destination under any single fault, then this abstract network suffices.
From Specification to Algorithm. It is not too difficult to find abstract networks that approximate a concrete network; the challenge is finding a valid abstract network that is small enough to make verification feasible and yet large enough to include sufficiently many paths to verify the given fault tolerance property. Rather than attempting to compute a single abstract network with the right properties all in one shot, we search the space of abstract networks using an algorithm based on counterexample guided abstraction refinement [5].
The CEGAR algorithm begins by computing the smallest possible valid abstract network. In the example above, this corresponds to the original compressed network in Fig. 1b, which faithfully approximates the original network when there are no link failures. However, if we try to verify reachability in the presence of a single fault, we will conclude that nodes \(\widehat{b}\) and \(\widehat{a}\) have no route to the destination when the link between \(\widehat{b}\) and \(\widehat{d}\) fails. The counterexample due to this failure could of course be spurious (and indeed it is). Fortunately, we can easily distinguish whether such a failure is due to lack of connectivity or an artifact of overabstracting, by calculating the number of corresponding concrete failures. In this example a failure on the link \({\langle {\widehat{b},\widehat{d}}\rangle }\) corresponds to 3 concrete failures. Since we are interested in verifying reachability for a single failure this cannot constitute an actual counterexample.
The next step is to refine our abstraction by splitting some of the abstract nodes. The idea is to use the counterexample from the previous iteration to split the abstract network in a way that avoids giving rise to the same spurious counterexample in the next iteration (Sect. 5). Doing so results in the somewhat larger network of Fig. 1d. A second verification pass over this larger network takes longer, but succeeds.
3 The Network Model
Though there are a wide variety of routing protocols in use today, they share a lot in common. Griffin et al. [16] showed that protocols like BGP and others solve instances of the stable paths problem, a generalization of the shortest paths problem, and Sobrinho [24] demonstrated their semantics and properties can be modelled using routing algebras. We extend these foundations by defining stable paths problems with faults (SPPFs), an extension of the classic Stable Paths Problem that admits the possibility of a bounded number of link failures. In later sections, we use this network model to develop generic network compression algorithms and reason about their correctness.
Stable Path Problems with Faults \(\mathbf{( }{{\mathbf {\mathsf{{SPPF}}}}}\)s): An SPPF is an instance of the stable paths problem with faults. Informally, each instance defines the routing behavior of an operational network. The definition includes both the network topology as well as the routing policy. The policy specifies the way routing messages are transformed as they travel along links and through the userconfigured import and export filters/transformers of the devices, and also how the preferred routes are chosen at a given device. In our formulation, each problem instance also incorporates a specification of the possible failures and their impact on the routing solutions.
 1.
A graph \(G={\langle {V,E}\rangle }\) denoting the network topology.
 2.
A set of “attributes” (i.e., routing messages) \(A_{\infty }=A \cup \{\infty \}\) that may be exchanged between devices. The symbol \(\infty \) represents the absence of a route.
 3.
A destination \(d \in V\) and its initial route announcement \(a_d \in A\). For simplicity, each SPPF has exactly one destination (d). (To model a network with many destinations, one would use a set of SPPFs.)
 4.
A partial order \(\mathord {\prec } \subseteq A_{\infty } \times A_{\infty }\) ranks attributes. If \(a \prec b\) then we say route a is preferred over route b. Any route \(a \in A\) is preferred to no route (\(a \prec \infty \)).
 5.
A function \(\mathsf {trans}:E \rightarrow A_{\infty } \rightarrow A_{\infty }\) that denotes how messages are processed across edges. This function models the route maps and filters that transform route announcements as they enter or leave routers.
 6.
A bound k on the maximum number of link failures that may occur.
SPPF Solutions: In a network, routers will repeatedly exchange messages, applying their transfer functions to neighbor routes and selecting a current best route based on the preference relation, until the network reaches a fixpoint (stable state). Interestingly, Griffin et al. [16] showed that all routing solutions can be described via a set of local stability constraints. We exploit this insight to define a series of logical constraints that capture all possible routing behaviors in a setting that includes link failures. More specifically, we define a solution (aka, stable state) \(\mathcal {S}\) of an SPPF to be a pair \({\langle {\mathcal {L},\mathcal {F}}\rangle }\) of a labelling \(\mathcal {L}\) and a failure scenario \(\mathcal {F}\). The labelling \(\mathcal {L}\) is an assignment of the final attributes to nodes in the network. If an attribute a is assigned to node v, we say that node has selected (or prefers) that attribute over other attributes available to it. The chosen route also determines packet forwarding. If a node X selects a route from neighbor Y, then X will forward packets to Y. The failure scenario \(\mathcal {F}\) is an assignment of 0 (has not failed) or 1 (has failed) to each edge in the network.
4 Network Approximation Theory
Given a concrete SPPF and an abstract \(\widehat{\mathsf {SPPF}}\), a network abstraction is a pair of functions (f, h) that relate the two. The topology abstraction \(f: V \rightarrow \widehat{V}\) maps each node in the concrete network to a node in the abstract network, while the attribute abstraction \(h: A_{\infty } \rightarrow \widehat{A}_{\infty }\) maps a concrete attribute to an abstract attribute. The latter allows us to relate networks running protocols where nodes may appear in the attributes (e.g. as in the \(\mathrm {Path}\) component of BGP).
The goal of Origami is to compute compact \(\widehat{\mathsf {SPPFs}}\) that may be used for verification. These compact \(\widehat{\mathsf {SPPFs}}\) must be closely related to their concrete counterparts. Otherwise, properties verified on the compact \(\widehat{\mathsf {SPPF}}\) will not be true of their concrete counterpart. Section 4.1 defines label approximation, which provides an intuitive, highlevel, semantic relationship between abstract and concrete networks. We also explain some of the consequences of this definition and its limitations. Unfortunately, while this broad definition serves as an important theoretical objective, it is difficult to use directly in an efficient algorithm. Section 4.2 continues our development by explaining two wellformedness requirements of network policies that play a key role in establishing label approximation indirectly. Finally, Sect. 4.3 defines effective Open image in new window approximation for wellformed SPPFs. This definition is more conservative than label approximation, but has the advantage that it is easier to work with algorithmically and, moreover, it implies label approximation.
4.1 Label Approximation
Intuitively, we say the abstract \(\widehat{\mathsf {SPPF}} \) labelapproximates the concrete \(\textsf {SPPF} \) when \(\textsf {SPPF} \) has at least as good a route at every node as \(\widehat{\mathsf {SPPF}} \) does.
Definition 1
(Label Approximation). Consider any solutions \(\mathcal {S}\) to \(\textsf {SPPF} \) and \(\widehat{\mathcal {S}}\) to \(\widehat{\mathsf {SPPF}} \) and their respective labelling components \(\mathcal {L}\) and \(\widehat{\mathcal {L}}\). We say \(\widehat{\mathsf {SPPF}} \) labelapproximates \(\textsf {SPPF} \) when \(\forall u \in V.~ h(\mathcal {L}(u)) \preceq \widehat{\mathcal {L}}(f(u))\).
If we can establish a label approximation relation between a concrete and an abstract network, we can typically verify a number of properties of the abstract network and be sure they hold of the concrete network. However, the details of exactly which properties we can verify depend on the specifics of the preference relation (\(\prec \)). For example, in an OSPF network, preference is determined by weighted path length. Therefore, if we know an abstract node has a path of weighted length n, we know that its concrete counterparts have paths of weighted length of at most n. More importantly, since “no route” is the worst route, we know that if a node has any route to the destination in the abstract network, so do its concrete counterparts.
Limitations. Some properties are beyond the scope of our tool (independent of the preference relation). For example, our model cannot reason about quantitative properties such as bandwidth, probability of congestion, or latency.
4.2 WellFormed SPPFs
Monotonicity and isotonicity properties are often cited [7, 8] as desirable properties of routing policies because they guarantee network convergence and prevent persistent oscillation. In practice too, prior studies have revealed that almost all real network configurations have these properties [13, 19].
In our case, these properties help establish additional invariants that tie the routing behavior of concrete and abstract networks together. To gain some intuition as to why, consider the networks of Fig. 2. The concrete network on the left runs BGP with the routing policy that node \(c_1\) (and \(c_2\)) prefers to route through node g instead of a, and that \(b_1\) drops announcements coming from \(b_2\). In this scenario, the similarly configured abstract node \(\widehat{b}_{12}\) can reach the destination—it simply takes a route that happens to be less preferred by \(\hat{c}_{12}\) than it would if there had been no failure. However, in the concrete analogue, \(b_1\), is unable to reach the destination because \(c_1\) only sends it the route through \(b_2\), which it cannot use. In this case, the concrete network has more topological paths than the abstract network, but, counterintuitively, due to the network’s routing policy, this turns out to be a disadvantage. Hence having more paths does not necessarily make nodes more accessible. As a consequence, in general, abstract networks cannot soundly overapproximate the number of failures in a concrete network—an important property for the soundness of our theory.
The underlying issue here is that the networks of Fig. 2 are not isotonic: suppose \(\mathcal {L}'(c_1)\) is the route from \(c_1\) to the destination through node a, we have that \(\mathcal {L}(c_1) \prec \mathcal {L}'(c_1)\) but since the transfer function over \({\langle {b_1,c_1}\rangle }\) drops routes that have traversed node \(b_2\), we have that \(\mathsf {trans}({\langle {b_1,c_1}\rangle }, \mathcal {L}(c_1)) \not \prec \mathsf {trans}({\langle {b_1,c_1}\rangle },\mathcal {L}'(c_1))\). Notice that \(\mathcal {L}'(c_1)\) is essentially the route that the abstract network uses i.e. \(h(\mathcal {L}'(c_1)) = \widehat{\mathcal {L}}(\hat{c}_{12})\), hence the formula above implies that \(h(\mathcal {L}(b_1)) \not \prec \ \widehat{\mathcal {L}}(\hat{b}_{12})\) which violates the notion of label approximation. Fortunately, if a network is strictly monotonic and isotonic, such situations never arise. Moreover, we check these properties via an SMT solver using a local and efficient test.
4.3 Effective SPPF Approximation
We seek abstract networks that labelapproximate given concrete networks. Unfortunately, to directly check that a particular abstract network label approximates a concrete network one must effectively compute their solutions. Doing so would defeat the entire purpose of abstraction, which seeks to analyze large concrete networks without the expense of computing their solutions directly.
 1.
The topology abstraction conforms to the \(\forall \exists \mathsf {abstraction} \) condition; this requires that there is an abstract edge \((\widehat{u},\widehat{v})\) iff for every concrete node u such that \(f(u) = \widehat{u}\) there is some node v such that \(f(v) = \widehat{v}\) and \((u,v) \in E\).
 2.The abstraction preserves the rank of attributes (rankequivalence):$$\begin{aligned} \forall a, b.~ a \prec b \iff h(a) ~\widehat{\prec }~ h(b) \end{aligned}$$
 3.The transfer function and the abstraction functions commute (transequivalence):$$\begin{aligned} \forall e,a.~ h(\mathsf {trans}(e,a)) = \widehat{\mathsf {trans}}(f(e),h(a)) \end{aligned}$$
We prove that when these conditions hold, we can approximate any solution of the concrete network with a solution of the abstract network.
Theorem 1
Given a wellformed SPPF and its effective approximation \(\widehat{\mathsf {SPPF}} \), for any solution \(\mathcal {S}\in \) SPPF there exists a solution \(\widehat{\mathcal {S}}\in \widehat{\mathsf {SPPF}} \), such that their labelling functions are label approximate.
5 The Verification Procedure
 1.
Search the set of candidate refinements for the smallest plausible abstraction.
 2.
If the candidate abstraction satisfies the desired property, terminate the procedure. (We have successfully verified our concrete network.)
 3.
If not, examine whether the returned counterexample is an actual counterexample. We do so, by computing the number of concrete failures and check that it does not exceed the desired bound of link failures. (If so, we have found a property violation.)
 4.
If not, use the counterexample to learn how to expand the abstract network into a larger abstraction and repeat.
Both the search for plausible candidates and the way we learn a new abstraction to continue the counterexampleguided loop are explained below.
5.1 Searching for Plausible Candidates
Though we might know an abstraction is not sufficient to verify a given fault tolerance property, there are many possible refinements. Consider, for example, Fig. 3(a) presents a simple concrete network that will tolerate a single link failure, and Fig. 3(b) presents an initial abstraction. The initial abstraction will not tolerate any link failure, so we must refine the network. To do so, we choose an abstract node to divide into two abstract nodes for the next iteration. We must also decide which concrete nodes correspond to each abstract node. For example, in Fig. 3(c), node \(\hat{a}\) has been split into \(\hat{a}_{13}\) and \(\hat{a}_{24}\). The subscripts indicate the assignment of concrete nodes to abstract ones.
A significant complication is that once we have generated a new abstraction, we must check that it continues to satisfy the effective approximation conditions, and if not, we must do more work. Figure 3(c) satisfies those conditions, but if we were to split \(\hat{a}\) into \(\hat{a}_{12}\) and \(\hat{a}_{34}\) rather than \(\hat{a}_{13}\) and \(\hat{a}_{24}\), the forallexists condition would be violated—some of the concrete nodes associated with \(\hat{b}\) are connected to the concrete nodes in \(\hat{a}_{12}\) but not to the ones in \(\hat{a}_{34}\) and vice versa. To repair the violation of the forallexists condition, we need to split additional nodes. In this case, the \(\hat{b}\) node, giving rise to diagram Fig. 3(d).
Overall, the process of splitting nodes and then recursively splitting further nodes to repair the forallexists condition generates many possible candidate abstractions to consider. A key question is which candidate should we select to proceed with the abstraction refinement algorithm?
One consideration is size: A smaller abstraction avoids taxing the verifier, which is the ultimate goal. However, there are many small abstractions that we can quickly dismiss. Technically, we say an abstraction is plausible if all nodes of interest have at least \(k+1\) paths to the destination. Implausible abstractions cause nodes to become unreachable with k failures. To check whether an abstraction is plausible, we compute the mincut of the graph. Figure 3(d) is an example of an implausible abstraction that arose after a poorlychosen split of node \(\hat{a}\). In this case, no node has 2 or more paths to the destination and hence they might not be able to reach the destination when there is a failure.
Clearly verification using an implausible abstraction will fail. Instead of considering such abstractions as candidates for running verification on, the refinement algorithm tries refining them further. A key decision the algorithm needs to make when refining an abstraction is which abstract node to split. For instance, the optimal refinement of Fig. 3(b) is Fig. 3(c). If we were to split node \(\hat{b}\) instead of \(\hat{a}\) we would end up with a suboptimal (in terms of size) abstraction. Intuitively, splitting a node that lies on the mincut and can reach the destination (e.g. \(\hat{a}\)) will increase the number of paths that its neighbors on the unreachable part of the mincut (e.g. \(\hat{b}\)) can use to reach the destination.
To summarize, the search for new candidate abstractions involves (1) splitting nodes in the initial abstraction, (2) repairing the abstraction to ensure the forallexists condition holds, (3) checking that the generated abstraction is plausible, and if not, (4) splitting additional nodes on the min cut. This iterative process will often generate many candidates. The breadth parameter of the search bounds the total number of plausible candidates we will generate in between verification efforts. Of all the plausible candidates generated, we choose the smallest one to verify using the SMT solver.
5.2 Learning from Counterexamples
Any nodes of an abstraction that have a min cut of less than \(k+1\) definitely cannot tolerate k faults. If an abstraction is plausible, it satisfies a necessary condition for sourcedestination connectivity, but not a sufficient one—misconfigured routing policy can still cause nodes to be unreachable by modifying and/or subsequently dropping routing messages. For instance, the abstract network of Fig. 3c is plausible for one failure, but if \(\widehat{b}\)’s routing policy blocks routes of either \(\widehat{a}_{13}\) or \(\widehat{a}_{24}\) then the abstract network will not be 1fault tolerant. Indeed, it is the complexity of routing policy that necessitates a heavyweight verification procedure in the first place, rather than a simpler graph algorithm alone.
In a plausible abstraction, if the verifier computes a solution to the network that violates the desired faulttolerance property, some node could not reach the destination because one or more of their paths to the destination could not be used to route traffic. We use the generated counterexample to learn edges that could not be used to route traffic due to the policy on them. To do so, we inspect the computed solution to find nodes \(\widehat{u}\) that (1) lack a route to the destination (i.e. \(\widehat{\mathcal {L}}(\widehat{u}) = \infty \)), (2) have a neighbor \(\widehat{v}\) that has a valid route to the destination, and (3) the link between \(\widehat{u}\) and \(\widehat{v}\) is not failed. These conditions imply the absence of a valid route to the destination not because link failures disabled all paths to the destination, but because the network policy dropped some routes. For example, in picture Fig. 3c, consider the case where \(\widehat{b}\) does not advertise routes from \(\widehat{a}_{13}\) and \(\widehat{a}_{24}\); if the link between \(\widehat{a}_{13}\) and \(\widehat{d}\) fails, then \(\widehat{a}_{13}\) has no route the destination and we learn that the edge \({\langle {\widehat{b},\widehat{a}_{13}}\rangle }\) cannot be used. In fact, since \(\widehat{a}_{13}\) and \(\widehat{a}_{12}\) belonged to the same abstract group \(\widehat{a}\) before we split them, their routing policies are equal modulo the abstraction function by transequivalence. Hence, we can infer that in a symmetric scenario, the link \({\langle {\widehat{b},\widehat{a}_{24}}\rangle }\) will also be unusable.
Given a set of unuseable edges, learned from a counterexample, we restrict the min cut problems that define the plausible abstractions, by disallowing the use of those edges. Essentially, we enrich the refinement algorithm’s topological based analysis (based on mincut) with knowledge about the policy; the algorithm will have to generate abstractions that are plausible without using those edges. With those edges disabled, the refinement process continues as before.
6 Implementation
Origami uses the Batfish network analysis framework [12] to parse network configurations, and then translate them into a pure functional intermediate representation (IR) designed for network verification. This IR represents the structure of routing messages and the semantics of transfer and preference relations using standard functional data structures.
The translation generates a separate functional program for each destination subnet. In other words, if a network has 100 topofrack switches and each such switch announces the subnets for 30 adjacent hosts, then Origami generates 100 functional programs (i.e. problem instances). We separately apply our algorithms to each problem instance, converting the functional program to an SMT formula when necessary according to the algorithm described earlier. Since vendor routing configuration languages have limited expressive power (e.g., no loops or recursion) the translation requires no userprovided invariants. We use Z3 [10] to determine satisfiability of the SMT problems. Solving the problems separately (and in parallel) provides a speedup over solving the routing problem for all destinations simultaneously: The individual problems are specialized to a particular destination. By doing so, opportunities for optimizations that reduce the problem size, such as dead code elimination, arise.
Optimizing Refinement: During the course of implementing Origami, we discovered a number of optimizations to the refinement phase.

If the mincut between the destination and a vertex u is less than or equal to the desired number of disjoint paths, then we do not need to compute another mincut for the nodes in the unreachable portion of vertices T; we know nodes in T can be disconnected from the destination. This significantly reduces the number of mincut computations.

We stop exploring abstractions that are larger in size than the smallest plausible abstraction computed since the last invocation of the SMT solver.

We bias our refinement process to explore the smallest abstractions first. When combined the previous optimization, this prunes our search space from some abstractions that were unnecessary large.
To mitigate the effect of this problem, we could ask the solver to minimize the returned counterexample, returning a counterexample that corresponds to the fewest concrete link failures. We could do so by providing the solver with additional constraints specifying the number of concrete links that correspond to each abstract link and then asking the solver to return a counterexample that minimizes this sum of concrete failures. Of course, doing so requires we solve a more expensive optimization problem. Instead, given an initial (possibly spurious counterexample), we simple ask the solver to find a new counterexample that (additionally) satisfies this constraint. If it succeeds, we have found a real counterexample. If it fails, we use it to refine our abstraction.
7 Evaluation
We evaluate Origami on a collection of synthetic data center networks that are using BGP to implement shortestpaths routing policies over common industrial datacenter topologies. Data centers are good fit for our algorithms as they can be very large but are highly symmetrical and designed for fault tolerance. Data center topologies (often called fattree topologies) are typically organized in layers, with each layer containing many routers. Each router in a layer is connected to a number of routers in the layer above (and below) it. The precise number of neighbors to which a router is connected, and the pattern of said connections, is part of the topology definition. We focus on two common topologies: fattree topologies used at Google (labelled FT20, FT40 and SP40 below) and a different fattree used at Facebook (labelled FB12). These are relatively large data center topologies ranging from 500 to 2000 nodes and 8000 to 64000 edges.
SP40 uses a pure shortest paths routing policy. For other experiments (FT20, FT40, FB12), we augment shortest paths with additional policy that selectively drops routing announcements, for example disabling “valley routing” in various places which allows updownupdown routes through the data centers instead of just updown routes. The pure shortest paths policy represents a bestcase scenario for our technology as it gives rise to perfect symmetry and makes our heuristics especially effective. By adding variations in routing policy, we provide a greater challenge for our tool.
Experiments were done on a Mac with a 4 GHz i7 CPU and 16 GB memory.
7.1 Compression Results
Figure 4 shows the level of compression achieved, along with the required time for compression and verification. In most cases, we achieve a high compression ratio especially in terms of links. This drastically reduces the possible failure combinations for the underlying verification process. The cases of 10 link failures on FT20 and 5 link failures on FbFT demonstrate another aspect of our algorithm. Both topologies cannot sustain that many link failures, i.e. some concrete nodes have less than 10 (resp. 5) neighbors. We can determine this as we refine the abstraction; there are (abstract) nodes that do not satisfy the min cut requirement and we cannot refine them further. This constitutes an actual counterexample and explains why the abstraction of FT20 for 10 link failures is smaller than the one for 5 link failures. Importantly, we did not use the SMT solver to find this counterexample. Likewise, we did not need to run a min cut on the much larger concrete topology. Intuitively, the rest of the network remained abstract, while the part that led to the counterexample became fully concrete.
7.2 Verification Performance
The verification time of Origami is dominated by abstraction time and SMT time, which can be seen in Fig. 4. In practice, there is also some time taken to parse and preprocess the configurations but it is negligible. The abstraction time is highly dependent on the size of the network and the abstraction search breadth used. In this case, the breadth was set to 25, a relatively high value.
7.3 Refinement Effectiveness
We now evaluate the effectiveness of our search and refinement techniques.

Heuristics off means that (almost) all heuristics are turned off. We still try to split nodes that are on the cutset.

Reachable off means that we do not bias towards splitting of nodes in the reachable portion of the cutset.

Common off means that we do not bias towards splitting reachable nodes that have the most connections to unreachable nodes.
The results of this experiment show that in order to achieve effective compression ratios we need to employ both smart heuristics and a wide search through the space of abstractions. It is possible that increasing the search breadth would make the heuristics redundant, however, in most cases this would make the refinement process exceed acceptable time limits.
Use of Counterexamples. We now assess how important it is to (1) use symmetries in policy to infer more information from counterexamples, and (2) minimize the counterexample provided by the solver.
We see in Fig. 6 that disabling them increases number of refinement iterations. While each of these refinements is performed quickly, the same cannot be guaranteed of the verification process that runs between them. Hence, it is important to keep refinement iterations as low as possible.
8 Related Work
Bonsai [3] and Surgeries [22] both leverage abstraction to accelerate verification for routing protocols and packet forwarding respectively. Both tools compute a single abstract network that is bisimilar to the original concrete network. Alas, neither approach can be used to reason about properties when faults may occur.
Minesweeper [2] is a general approach to control plane verification based on a stable state encoding, which leverages an SMT solver in the backend. It supports a wide range of routing protocols and properties, including fault tolerance properties. Our compression is complementary to such tools; it is used to alleviate the scaling problem that Minesweeper faces with large networks.
With respect to verification of fault tolerance, ARC [13] translates a limited class of routing policies to a weighted graph where faulttolerance properties can be checked using graph algorithms. However, ARC only handles shortest path routing and cannot support stateful features such as BGP communities, or local preference, etc. While ARC applies graph algorithms on a staticallycomputed graph, we use graph algorithms as part of a refinement loop in conjunction with a general purpose solver.
9 Conclusions
We present a new theory of distributed routing protocols in the presence of bounded link failures, and we use the theory to develop algorithms for network compression and counterexampleguided verification of fault tolerance properties. In doing so, we observe that (1) even though abstract networks route differently from concrete ones in the presence of failures, the concrete routes wind up being “at least as good” as the abstract ones when networks satisfy reasonable wellformedness constraints, and (2) using efficient graph algorithms (min cut) in the middle of the CEGAR loop speeds the search for refinements.
We implemented our algorithms in a network verification tool called Origami. Evaluation of the tool on synthetic networks shows that our algorithms accelerate verification of fault tolerance properties significantly, making it possible to verify networks out of reach of other stateoftheart tools.
References
 1.Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 203–213 (2001)Google Scholar
 2.Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: SIGCOMM, August 2017Google Scholar
 3.Beckett, R., Gupta, A., Mahajan, R., Walker, D.: Control plane compression. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 476–489. ACM (2018)Google Scholar
 4.Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450–462. Springer, Heidelberg (1993). https://doi.org/10.1007/3540569227_37CrossRefGoogle Scholar
 5.Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexampleguided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15CrossRefGoogle Scholar
 6.Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
 7.Daggitt, M.L., Gurney, A.J.T., Griffin, T.G.: Asynchronous convergence of policyrich distributed bellmanford routing protocols. In: SIGCOMM, pp. 103–116 (2018)Google Scholar
 8.Daggitt, M.L., Gurney, A.J., Griffin, T.G.: Asynchronous convergence of policyrich distributed BellmanFord routing protocols. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 103–116. ACM (2018)Google Scholar
 9.Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS 2001, p. 51 (2001)Google Scholar
 10.de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_24CrossRefGoogle Scholar
 11.Feamster, N., Rexford, J.: Networkwide prediction of BGP routes. IEEE/ACM Trans. Netw. 15(2), 253–266 (2007)CrossRefGoogle Scholar
 12.Fogel, A., et al.: A general approach to network configuration analysis. In: NSDI (2015)Google Scholar
 13.GemberJacobson, A., Viswanathan, R., Akella, A., Mahajan, R.: Fast control plane analysis using an abstract representation. In: SIGCOMM (2016)Google Scholar
 14.Gill, P., Jain, N., Nagappan, N.: Understanding network failures in data centers: measurement, analysis, and implications. In: SIGCOMM (2011)Google Scholar
 15.Godfrey, J.: The summer of network misconfigurations (2016). https://blog.algosec.com/2016/08/businessoutagescausedmisconfigurationsheadlinenewssummer.html
 16.Griffin, T.G., Shepherd, F.B., Wilfong, G.: The stable paths problem and interdomain routing. IEEE/ACM Trans. Netw. 10(2), 232–243 (2002)CrossRefGoogle Scholar
 17.Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. Softw. Tools Technol. Transf. 2(4), 328–342 (2000)CrossRefGoogle Scholar
 18.Lapukhov, P., Premji, A., Mitchell, J.: Use of BGP for routing in largescale data centers. Internet draft (2015)Google Scholar
 19.Lopes, N.P., Rybalchenko, A.: Fast BGP simulation of large datacenters. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 386–408. Springer, Cham (2019). https://doi.org/10.1007/9783030112455_18CrossRefGoogle Scholar
 20.Lougheed, K.: A border gateway protocol (BGP). RFC 1163, RFC Editor (1989). http://www.rfceditor.org/rfc/rfc1163.txt
 21.Mahajan, R., Wetherall, D., Anderson, T.: Understanding BGP misconfiguration. In: SIGCOMM (2002)Google Scholar
 22.Plotkin, G.D., Bjørner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: POPL (2016)Google Scholar
 23.Quoitin, B., Uhlig, S.: Modeling the routing of an autonomous system with CBGP. Netw. Mag. Glob. Internetworking 19(6), 12–19 (2005)Google Scholar
 24.Sobrinho, J.A.L.: An algebraic theory of dynamic network routing. IEEE/ACM Trans. Netw. 13(5), 1160–1173 (2005)CrossRefGoogle Scholar
 25.Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Formal semantics and automated verification for the border gateway protocol. In: NetPL (2016)Google Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.