CB-V ER: A Stable Foundation for Modular Control Plane Verification Dexin Zhang Timothy Alberdingk Thijm Princeton University
arXiv:2604.03539v1 [cs.NI] 4 Apr 2026
David Walker Princeton University
Aarti Gupta Princeton University
Abstract
Fundamentally, such outages occur because key eventuallystable properties of networks are violated. Informally, an eventually-stable property is one that holds at some time τ, and forever after that. In linear temporal logic, these properties can be expressed as FGp, where F is the eventually temporal operator, G is the globally temporal operator, and p does not have temporal operators. A typical example property is eventually stable reachability: After some time τ, a node X always has a path to node Y, provided the operating environment (external announcements, failures, etc.) does not change. In this paper, we develop a new, general theory for reasoning about eventually-stable properties of networks and study its practical benefits. In this theory, every network device v is associated with two interfaces, I(v) and Q(v). The interface I overapproximates the set of states the devices can enter at any time during execution, while Q overapproximates the eventually-stable states. Because the device interfaces Q overapproximate the states to which the network converges, we say that these interfaces characterize abstract (rather than concrete) convergence of the network. To prove that Q characterizes abstract convergence of a network, we first define a collection of local verification conditions for each device v that relate I and Q to each other, and to the interfaces of adjacent devices. Second, to complete the proof that such interfaces really do converge to the proposed eventually-stable states, one must supply a witness for the convergence process. We call this witness the converges-before graph (CB-graph)1 . It must connect all devices to the origin of the routing process. Once the interfaces are proven valid, a user can consider other eventually stable properties Y that Q entails. We formalized this new theory in Lean [37] and proved it sound. This new theory of abstract convergence is useful first and foremost because it serves as a basis for modular network verification: If a user supplies interfaces I and Q per device, the verification conditions for each device can be proven
Network operators are often interested in verifying eventuallystable properties of network control planes: properties of control plane states that hold eventually, and hold forever thereafter, provided the operating environment remains unchanged. Examples include eventually-stable reachability, access control, or path length properties. In this work, we introduce CB-V ER, a new framework for verifying such properties, based on the key idea of a converges-before graph (CB-graph for short). When a user provides interfaces for each network component, CB-V ER checks the necessary component-bycomponent requirements in parallel using an SMT solver. In addition, the tool automatically synthesizes a CB-graph and checks whether it connects all nodes in a network—if it does, the interfaces are valid and users can check whether additional eventually-stable properties are implied. Moreover, the CBgraph can then be used to determine fault tolerance properties of the network. We formalize our verification algorithm in the Lean theorem proving environment and prove its soundness. We evaluate the performance of CB-V ER on a range of benchmarks that demonstrate its ability to verify expressive properties in reasonable time. Finally, we demonstrate it is possible to automatically generate suitable interfaces by turning the problem around: Given a CB-graph, we use an off-the-shelf Constrained Horn Clause (CHC) solver to synthesize interfaces for every network component that together ensure the given correctness property.
1
Introduction
Large cloud providers now own, manage, monitor, and maintain vast networks of networks that span a hundred or more countries, connect millions of servers, and consist of hundreds of thousands of network devices [27]. Unfortunately, it is rather routine to see mainstream news stories about errors in the configuration of network control planes causing significant network downtime and disrupting critical services (e.g., see the Rogers outage in Canada amongst others [2])
1 This
name is inspired by the standard "happened-before relationship" [33].
1
2.2 Background: Modeling routing protocols in SMT theories
independently and in parallel. Moreover, a CB-graph that validates these properties can be synthesized automatically and efficiently. Put together, these procedures result in an efficient and scalable new algorithm for network verification. In addition, we observe that the synthesized CB-graph has effectively the maximal connectivity for the given interfaces: If edges of the CB-graph fail, then connectivity is reduced. Hence, by analyzing the connectivity of the CB-graph, it is possible to determine the degree of fault tolerance of any proven property—a key concern for network engineers building resilient systems. We also consider the inverted problem: when a connected CB-graph is supplied, the interfaces I and Q can be synthesized automatically by using an off-the-shelf Constrained Horn Clause (CHC) solver. To demonstrate these ideas, we built a new network verifier called CB-V ER, applied it to an array of examples, used it to prove properties and analyze fault tolerance. We also built CB-2IQ, a prototype tool for automated interface synthesis. Our work was inspired by recent research on modular network verification [7,41] – we highlight key differences from closely related past work in the next section (§2) along with some motivating examples. Other related work on control plane verification [3, 5, 13–15, 23, 28, 38, 39, 44–46] and control plane convergence [19, 26, 40] is discussed in section §7.
2
Modeling routing protocols using SMT theories is a wellunderstood process. Minesweeper [13] provides an extensive explanation of the basic mechanics for BGP and other protocols (RIP, OSPF, static routes). We assume a multi-sorted first-order theory T [11]. The routes can be viewed as records of routing fields that vary according to a protocol, where each field is of some sort. We use S = σ1 × σ2 × · · · σn to represent this (each σi is a sort). The merge operator and transfer functions also vary according to the protocol, and are modeled as expressions and formulas in theory T . We use merge and tre for the SMT-encoded versions of ⊕ and fe . Take BGP protocol as an example. A BGP route is encoded in CB-V ER as a quadruple (prefix, lp, path, comm). 2 where prefix is a 32-bit vector (assuming IPv4) indicating the destination prefix, lp is an integer indicating local preference, path is an ordered sequence of AS numbers for each router this message has traversed (called AS-path in BGP), and comm is a finite set of community tags. We use expression prefix(s) to denote the prefix field of a route s. In BGP, the merge function encodes the preference order between two routes, checking the local preference first (higher is preferred), and if it is the same, then the length of the AS-path (shorter path is preferred). Accordingly, the merge operator is modeled as:
CB-V ER: Overview and Key Ideas
2.1
Background: The control plane model
The network control plane is a set of routers that exchange messages with each other about available paths to a destination using standard routing protocols such as BGP, OSPF, RIP. We refer to these messages as routes (s), and use ∞ to denote “no route.” Following prior work [19], we model control plane execution using an asynchronous message-passing semantics. Each instance of the model considers the forwarding behavior of a network with respect to a particular destination prefix (a set of IP addresses). All routers start with an initial route (routers may start with the ∞ route if they do not originate a route). Routers then asynchronously and repeatedly:
merge(s1 , s2 ) =
s1 s2 s1 s2 s1
lp(s1 ) > lp(s2 ) lp(s1 ) < lp(s2 ) lp(s1 ) = lp(s2 ) ∧ len(path(s1 )) < len(path(s2 )) lp(s1 ) = lp(s2 ) ∧ len(path(s1 )) > len(path(s2 )) otherwise
Cases can be expressed through if-then-else expressions, len(l) is a pre-defined function in the theory of sequences, returing the length of the list l. (We write len(s) in short for len(path(s)) in the paper.) For the last case, two routes are equally preferred, and one of them is chosen arbitrarily. The transfer functions are modeled based on the configuration and its semantics. For example, a set community 100:2 statement in Cisco’s configuration language sets the communities field to be {100 : 2}, which can be modeled as:
• receive routes transmitted from their neighbors, • select the preferred route between their current route and the routes they have received so far (the route preference relation is determined by the protocol, and modeled by a merge function ⊕; the result of s1 ⊕ s2 is the preferred route between s1 and s2 ), • store the preferred route for use (often called the current state of the node)
tr(s, s′ ) ⇔ comm(s′ ) = {100 : 2}
• transform that route according to router policies (modeled by a transfer function f , where fe (s) denotes how router policy on edge e transforms route s into s′ ), and
∧ lp(s′ ) = lp(s)
∧ prefix(s′ ) = prefix(s) ∧ path(s′ ) = path(s) 2 for simplicity, we do not show the model of all BGP features here.
• forward the preferred route to neighbors. 2
routes that eventually persist at each node, but narrow enough (i.e., strong enough) (iia) to imply the properties Yi and (iib) to explain the convergence behavior of adjacent nodes. For our example, to prove Y1 (E), it suffices to choose Q1 (v) = {s | s ̸= ∞} for v ∈ {A, B,C, E}. Notice in particular that Q1 (E) = Y1 (E) so our desired property Y1 (E) is particularly easy to prove if the Q1 (v) interfaces are valid for all v. However, to prove Y2 (E), we need a stronger interface (lp(s) stands for local preference of the route s and len(s) stands for length of the path of s):
B E
A C
Figure 1: Example network with devices A, B, C, D. A originates the route. Local preference is set to 300 on the B-E edge and to 100 elsewhere. Properties and interfaces are encoded as predicates over routes, which can be written in the language of SMT theories. For example, in the theory of sequences, one can use as the length of a list. Therefore, a property “routes with length of AS-path equal to 2” can be written as: Y (s) ⇔ len(s) = 2.
2.3
Q2 (E) = {s | s ̸= ∞ ∧ lp(s) = 300 ∧ len(s) = 2 ∧C ∈ / path(s)}. In addition, the Q2 (v) interfaces at other nodes v must also be more specific to affirm the absence of node C along the route from A through B to E:
Motivating Example
Q2 (A) = {s | s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) = 0 ∧C ∈ / path(s)}
Consider the simple network running a variant of the BGP routing protocol shown in Fig. 1. A network operator would like to prove that node E has a route to destination node A after the network has converged, and moreover that the route travels through B rather than C (perhaps the former route is less costly than the latter). To implement that preference, the network operator uses BGP’s local preference mechanism, setting the local preference attribute to 300 on the route from B to E and everywhere else leaving the local preference for routes at the default value of 100. When a router such as E receives routes from multiple neighbors, it chooses the route with the highest local preference (in this case, the route from B with value 300 over the route from C with value 100).
Q2 (B) = {s | s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) = 1 ∧C ∈ / path(s)} Q2 (C) = {s | s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) = 1}.
Step 3: Check that Q interfaces are sufficient to prove the properties Y . Given the Q(v) interfaces for each node v, it is straight-forward to check that for each property, Q1 (E) ⇒ Y1 (E) and Q2 (E) ⇒ Y2 (E), i.e., if the Q(v) predicates are eventually-stable, then the desired properties are eventuallystable. Step 4: Check that Q interfaces are correct. We now need to prove that the user-provided interfaces Q are eventuallystable. Doing so can be split into two parts: (1) Verification of local invariance and convergence conditions, and (2) Generation and verification of a converges-before graph.
Step 1: Specify correctness properties. The first step in using CB-V ER is to specify properties of interest. In our example, we might specify: • Y1 (E): Will node E be able to reach A?
Step 4.1: Verify local conditions. To prove that Q(v) properly overapproximates the converged set of states for the node v, one must often reason about the set of messages that can reach v. To do so, we augment our interfaces with the auxiliary set I(v), which overapproximates the set of routes that can reach v, and we define local verification conditions that ensure I and Q maintain the appropriate relationship: For any neighbor u of v, given I(u), one can check that u does not send messages that cause v to deviate from I(v). In addition, if u has already converged to a route s in Q(u), and a transfer of s leads to v selecting a route in Q(v), when it had a route in I(v) before the transfer, then this witnesses a convergence step of the process—such convergence steps play a special role, described soon. In our example, for proving Y1 (E), we can say I1 (v) (for any node v) is the set of all routes (including ∞), since our goal is simply to prove that any route is accepted by each node. (The overapproximations allowed by our theory are
• Y2 (E): Will node E select a path to A using a route from node B rather than from node C? The first property Y1 (E) expresses a simple reachability property, while the second Y2 (E) captures a preference property. The user is interested in checking that these properties hold at some point and forever after (provided changes to the operating environment do not occur). In terms of a routing state s, we express these properties as the formulas shown below: Y1 (E) = {s | s ̸= ∞} Y2 (E) = {s | s ̸= ∞ ∧C ∈ / path(s)} Step 2: Specify Q, an overapproximation of the states to which the network converges. The second step in CBV ER is for the user to specify the abstract interface Q, which is a mapping from nodes to sets of routes. The interface Q must be: (i) large enough that it overapproximates the set of 3
useful here: We need not think much about the exact set of routes that can reach a given point because the property we wish to prove is a loose one.) However, for proving Y2 (E), I2 (C) should not contain a high-priority route (say priority 700, or any priority greater than 300), because if it did, then one might conclude that node E will converge to a bad route that runs through C rather than B. With these ideas in mind, we could use the following I2 interfaces:
B
B
CB-root
CB-root E
A C
(a) CB-graph for I1 , Q1 .
E
A C
(b) CB-graph for I2 , Q2 .
Figure 2: Synthesized CB-graphs for interfaces I1 , Q1 and I2 , Q2 .
I2 (A) = Q2 (A)
route in Q2 (C), and transfers this route to node E. Suppose E I2 (B) = I2 (C) = {s | s = ∞ ∨ (s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) ≥ 1)} does not have any route before this transfer, e.g., if the route I2 (E) = {s | s = ∞ ∨ (s ̸= ∞ ∧ lp(s) ≤ 300 ∧ len(s) ≥ 2)} transfer from node B is much delayed. Then, as a result of transfer from C, node E will select this route where the path includes C. However, this route does not belong to Q2 (E), as Step 4.2: Key Idea: CB-graphs. The interface Q(v) can defined earlier (since its path includes C). Therefore, the CE (perhaps) be justified by looking at the interfaces of its neighedge is not a CB-edge. bors Q(u) (and I(u)), but not if such neighboring interfaces are in turn justified recursively by Q(v). Such circular reasoning is clearly unsound. To ensure soundness of our theory, we introduce the CB-graph—if this graph connects all nodes in the network, the length of the shortest path from any node to the roots in this graph can be used in an inductive argument about the correctness of our verification conditions. A CB-graph is composed of a subset of nodes called CBroots, and a subset of directed edges called CB-edges. Informally, a node v is a CB-root if its initial route (at time t = 0) and any route forever thereafter (at time t > 0) belong to Q—in other words, each CB-root v converges (in an abstract sense) to its interface Q(v) at time 0 itself. CB-edges capture a “converges-before” relationship between nodes. Informally, a CB-edge (u, v) ensures that a route in Q(u) at node u, when transferred to v, must result in selection of a route in Q(v) at node v. Note that node v may already have a route in Q(v) before the route transfer from u, but if it does not, then the CB-edge (u, v) will ensure that it does so after the route transfer and merge at v. This latter condition corresponds to witnessing a convergence step mentioned earlier. In our example, it is easy to see that node A is a CB-root in a CB-graph for both sets of interfaces (I1 , Q1 as well as I2 , Q2 ). Thanks to the originated routes at node A (that have the shortest length 0), the routes at t = 0 and at all times thereafter belong to Q1 (A) (Q2 (A)) specified by the user. In practice, a node that originates routes, or acts as a border node that receives and transfers route announcements from external sources to other nodes in the network, serves as a CB-root. As an example of a CB-edge, consider the edge BE in the network with the I1 , Q1 interfaces. If node B has a route in Q1 (B) (i.e., if it has a route at all), then a route transfer from node B to node E will definitely result in node E having a route in Q1 (E) after the transfer. Critically, this is true regardless of which other messages may have reached this node earlier (i.e., for any state in I1 (E) that node E was in earlier). Thus, the edge BE is a CB-edge. As an example of an edge that is not a CB-edge, consider the edge CE for the I2 , Q2 interfaces. Suppose node C has a
Key Idea: Connected CB-graphs. If the CB-graph connects all nodes in the network (and all local verification conditions are validated), then all nodes will indeed eventually reach states included in Q. We have proven this central theorem (§3.2) in Lean. Note we do not require a CB-graph to be acyclic, because a CB-edge (u, v) only says v will abstractly converge if u abstractly converges — it does not enforce an ordering that u must converge at a time before v. This allows us to synthesize a maximal CB-graph— note that any connected CB-graph must have a connected acyclic subgraph. Step 5: Synthesis of a CB-graph. CB-V ER does not require a user to provide a CB-graph; it synthesizes a maximal CB-graph automatically and checks if it is connected. In parallel, it uses the collection of node-local and edge-local verification conditions to generate the maximal set of valid CB-nodes and CB-edges. After doing so, there is one global check, implemented as a standard graph traversal algorithm, which determines whether the synthesized graph is connected. If verification fails, CB-V ER provides debugging information—we briefly describe a user-assisted debugging process to refine the interfaces. Fig. 2 shows the CB-graphs that are synthesized by CBV ER for our running example with interfaces I1 , Q1 and I2 , Q2 , respectively. In both graphs, node A is a CB-root (as described earlier). For I1 , Q1 , every directed edge is a CB-edge as shown. This is because no routes are dropped along any edge — thus, transfer of a route along each edge necessarily establishes Q1 at the receiving node. Clearly, a connected CB-graph exists for I1 , Q1 . For I2 , Q2 , there are three CB-edges: AB, AC, and BE as shown. As described earlier, the edge CE is not a CB-edge. Also, the edges BA,CA, EB are not CB-edges, because route transfers along these edges would result in routes with length greater than what is allowed in the respective Q2 interfaces 4
of the receiving node. Still, a connected CB-graph exists for I2 , Q2 as well. CB-V ER reports success for this example because VCs generated by CB-V ER establish I as an invariant and identify a connected CB-graph for Q, and Q entails Y . This guarantees correctness of the given properties in this example.
• R is the set of all routing messages, or simply routes, that can be exchanged between nodes. ∞ ∈ R (invalid route) is used when no route is selected.
Closely Related Work. Timepiece [7] and Lightyear [41] are two recent modular verifiers that share some similar goals with our work. Timepiece’s operational model assumes the network is synchronous, sending and receiving messages in lockstep.3 In contrast, CB-V ER is sound for all asynchronous schedules. More importantly, a Timepiece user must write a symbolic function A(v,t) for each node v, that specifies for each time t ∈ N, the set of routes that node v may select at time t. In contrast, CB-V ER users need not worry about exactly when messages are sent or received from neighboring nodes, simplifying construction of interfaces. Timepiece does not support failure analysis or interface synthesis. Lightyear [41] allows users to prove safety properties and a limited kind of liveness property, provided users supply a path along which routing announcements can flow. CB-V ER improves upon Lightyear in a number of ways: (1) CB-V ER can prove many eventually stable properties that Lightyear cannot, because CB-V ER uses a more general network model that includes, for instance, route preferences and route selection (Lightyear cannot prove the Y2 property from our example); (2) CB-V ER supports a fully automatic fault tolerance analysis whereas Lightyear does not; (3) CB-V ER synthesizes a CB-graph whereas Lightyear users must supply a path manually; (4) when given a CB-graph, CB-2IQ can automatically synthesize interfaces, whereas Lightyear does not provide a method for interface synthesis.
• f : E → (R → R) maps each edge (u, v) ∈ E to a transfer function f (e) : R → R (also written as fe ). For instance, f(u,v) is the transfer function for routes sent from u to v.
3
• init : V → R is a function that maps each node v ∈ V to its initial route init(v), which is the route that originates from v or is imported from external sources at a border node. It is ∞ if there is no routes originated or imported.
• ⊕ : R × R → R is a binary associative, commutative and selective function (the merge function) that selects the best route between two routes. Asynchronous schedules and fairness. To model an asynchronous network, we follow the approach of Üresin and Dubois [42] and Daggitt et al. [19]. In this model, times are natural numbers T = N, and a schedule for a network N is a pair (α, β) with: 1. An activation function α : T → 2V that maps a time t to a set of routers α(t) activated at that time. 2. A data flow function β : E → (T → T) that defines the time taken to traverse each link e = (u, v). If t1 = β(e)(t2 ) (also written βe (t2 )), the route sent by u at time t1 will arrive at v at time t2 . Messages must be received after they sent and hence t2 > t1 in all cases. Such schedules can model arbitrary delay, loss, or duplication of any message in transit. To prove soundness, we assume that schedules satisfy some standard axioms, including fairness (messages are delivered eventually), and in-order message delivery (messages from the same neighbor are delivered in sending order). Note that messages from different neighbors are sent and received in parallel. Details are described in Appendix B. (In §4.2 we discuss fault tolerance under edge failures; for the rest, we assume that a schedule is fair unless stated otherwise.) The network semantics of N with respect to a schedule S = (α, β) is defined as the following function σS : V ×T → R.
Abstract Convergence and CB-graphs
3.1
Network Model and Semantics
We represent network control planes using a common network model, inspired by routing algebras [26,40], where each network instance considers one destination prefix. This model has been applied to a wide range of routing protocols used in practice, including BGP, RIP, OSPF. Formally, a network instance (network for short) is a 5-tuple N = (G, R, init, f , ⊕), where:
t =0 init(v) σS (v,t) = σS (v,t − 1) t > 0∧v ∈ / α(t) L init(v) ⊕ u f(u,v) (σS (u, β(u,v) (t))) otherwise (1) At t = 0, each node v selects its initial route init(v). Henceforth, if v is activated at time t (i.e., v ∈ α(t)), it will select the best route among all routes received from its neighbors (possibly delayed). Otherwise, its route remains the same as at time t − 1. For a given schedule S and network N, we say node v converges to r if ∃τ. ∀t ≥ τ, σS (v,t) = r. In other words, v
• G = (V, E) is a simple, finite directed graph. The nodes V of G are routers, and the edges E ⊆ V × V of G are links. 3 Alberdingk Thijm describes an extension [8] that considers an asynchronous network semantics, but such assumptions make construction of interfaces more difficult. This extension was not implemented.
5
converges to r if σS (v,t) is equal to r for some t and forever after. At the network level, we say the network semantics σS converges to σ∗S : V → R if v converges to σ∗S (v) for each node v. Such a state σ∗S is called a converged state of the network. Note that a network may have multiple converged states for different schedules S (this can happen in real networks [17]), or it may have no converged state (e.g., it may oscillate between a set of states [25]).
property Y at each node. Our two-step strategy is: (1) establish that all nodes v abstractly converge to Q(v), (2) for each node v, check that every route in Q(v) satisfies Y (v). The second step is easy to do: we use an SMT solver to check the validity of Q(v) ⇒ Y (v) (where ⇒ denotes propositional implication). However, the first step is more challenging. CB-graph. For sound reasoning about abstract convergence for the given interfaces I, Q, we introduce a structure called a CB-graph, comprised of CB-roots and CB-edges, defined in terms of the network semantics as follows:
Correctness properties Y . Network engineers need to verify correctness properties of such systems. A user-provided correctness property Y : V → 2R maps each node v to some predicate (formula) Y (v) on routes. Our theory will support verification of eventually-stable variants of Y . More formally, we will verify that for all schedules S:
• CB-roots: a non-empty subset of nodes w ∈ V , each w must select a route σS (w,t) ∈ Q(w) at any time t starting from the t = 0, for any schedule S. • CB-edges: a subset of directed edges (u, v) in the network, such that for any schedule S, if u selects a route σS (u,t1 ) ∈ Q(u) at time t1 , and transfers this route along edge (u, v), then v must select a route σS (v,t2 ) ∈ Q(v), where t2 is the time that v receives and merges u’s route.
∀v. ∃τ. ∀t ≥ τ. σS (v,t) ∈ Y (v). CB-V ER requires the properties Y to be written as predicates per node, to allow modular verification of such properties. However, global properties or path-dependent properties can also be expressed in CB-V ER in a modular form through decomposition or introducing ghost variables and ghost code. For example, global connectivity (i.e., connectivity between all/certain nodes) can be decomposed into single-destination connectivity per destination d. For each d, we can define property Y (v) to be “v can reach the destination d”, and then verify separately for all/certain destinations d. For path-dependent properties, we can introduce ghost fields that are updated along the path. For example, to verify that any route selected by v must go through a certain set of nodes S, one can add a ghost field AcrossS that is set true when a route is imported by a node in S. Then verifying Y (v) as “only route s with AcrossS(s) = true can be selected by v ” ensures this pathdependent property.
Connectedness of a CB-graph. We say that a CB-graph is connected if every node v in the network is itself a CB-root or has a path of CB-edges from some CB-root w to v. The following theorem states that a connected CB-graph provides a basis for reasoning about abstract convergence (a proof sketch appears in the Appendix B; a formal proof has been carried out in Lean). Theorem 1 (Connected CB-graph Theorem). If a CB-graph for Q is connected, then all nodes v in the network abstractly converge to Q(v).
4
From Theory to Modular Tool: CB-V ER
We now describe how we use our theory of abstract convergence to develop a modular verifier CB-V ER. As note earlier, in addition to Q, we use an interface I : V → 2R , that maps map each node v to a set of routes that includes all routes that may be selected at v at any time and in any schedule.
3.2 Abstract Convergence: Semantic Definitions and Theorems Abstract convergence. Consider Q : V → 2R , which maps each node v to some predicate (formula) Q(v) on routes. Given a specific network and (fair) schedule S, σS (v,t) abstractly converges to Q(v) if:
4.1
CB-V ER Algorithm
CB-V ER generates and checks various Verification Conditions (VCs) on nodes and edges in the network. These are summarized in Fig. 3, where each row shows a different VC set based on their role (explained below), and the respective formula generated by CB-V ER. The formulas capture conditions on arbitrary routes su and sv at nodes u and v, respectively. The conditions are expressed in terms of the network model (i.e., with operations init, f , ⊕ drawn from the network in question), interfaces (Q, I), and correctness property (Y ) provided by the user. For each of these VCs, CB-V ER invokes an SMT solver (e.g., Z3 [20]) to check its validity. If
∃τ. ∀t ≥ τ, σS (v,t) ∈ Q(v). Note that when σS (v,t) abstractly converges to Q(v), it may not concretely converge, but if it converges, then the concrete converged route σ∗S (v) must be included in the set Q(v). We say a node v abstractly converges to Q(v) if σS (v,t) abstractly converges to Q(v) for all schedules S. Abstract convergence interface Q. We require the user to provide an annotation Q, which we call an abstract convergence interface, and use it to verify the given correctness 6
VC Set
VC Formula
VCInit (v)
init(v) ∈ I(v)
VCInv ((u, v)) VCProp (v)
Algorithm 1: CB-V ER Verification Algorithm. Input :Network N, Correctness Properties Y , and modular interfaces Q, I Output :Correct or Fail (with counterexamples) / CBEdges ← 0; / 1 CBRoots ← 0, 2 for v ← V do in parallel 3 if VCInit (v) ∧VCProp (v) is not valid then 4 return Fail; 5 end 6 if VCCBroot (v) is valid then 7 CBRoots ← CBRoots ∪ {v}; 8 end 9 end 10 for e ← E do in parallel 11 if VCInv (e) is not valid then 12 return Fail; 13 end 14 if VCCBedge (e) is valid then 15 CBEdges ← CBEdges ∪ {e}; 16 end 17 end 18 if IsConnected(CBRoots, CBEdges) then 19 return Correct; 20 else 21 return Fail; 22 end
∀su , sv . su ∈ I(u) ∧ sv ∈ I(v) ⇒ sv ⊕ f(u,v) (su ) ∈ I(v) ∀sv . sv ∈ Q(v) ⇒ sv ∈ Y (v) init(v) ∈ Q(v)
VCCBroot (v)
VCCBedge ((u, v))
∧
^
! ∀su , sv . su ∈ I(u) ∧ sv ∈ Q(v)
u∈V,(u,v)∈E
⇒ sv ⊕ f(u,v) (su ) ∈ Q(v)
∀su , sv . su ∈ Q(u) ∧ sv ∈ I(v) ⇒ sv ⊕ f(u,v) (su ) ∈ Q(v)
Figure 3: Summary: Verification Condition (VC) Formulas. the validity check fails, the solver provides a counterexample, i.e., values of routes su , sv where the formula is false. The first three VCs are regarded as essential VCs, because if any of them fail, then CB-V ER immediately reports failure. They serve the following roles: • Checking invariant interface I: VCInit and VCInv together ensure that the user-provided interface I is an inductive invariant at each node v. As shown, VCInit performs a base check on every node v, to ensure that the initial route init(v) is in I(v). VCInv performs an inductive check for every edge (u, v): if a route su is in I(u), then the route sv selected by v after its transfer-and-merge must also be in I(v). Here, the subformula sv ⊕ fu,v (su ) represents the new route at node v after the merge (⊕) of its existing route sv and the transferred route ( f(u,v) (su )) from neighbor u.
Algorithm 1. The complete verification algorithm including generation and checking of the VCs is shown (as pseudocode) in Algorithm 1. It takes as inputs: a network N, correctness property Y , and modular interfaces Q, I; and produces output Correct or Fail (with debugging information). The algorithm has two phases. In phase 1 (lines 1-17), CBV ER generates and checks all VCs on the nodes and edges in parallel. If any of the essential VCs (VCInit ,VCInv ,VCProp ) is not valid, then CB-V ER reports Fail immediately, along with a counterexample for debugging purposes. The other two VCs (VCCBroot , VCCBedge ) are not essential in the sense that CBV ER does not report Fail immediately. If a VC in VCCBroot or VCCBedge is not valid, the associated node or edge is not added to the corresponding set (in phase 1), and CB-V ER will save the counterexample for later use. In phase 2 (line 18-22), CB-V ER uses a standard breadthfirst search (BFS) graph algorithm to check whether there exists a connected CB-graph using the CB-roots and CBedges identified in phase 1. If CB-V ER finds a connected CB-graph, it reports Correct; otherwise, it reports Fail (along with saved counterexamples for unconnected nodes).
• Checking correctness property Y : VCProp ensures that every route in the abstract convergence interface Q(v) satisfies Y (v). This is needed for checking the correctness of the eventual-stability property. CB-V ER requires that a user provide Q, I, but it alleviates some burden by constructing a CB-graph for Q. It checks two VCs, VCCBroot and VCCBedge , on all nodes and edges to identify CB-roots and CB-edges, respectively. • Identifying CB-roots: VCCBroot (v) checks that init(v) is in Q(v), and for every incoming edge (u, v) with su as some arbitrary selected state at node u (i.e., su ∈ I(u)), the route selected by v after transfer-and-merge must also belong to Q(v). If VCCBroot (v) is valid, then node v is a CB-root. • Identifying CB-edges: VCCBedge ((u, v)) checks that if su is in Q(u), and if sv is some arbitrary selected route at node v (i.e., sv ∈ I(v)), then the route selected by v after transfer-and-merge must belong to Q(v). If VCCBedge ((u, v)) is valid, then edge (u, v) is a CB-edge.
Discussion. To use CB-V ER in practice, a user needs to provide suitable Q and I interfaces, such that each node v abstractly converges to Q(v). Q(v) must be sufficient to estab7
lish a desired property Y (v). If a user provides an incorrect or an inadequate interface, the counterexamples generated by the SMT checks provide feedback for user-assisted debugging. For example, when VCCBedge fails, the SMT solver will generate concrete routes su , sv such that su ∈ Q(u) ∧ sv ∈ I(v) but sv ⊕ f(u,v) (su ) = s′v ∈ / Q(v). Based on their beliefs (or knowledge) about su , sv and s′v , they can strengthen Q(u), I(v) to exclude su , sv , or weaken Q(v) to include s′v . We describe an interactive error debugging process later in this section (§4.3). It is also possible that the transfer function f(u,v) is erroneous and needs repair – we leave automated repair to future work.
Figure 4: CB-graph of a cross-world network from the Batfish tutorial [47]. Houston (bordered in red) is a CB-root and directed arrows are CB-edges. tolerate any 1-edge failure, since the CB-graph is connected even if any one CB-edge is removed. However, the CB-graph does not show that AS3 (Asia) is tolerant to 1-edge failures, because removal of a single CB-edge from Seattle to Tokyo disconnects the CB-graph.
Correctness of CB-V ER. The correctness theorem is stated below (with a proof sketch in Appendix B). We have also formalized the network semantics and proofs in Lean [37] (with the Leans proof scripts in an anonymous repository shown in Appendix A).
4.3
Theorem 2 (Correctness Theorem). If the CB-V ER verification algorithm reports Correct for a network N, property Y , and interfaces Q, I, then for any schedule S, the network semantics σS (v,t) satisfies ∀v. ∃τ. ∀t ≥ τ. σS (v,t) ∈ Y (v).
4.2
Interactive Error Debugging
When Algorithm 1 fails, either some verification conditions (VCInit , VCInv or VCProp ) are violated, or the CB-graph is not connected (where some VCCBroot or VCCBedge are violated). Such violations could be due to incorrect network configurations (affecting init(v) and fe used in the VCs), or erroneous interfaces Q(v) and I(v) that may need to be refined. The property Y (v) itself may also be false. To debug these errors, the user needs to determine the cause of VC violation and take action, e.g., refine the interfaces or repair the configuration. A key advantage of modular verification is that VC violations are localized to particular edges or nodes. However, VC violations arising from monolithic verification, even when caused by a small error somewhere, would involve the whole network, making it harder for the user to track it down. In Appendix C, we present an interactive debugging process based on counterexamples that are generated by SMT solvers during Algorithm 1. Thanks to the localized VCs, the counterexamples are also localized, allowing users to diagnose the cause between a few possible cases. In Appendix D, we further provide an illustrative example of this debugging process.
CB-graphs and Fault Tolerance
In this subsection, we consider edge failures and correctness of properties under at most k edge failures. An edge is failed if it does not deliver any messages after a certain time (a formal definition is in Lean formalization §A or §B). We say a CB-graph is k-fail-connected if it remains connected no matter which combination of k CB-edges is removed. Algorithmically, CB-V ER’s phase 2 check executes a variant of Dinitz’s algorithm [21] to determine whether there exists a k-fail-connected CB-graph. Doing so is possible since CB-graph synthesis generates a maximal CB-graph in phase 1. We have proved the following theorem about our algorithm. Theorem 3 (Fault tolerance theorem). If the modified CBV ER algorithm reports Correct (i.e., the essential VCs pass and there exists a k-fail-connected CB-graph), then N is kfault tolerant: for any schedule S with at most k edge failures, ∀v. ∃τ. ∀t ≥ τ. σS (v,t) ∈ Y (v).
5
Note that the above theorem is one-directional: if CB-V ER reports Correct, then N is k-fault tolerant; but if a check fails, then N may be k-fault tolerant but this is not provable with the given interfaces.
Automated Synthesis of Abstract Interfaces
In this section, we consider a different variation of the verification problem, where a user may have an idea of a CB-graph, but would like to automatically synthesize the abstract interfaces I, Q, in order to prove the property Y of interest. This is often the case in practice for highly structured networks, such as a fat-tree topology in data centers [4], that is designed and configured to provide well-structured routes (e.g., valley-free paths) between top-of-rack nodes via aggregator and core nodes. In such structured topologies and policies, a CB-graph often corresponds to a BFS graph from the destination. Given a CB-graph, our approach for synthesis of the interfaces is based on using a solver for Constrained Horn Clauses
Example for fault-tolerance. Consider Fig. 4, which shows a network with 13 routers and 3 ASs (taken from a Batfish tutorial [47]). Suppose a user is interested in checking reachability to Houston and provides Q as an interface, where Q includes all routes except ∞. The CB-root and CB-edges (red arrows) identified by CB-V ER are also shown in the figure. It is easy to see that the node at Paris in AS1 (Europe) can 8
(CHC), e.g., Spacer/Z3 [31, 32]. We note that the problem of simultaneous synthesis of both a CB-graph and the interfaces is not a CHC problem, but can be formulated as a syntax-guided synthesis (SyGuS) problem [9] (e.g., by using a SyGuS solver such as cvc5 [10]) – we leave this to future work. CHC solvers are widely used in program verification and invariant synthesis [16, 24, 31]. Following their notation, we define them below.
and Juniper configurations. The tool is implemented in C#, using Microsoft’s Zen library [36] and SMT solver Z3 [20]. Evaluation Goals for CB-V ER. We seek to answer the following questions. • RQ1: Expressiveness. Is CB-V ER able to verify a variety of properties for a diverse collection of networks, including data center fat-trees [4] as well as other realworld topologies and policies?
Definition 1. A constrained Horn clause (CHC) rule has one of the following two forms:
• RQ2: Performance of verification. How well does CBV ER perform as a verifier? Does it scale on large networks and complex configurations?
∀x1 , · · · , xn . φ(⃗x) ∧ R1 (⃗x) ∧ · · · Rn (⃗x) ⇒ Rn+1 (⃗x) ∀x1 , · · · , xn . φ(⃗x) ∧ R1 (⃗x) ∧ · · · Rn (⃗x) ⇒ False
• RQ3: Usability of fault tolerance analysis. Is CB-V ER able to perform a push-button fault tolerance analysis based on CB-graph? What information can users get from that analysis?
where φ is an interpreted formula (over some first order theory) and each Ri is an uninterpreted predicate. Note that the variables in each CHC rule (x1 , · · · , xn ) are universally quantified – these quantifiers can be regarded as implicit (when not shown). A predicate Ri (⃗x) may use a subset of the variables.
Comparison of CB-V ER with other tools. We implemented a monolithic verifier (MS) based on the algorithm in Minesweeper [13], and use it as a baseline for comparison. We also compare CB-V ER with Timepiece [7], with an available artifact [6, 7] on the same benchmarks and properties, but which has different user-provided interfaces as required by Timepiece. We could not perform an experimental comparison with Lightyear [41], since the tool is not available (as confirmed by its authors). The goal is not to show that CB-V ER performs better than these other modular verifiers but rather that it is roughly similar. CB-V ER improves on these other modular verifiers in other dimensions (simplicity of interfaces, expressiveness of properties verified, fault tolerance analysis, support for interface inference).
A CHC system is an implicit conjunction of CHC rules. A solution of a CHC system is an interpretation of predicates Ri (typically in the form of formulas in some first-order theory) such that all CHC rules are valid. A CHC solver (such as Spacer/Z3 [32]) searches for a solution; a CHC system is called infeasible if no such solution exists. For our problem of automated synthesis of abstract interfaces, we formulate CHC rules based on the VCs we showed earlier, but where Iv , Qv are now uninterpreted predicates to be solved, rather than interpreted predicates provided by a user. The CB-graph (CBRoot ⊆ V , CBEdge ⊆ E) is provided by the user, property Yv and network logic (initv , f(u,v) ) are interpreted (based on the network configurations). The complete CHC system for the network interface synthesis problem is shown in Fig. 5. Each VC from Fig. 3 (listed in the first column here), is applied accordingly to a node v, an edge (u, v), a CB-root, or a CB-edge (listed in the second column here), to formulate a CHC rule (listed in the last column). Note that VCCBroot results in two CHC rules to conform to the definition of CHCs. We have developed a prototype synthesis tool called CB2IQ based on the above CHC formulation. Note that the userprovided CB-graph must be connected, to ensure soundness via Theorem 1. In our tool, we use BFS traversal on the CB-graph to ensure its connectedness, before we invoke the CHC solver. If a CHC solution exists, it corresponds to an interpretation of the Qv , Iv predicates that make all CHC rules valid, which corresponds to successful verification with all VCs passing.
6
Evaluation of CB-2IQ for automated interface synthesis. CB-2IQ translates the CHC rules (Fig. 5) into SMTLib format [12] and uses Spacer [31, 32] (version 4.13.0, part of Z3) to solve the CHC problem. To simplify the theory encoding into CHC, we use a simpler BGP model, where we consider only two BGP communities and model the IP prefix as a single bit (instead of a bitvector with 32 bits). We use the same simplified BGP model in CB-2IQ and the MS verifier used for baseline comparison.
6.1
Benchmarks and Setup
We worked with three sets of benchmarks: (1) synthetic fattree networks, parameterized by the size of the network (from 20 nodes to 2000 nodes), (2) Internet2, a real wide-area network of about 300 nodes with over 100,000 lines of Juniper configurations; (3) Batfish tutorial networks, with two example networks. All benchmarks are available in an anonymous repository (see Appendix A).
Implementation and Evaluation
We have developed a prototype implementation of CB-V ER, using Batfish [22] to extract the network model from Cisco 9
Interpreted: Uninterpreted:
Yv : R → B, initv ∈ R, f(u,v) : R → R Iv , Qv : R → B
VC
For each
CHC rule
VCInit (v)
v ∈V
sv = initv ⇒ Iv (sv )
VCProp (v)
v ∈V
¬Yv (sv ) ∧ Qv (sv ) ⇒ False
VCInv ((u, v))
(u, v) ∈ E
s′v = sv ⊕ f(u,v) (su ) ∧ Iu (su ) ∧ Iv (sv ) ⇒ Iv (s′v )
v ∈ CBRoot
sv = initv ⇒ Qv (sv )
VCCBroot (v)
v ∈ CBRoot and (u, v) ∈ E
s′v = sv ⊕ f(u,v) (su ) ∧ Iu (su ) ∧ Qv (sv ) ⇒ Qv (s′v )
VCCBedge (u, v)
(u, v) ∈ CBEdge
s′v = sv ⊕ f(u,v) (su ) ∧ Qu (su ) ∧ Iv (sv ) ⇒ Qv (s′v )
Figure 5: CHC system for the network interface synthesis problem, given the CB-graph. B = {True, False} is the Boolean domain, variables su , sv , s′v in CHC rules are universally quantified implicitly. Synthetic fattrees.
Batfish tutorial networks. Two examples are drawn from Batfish tutorials [43, 47]. One example involves a school with 13 routers running BGP. The other (the network in Figure 4) has 13 routers distributed across Asia, Europe, and the US. We verify reachability and AS path length properties for the first network, and verify reachability to Houston in the second network.
We consider four different properties:
• Reachability: all nodes must have reachability to a fixed destination; • PathLength: the selected route at all nodes (to a fixed destination) must be the shortest path; • ValleyFree: the selected route at all nodes (to a fixed destination) must not be a valley (up-down-up);
Experimental setup. All experiments were run on a Linux server with 16 Intel(R) Xeon(R) CPUs and 252GB memory. We run the CB-V ER and Timepiece modular verifiers in parallel using all 16 CPUs, and run the monolithic verifier (which is not easily parallelizable) on 1 CPU.
• Hijack: certain routes from an external "hijacker" node must be blocked from the internal network. These properties are the same as those used in Timepiece [7] (note that Lightyear does nort support the properties in PathLength and ValleyFree benchmarks). Additional details and full specifications are available in Appendix E.
6.2
Evaluation Results for CB-V ER
Fattrees. We verified four properties on different sizes of fattrees, from 20 nodes to 2000 nodes. The evaluation results (Figure 6) show the performance of CB-V ER, Timepiece, and the baseline monolithic verifier (MS) for different properties. Each graph plots the number of nodes in the network against the wall-clock time (in seconds) on a log scale, with a timeout of 24 hours. Note that CB-V ER successfully verifies all properties on all networks. This answers RQ1 positively: CB-V ER is able to express and verify these properties deemed useful by network operators. Regarding RQ2, these graphs show that CB-V ER is able to verify (all properties) on a 2000-node fattree networks within 20 minutes, whereas the monolithic verifier (MS) has many timeouts, e.g., it fails to verify the Hijack property on a 180-node fattree. The performance of CB-V ER is generally comparable with Timepiece, marginally better for the ValleyFree benchmark, but worse in the Reachability benchmark (where the CB-graph generation and connectedness check in CB-V ER is more of an overhead with a simple property).
Internet2. The Internet2 benchmark tests CB-V ER on a real-world wide-area network [1], which contains 293 nodes (including 10 internal routers and 283 external neighbors). We use a snapshot of Internet2’s configurations [45] that has been reported to violate some properties. 4 We consider three properties: • BlockToExternal property (first presented in Bagpipe [45]): check that internal routes with a BTE community are not advertised to Internet2’s peers. • NoMartian property (first presented in Bagpipe [45]): check that internal routes should not select routes with external Martian prefixes as destination. • InternalReachability property: check that internal nodes should be able to advertise themselves to other internal nodes. 4 Some features used by Internet2, e.g., IPv6, next-hop self, are not mod-
eled. These do not affect our evaluation.
10
Verification time (s)
CB-V ER
Timepiece
MS
Timeout
104 102 100 0
1,000 2,000 0
1,000 2,000 0
1,000 2,000 0
#Nodes
#Nodes
#Nodes
(a) Reachability (b) PathLength (c) ValleyFree
1,000 2,000 #Nodes (d) Hijack
Figure 6: Evaluation results for CB-V ER on fattree networks, compared with Timepiece (a modular verifier) and MS (a Minesweeper-style monolithic verifier).
6.3 Evaluation Results for Automated Interface Synthesis
Internet2.
CB-V ER spends 22s (seconds) to verify the BlockToExternal property and reports 3 (true) violations (in phase 1). CB-V ER spends 121s to verify the NoMartians property and reports one violation. Finally, CB-V ER spends 74s successfully verifying InternalReachability (CBV ER constructs one CB-graph per destination, increasing the
We perform the experiments on the synthetic fattree benchmarks, reusing all the four properties described earlier. The CB-graph we provided is in BFS order from the destination. Fig. 7 shows the evaluation results. Each graph plots the number of nodes and the wall-clock time (in seconds) on a log scale, with a timeout of 1 hour. (Due to a simplified BGP model, the performance of MS here is better than in Fig. 6.) In almost all experiments (except one), CB2IQ is faster than monolithic verification in MS. In the best improvement against MS, CB-2IQ is 22-27x faster for checking Reachability. In the least improvement, CB-2IQ is 1.3x faster for checking ValleyFree. We also see some fluctuations in performance of automated synthesis, e.g., in Pathlength and Hijack, possibly due to some heuristics in Spacer. (These fluctuations were reproduced multiple times in our experiments.) These results are encouraging for interface synthesis: they show that even with an out-of-the-box CHC solver (not necessarily modular), CB-2IQ already shows an improvement against monolithic verification. In future work, we would like to investigate the potential of implementing interface synthesis using a specialized modular solver over the network.
analysis time here). In comparison, the monolithic verifier (MS) is unable to solve BlockToExternal, throwing an outof-memory error after 56 minutes.
Batfish tutorial networks. CB-V ER spends 0.4s to verify the reachability property in the school network, and also 0.4s to verify the AS path length property (i.e., AS paths are of length 2 or less). It spends 0.5s to verify the reachability property in the cross-world network. Since MS has limitations in handling IGP, it gave a counterexample, which is actually spurious.
Fault tolerance analysis. To answer RQ3, we run the fault tolerance analysis on each benchmark that passes the validity checks. For the largest fattree network benchmark, CBV ER finds that the 2000-node fattree network (k=40) can tolerate 19-edge failures forReachability (spending 14s for checking connectivity) and for Hijack (spending 19s). In Pathlength (spending 7s) and ValleyFree (spending 8s), top-of-rack routers (also called edge routers) can tolerate 19-edge failures, while core and aggregation routers do not tolerate any edge failure.
7
Related Work
Modular Network Verification. CB-V ER was inspired by recent research on modular network verification [5, 7, 28, 41]. It focuses on a broad, new category of eventually-stable properties, has different (simpler, we would argue) interfaces, adds failure analysis, and comes with an additional tool for interface synthesis. In addition to Timepiece and Lightyear (discussed in detail earlier, §2), RCDC [28] was a pioneer in modular network verification. It was customized for checking invariants of Azure data centers, but was not engineered for other settings. Kirigami [5] asked a user to exactly identify the concrete converged state of a network, a difficult task requiring exact knowledge of network internals.
In the Internet2 benchmark, CB-V ER spends 23ms (milliseconds) for fault tolerance analysis in InternalReachability, and finds the whole network tolerant to 8-edge failures. In the Batfish tutorial benchmarks, CB-V ER finds the school network can tolerate 1-edge failure for reachability, but does not tolerate any edge failure for AS path length property. In the second (cross-world) network, CB-V ER finds the routers in Asia (at Hong Kong, Milan, Singapore, and Tokyo) do not tolerate any edge failure, while other routers can tolerate 1-edge failures (as discussed earlier, §4.2). Each failure analysis takes 8 ms. 11
Verification time (s)
CB-2IQ
MS
Timeout
103 101 10−1 0
1,000 2,000 0
1,000 2,000 0
1,000 2,000 0
#Nodes
#Nodes
#Nodes
(a) Reachability (b) PathLength (c) ValleyFree
1,000 2,000 #Nodes (d) Hijack
Figure 7: Evaluation results for automated interface synthesis (CB-2IQ), compared with a monolithic verifier (MS). Control plane verification. Our work is more broadly related to prior efforts on network control plane verification [3, 13–15,23,38,39,44–46]. Bagpipe [45] and Minesweeper [13] use SMT-based verification, but are monolithic verifiers. ARC [23] and Tiramisu [3] reduce verification problems to efficient graph analyses, but do not handle all network features. Plankton [38], Hoyan [46], and Expresso [44] combine a mix of symbolic analyses and simulation to improve scalability. Bonsai [14] uses symmetry-based abstractions, Shapeshifter [15] uses abstractions on routing fields, and ACORN [39] uses route nondeterminism to improve scalability — these abstractions are orthogonal to modular verification. There are prior efforts that aim to check concrete convergence of control planes, and to identify conditions under which (unique) convergence is guaranteed for different kinds of routing protocols [19, 26, 40]. However, practical networks sometimes use rich routing policies that do not follow these conditions. More importantly, our work is largely orthogonal to efforts that check for (concrete) convergence of routing protocols: our system does not check for concrete convergence; its goal is to verify important network- and policy-specific routing path properties such as reachability and route preferences, which have been known to cause many real-world failures and/or security vulnerabilities.
the usual invariants I, we use interfaces Q to prove properties that are eventually-stable.
8
Conclusion
We developed CB-V ER, a new tool for verifying eventuallystable control plane properties in a modular way, based on the ideas of abstract convergence and synthesis of a convergesbefore (CB) graph from given component interfaces. We prove our verifier correct in Lean, and illustrate its benefits in fault tolerance analysis. We evaluate CB-V ER on a collection of benchmark examples, illustrating its expressiveness and utility. Given a CB-graph, we also perform automated interface synthesis and show its effectiveness in practice.
9
Acknowledgements
We thank Mia Kaarls for her work in development of parts of the frontend and the backend of CB-V ER.
References [1] Internet2. https://internet2.edu, 2013. https: //en.wikipedia.org/wiki/2022_Rogers_ Communications_outage.
[2] 2022 rogers communications outage. Data plane verification. While the network control plane, which is the object of study for CB-V ER, makes decisions about the routes chosen, the network data plane is responsible for forwarding packets. Much work has also been done on data plane verification [29, 30, 34, 35]. Since data plane policies and semantics differ substantially from those of the control plane, the two systems require different kinds of verifiers.
[3] Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast multilayer network verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 201–219, 2020.
Program verification and invariant synthesis. CHC solvers have been widely used in program verification and invariant synthesis [16, 24, 31]. In these methods, the CHC rules are formulated along edges in the program’s control flow graph, which naturally provides an ordering during program execution. In network control planes, the network graph itself does not provide an ordering on route transfers, but our CB-graph provides a witness for such an ordering in eventually-stable executions of the network. In addition to
[4] Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. A scalable, commodity data center network architecture. ACM SIGCOMM computer communication review, 38(4):63–74, 2008. [5] Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Kirigami, the verifiable art of network cutting. In 2022 IEEE 30th International Conference on Network Protocols (ICNP), pages 1–12, 2022. 12
[6] Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Artifact associated with the pldi 2023 submission "modular control plane verification via temporal invariants"., 2023.
Occasion of His 75th Birthday, volume 9300 of Lecture Notes in Computer Science, pages 24–51. Springer, 2015.
[7] Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Modular control plane verification via temporal invariants. Proceedings of the ACM on Programming Languages, 7(PLDI):50–75, 2023.
[17] Matt Brown, Ari Fogel, Daniel Halperin, Victor Heorhiadi, Ratul Mahajan, and Todd Millstein. Lessons from the evolution of the batfish configuration analysis tool. In Proceedings of the ACM SIGCOMM 2023 Conference, pages 122–135, 2023.
[8] Timothy Robin Alberdingk Thijm. Modular Control Plane Verification. PhD thesis, Princeton University, 2024.
[18] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In CAV, pages 154–169, 2000.
[9] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design, pages 1–8. IEEE, 2013.
[19] Matthew L Daggitt, Alexander JT Gurney, and Timothy G Griffin. Asynchronous convergence of policy-rich distributed bellman-ford routing protocols. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 103–116, 2018. [20] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008.
[10] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 415–442. Springer, 2022.
[21] Yefim Dinitz. Dinitz’ Algorithm: The Original Version and Even’s Version, pages 218–240. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006.
[11] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.
[22] Ari Fogel, Stanley Fung, Luis Pedrosa, Meg WalraedSullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 469–483, 2015.
[12] Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010.
[23] Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. Fast control plane analysis using an abstract representation. In Proceedings of the 2016 ACM SIGCOMM Conference, pages 300–313, 2016.
[13] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. A general approach to network configuration verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, pages 155–168, 2017. [14] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Control plane compression. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 476–489, 2018.
[24] Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pages 405–416. ACM, 2012.
[15] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract interpretation of distributed network control planes. Proceedings of the ACM on Programming Languages, 4(POPL):1–27, 2019.
[25] Timothy G Griffin, F Bruce Shepherd, and Gordon Wilfong. The stable paths problem and interdomain routing. IEEE/ACM Transactions On Networking, 10(2):232– 243, 2002.
[16] Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the
[26] Timothy G Griffin and Joäo Luís Sobrinho. Metarouting. In Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications, pages 1–12, 2005. 13
Zen. https://github.com/ microsoft/Zen/tree/master.
[27] Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. Validating datacenters at scale, 2019. Presentation at SIGCOMM 2019.
[36] Microsoft.
[37] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021.
[28] Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. Validating datacenters at scale. In Proceedings of the ACM Special Interest Group on Data Communication, SIGCOMM ’19, page 200–213, New York, NY, USA, 2019. Association for Computing Machinery.
[38] Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. Plankton: Scalable network configuration verification through model checking. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 953–967, 2020. [39] Divya Raghunathan, Ryan Beckett, Aarti Gupta, and David Walker. Acorn: Network control plane abstraction using route nondeterminism. In FMCAD, pages 261– 272, 2022.
[29] Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 113– 126, 2012.
[40] Joao L Sobrinho. An algebraic theory of dynamic network routing. IEEE/ACM Transactions on Networking, 13(5):1160–1173, 2005.
[30] Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. Veriflow: Verifying network-wide invariants in real time. In Proceedings of the first workshop on Hot topics in software defined networks, pages 49–54, 2012.
[41] Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman, Tejas Patil, Todd Millstein, and George Varghese. Lightyear: Using modularity to scale bgp control plane verification. In Proceedings of the ACM SIGCOMM 2023 Conference, pages 94–107, 2023.
[31] Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. Smt-based model checking for recursive programs. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification, pages 17–34, Cham, 2014. Springer International Publishing.
[42] Aydin Üresin and Michel Dubois. Parallel asynchronous algorithms for discrete data. Journal of the ACM (JACM), 37(3):588–606, 1990. [43] Harsh Verma and Dan Halperin. Introduction to route computation and analysis using batfish. https:
[32] Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. Smt-based model checking for recursive programs. Formal Methods in System Design, 48(3):175–205, 2016.
//github.com/batfish/pybatfish/blob/ master/jupyter_notebooks/Introduction% 20to%20Route%20Analysis.ipynb, August 2018.
[33] Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. In Concurrency: the Works of Leslie Lamport, pages 179–196. 2019.
[44] Dan Wang, Peng Zhang, and Aaron Gember-Jacobson. Expresso: Comprehensively reasoning about external routes using symbolic simulation. In Proceedings of the ACM SIGCOMM Conference, pages 197–212. ACM, 2024.
[34] Nuno P Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Checking beliefs in dynamic networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 499–512, 2015.
[45] Konstantin Weitz, Doug Woos, Emina Torlak, Michael D Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Scalable verification of border gateway protocol configurations with an smt solver. In Proceedings of the 2016 acm sigplan international conference on objectoriented programming, systems, languages, and applications, pages 765–780, 2016.
[35] Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P Brighten Godfrey, and Samuel Talmadge King. Debugging the data plane with anteater. ACM SIGCOMM Computer Communication Review, 41(4):290–301, 2011. 14
[46] Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, et al. Accuracy, scalability, coverage: A practical configuration verifier on a global wan. In Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication, pages 599–614, 2020.
This definition is formalized as Network in Lean. Note that instead of defining ∞ and ⊕, we use existing type classes OrderTop and SemilatticeInf in Mathlib. Definition 3 (Asynchronous schedule). A schedule of a network N is a pair (α, β) where • α : T → 2V is the activation function. • β : E → (T → T) is the data flow function (we also write β(e) as βe ).
[47] Yifei Yuan. Analyzing the impact of failures (and letting loose a chaos monkey). https://github.com/
• β satisfies the casuality axiom that messages are delivered after sent, i.e.,
batfish/pybatfish/blob/master/jupyter_ notebooks/Analyzing%20the%20Impact%20of% 20Failures%20(and%20letting%20loose%20a% 20Chaos%20Monkey).ipynb, December 2018.
∀e. ∀t > 0. βe (t) < t. This definition is formalized as Schedule in Lean. Definition 4 (Network semantics). The network semantics of a network N respect to a schedule S = (α, β) is a function σS : V × T → S defined as I(v) t =0 σS (v,t − 1) t > 0∧v ∈ / α(t) L σS (v,t) = init(v) ⊕ f (σ (u, β (t))) (u,v) u (u,v) S t > 0 ∧ v ∈ α(t) (2) This definition is formalized as Schedule.sem in Lean.
Repository for Lean formalization and benchmarks
A
The benchmarks are presented in https://github.com/ dz7903/cbgraphs-benchmarks, and the Lean formalization is presented in https://github.com/dz7903/ cbgraphs-formalization. We plan to release our tool in future.
B
Key definitions and theorems
Now we present several conditions related to the fairness of a schedule.
We provide a catalog of key definitions and theorems used in §3 and §4 in this section, and connect them with Lean definitions and proofs, which are presented in the repository in §A. Every theorem we present in these sections has a formalized proof in Lean.
Definition 5. Let S = (α, β) be a schedule on a network N. • A node v is said eventually activated (EA) if it is activated in α infinitely often, i.e., ∀T. ∃t ≥ T. v ∈ α(t).
B.1
Key definitions
• An edge e is said eventually delivering (ED) if it deliver messages infinitely often, i.e.,
We quickly review the definitions of a network instance N, an asynchronous schedule S and the network semantics respect to N and S, which have been presented in §3.
∀T. ∃t ≥ T. βe (t) ≥ T.
Definition 2 (Network instance). A network is a 5-tuple N = (G, R, init, f , ⊕) where
Note this is a very weak condition; it does not require every message being delivered, just delivering messages infinitely often.
• G = (V, E) is the directed graph with nodes V and edges E.
• An edge e is said eventually flushed (EF) if no message at a certain time is sent infinitely often (messages up to that time must be flushed away since a certain time), i.e.,
• R is the set of routes. We assume a maximal element ∞ ∈ R.
∀T. ∃T ′ ≥ T. ∀t ≥ T ′ . βe (t) ≥ T.
• init : V → S is the initial routes for each node. • An edge e is said delivering in order (DO) if the order of messages being received is the same as the order being sent, i.e.,
• f : E → (S → S) are transfer functions. We may write f (e) as fe . • ⊕ : S × S → S is a binary associative, commutative and selective function (the merge function).
∀t1 ,t2 . t1 ≤ t2 ⇒ βe (t1 ) ≤ βe (t2 ). 15
These definitions are formalized as
We define interfaces and verification conditions in bundle as follows.
• NodeEventuallyActivated ,
Definition 8. A verification condition structure over a network N includes:
• EdgeEventuallyDelivering , • EdgeEventuallyFlushed and
• interfaces and properties (I, Q,Y ),
• EdgeOrdered
• and a CB-graph CB = (CBRT,CBEG) (in practice this CB-graph is inferred by CB-V ER), such that
in Lean.
• the verification conditions in Figure 3 all hold, and
All these conditions are reasonable since BGP-over-TCP guarantees messages are delivered eventually and in-order. The relationships between edge-level assumptions (ED, EF and DO) are:
This definition is formalized as VC in Lean.
Theorem 4. We have the following implications:
Finally, for a verification condition structure, we define
• the CB-graph CB is connected.
Definition 9. A node v ∈ V abstractly converges to Q(v) under schedule S if
• EF implies ED. • ED and DO implies EF.
∃τ. ∀t ≥ τ. σS (v,t) ∈ Q(v).
These theorems are formalized as • eventuallyFlushed_implies_eventuallyDelivering and
This definition is formalized as AbstractlyConverge in Lean.
• ordered_and_eventuallyDelivering_implies_eventuallyFlushed
B.2
in Lean.
Theorems
We present formal version of Theorem 1, Theorem 2 and Theorem 3, with several key lemmas formalized in Lean. The first lemma shows I(v) holds for any time t and any schedule:
In our assumption of fairness, we require EA (for nodes) and EF (for edges). From the theorem above we see this assumption is quite weak. We assume EA always, and assume EF for non-failed edges. That is, when we talk about k failures, we mean k edges violate EF. The formal definition of fairness is
Lemma 1. Given verification conditions hold, for any schedule S, any time t ∈ T and node v ∈ V ,
Definition 6 (Fairness). A schedule S is fair if every node is eventually activated and every edge is eventually flushed. S is fair with at most k failures if every node is eventually activated and all edges in E − F (where F are failed edges with |F| ≤ k) are eventually flushed. These definitions are formalized as Schedule.Fair and Schedule.FairWithFailure in Lean.
σS (v,t) ∈ I(v). Proof sketch. Induction on t and do case analysis on t = 0 (which uses VCInit ), t > 0 ∧ v ∈ / α(t) (inductive hypothesis) and t > 0 ∧ v ∈ α(t) (VCInv and inductive hypothesis). This lemma is formalized as VC.invariance in Lean.
We also define the concept of connectedness and k-failconnectivity:
The second lemma and its corollary shows CB-roots satisfy their semantics definition and therefore abstractly converge:
Definition 7 (Connectedness). In a graph G = (V, E), let RT ⊆ V be a set of nodes and EG ⊆ E be a set of edges. We say a node v is connected under (RT, EG) if there exists a path in EG from a node u ∈ RT to v, and (RT, EG) itself is connected if every node v ∈ V is connected under it. We say a node v is k-fail-connected under (RT, EG) if it is connected under (RT, EG − F) for any F ⊆ EG with |F| ≤ k, and (RT, EG) itself is k-fail-connected if every node is kconnected under it. These definitions are formalized as Graph.Connected and Graph.ConnectedWithFailure in Lean.
Lemma 2. Given verification conditions hold, for any schedule S, any v ∈ CBRT and any time t, σS (v,t) ∈ Q(v). Proof sketch. Induction on t and do case analysis on t = 0 (which uses the first part of VCCBroot ), t > 0 ∧ v ∈ / α(t) (inductive hypothesis) and t > 0 ∧ v ∈ α(t) (the second part of VCCBroot and Lemma 1). This lemma is formalized as VC.cbroot in Lean. Corollary 1. Given verification conditions hold, for any schedule S and any v ∈ CBRT , it abstractly converges to Q(v). 16
Proof sketch. Pick τ = 0 and this is Lemma 2. This lemma is formalized VC.cbroot_abstractly_converge in Lean.
Finally, we formally state Theorem 2 and Theorem 3. The proofs are direct application of Theorem 1 and VCProp .
as
Theorem 2. Given verification conditions hold, for any fair schedule S and any node v ∈ V ,
The third lemma and its corollary shows CB-edges satisfy their semantics definition and therefore form the inductive steps of abstract convergence:
∃τ. ∀t ≥ τ. σS (v,t) ∈ Y (v). This theorem is formalized as VC.correctness in Lean.
Lemma 3. Given verification conditions hold, for any schedule S and e = (u, v) ∈ CBEG, if σS (u, β(u,v) (t)) ∈ Q(u) and v ∈ α(t), then σS (v,t) ∈ Q(v).
Theorem 3. Given verification conditions hold, for any schedule S that is fair with at most k failures, if the CB-graph CB is k-fail-connected, then for any node v ∈ V ,
Proof sketch. Note that
∃τ. ∀t ≥ τ. σS (v,t) ∈ Y (v).
σS (v,t) = σS (u, β(u,v) (t)) ⊕ init(v) ⊕
M
This
σS (u′ , β(u′ ,v) (t))
theorem
is
formalized
as
VC.correctness_with_failure in Lean.
(u′ ,v)∈E,u′ ̸=u
C
(noted as σS (v,t) = s1 ⊕ s2 ). By VCInit , VCInv and Lemma 1 we have s2 ∈ I(v). Then by VCCBedge we have σS (v,t) ∈ Q(v). This lemma is formalized as VC.cbedge in Lean.
Error Debugging Process
Figure 8 presents how a user of CB-V ER can debug the VC violations found during Algorithm 1. The top part (separated by a double-line from the bottom part) describes violations in the essential VCs (VCInit , VCInv or VCProp ) that result in immediate failure in phase 1; the bottom part describes VC violations (in VCCBroot ,VCCBedge ) that are saved in phase 1, to possibly recover from a failure in phase 2 if the connectedness check on the constructed CB-graph fails. We now explain some cases in Figure 8 with more details below.
Corollary 2. Given verification conditions hold, for any schedule S and e = (u, v) ∈ CBEG, if v is eventually activated, e is eventually flushed in S, and u abstractly converges to Q(u), then v abstractly converges to Q(v). Proof sketch. Suppose σS (u,t) ∈ Q(u) for any t ≥ t1 . By the fairness conditions (EA and EF) there is a time t2 > t1 such that v ∈ α(t2 ) and ∀t ≥ t2 . β(u,v) (t) ≥ t1 . Now for any t ≥ t2 we show σS (v,t) ∈ Q(v) by induction on t and case analysis on t > t2 ∧ v ∈ / α(t) (inductive hypothesis) and t ≥ t2 ∧ v ∈ α(t) (Lemma 3). This lemma is formalized as VC.cbedge_abstractly_converge in Lean.
Violation of VCInv . To illustrate the process in detail, consider a violation of VCInv (shown in Fig. 8). Recall that VCInv (shown earlier in Fig. 3) states: ∀su , sv . su ∈ I(v) ∧ sv ∈ I(v) ⇒ sv ⊕ f(u,v) (su ) ∈ I(v). When this VC check fails, a counterexample is an assignment to su and sv such that the formula is false. That is, su ∈ I(u) and sv ∈ I(v) are true, but sv ⊕ f(u,v) (su ) ∈ I(v) is false (shown in column 1, Fig. 8). To diagnose the cause of this VC violation, the user performs a case analysis based on their beliefs (cases shown in column 2). They first decide whether su and sv are plausible routes that could be selected at nodes u and v, respectively, based on their beliefs about the routing behavior at u and v. Plausibility indicates whether the user believes that such su and sv can occur in a real simulation; in the case of VCInv this means there exists a schedule S such that su and sv are selected by u and v at some time. The first case (case 1 in the second column) is if one or both of su , sv are not plausible. In this case, the corresponding I(u) or I(v) is considered erroneous, i.e., it is too weak. To fix this, the interface I(u) or I(v) should be strengthened, i.e., it should be made more restrictive by excluding su and/or sv . Otherwise, if both su and sv are plausible, the user will next examine s′v = sv ⊕ f(u,v)(su ) , the newly selected route at v. Note that s′v does not belong to I(v) according to the counterexample. If s′v is plausible (case 2), then I(v) is too strong and
We now formally state Theorem 1 and its improved version: Theorem 1. Given verification conditions hold, for any fair schedule S and any node v ∈ V , v abstractly converge to Q(v) at some time τv . Proof sketch. By induction on the connectedness of CBgraph, the base step is Corollary 1 and the inductive step is Corollary 2. This theorem is formalized as VC.connected_cbgraph in Lean. Theorem 1, improved. Given verification conditions hold, for any schedule S that is fair with at most k failures, and any node v ∈ V , if v is k-fail-connected under the CB-graph CB, then v abstractly converge to Q(v). Proof sketch. By induction on the connectedness of CBgraph excluding all failed edges in S. The remained is the same as proof of Theorem 1 This theorem is formalized as VC.connected_cbgraph_with_failure in Lean. 17
VC and Counterexample
User Beliefs
Cause and Suggested Action
VCInit is violated: sv = init(v) ∈ / I(v)
case 1: sv ✗
init(v) is wrong, bug in configuration
case 2: sv ✓
I(v) is too strong, weaken it
VCInv is violated: su ∈ I(u), sv ∈ I(v),
case 1: su or sv ✗
I(u) or I(v) is too weak, strengthen it
case 2: su , sv and s′v ✓
I(v) is too strong, weaken I(v)
s′v = sv ⊕ f(u,v) (su ) ∈ / I(v)
case 3: s′v ✗
f(u,v) is wrong, use repair algorithm
VCProp is violated: sv ∈ Q(v), sv ∈ / Y (v)
case 1: sv ✗
Q(v) is too weak, strengthen it
case 2: sv ✓
property Y (v) fails on a plausible route
case 1: v should not be a CB-root
skip this counterexample
case 2: sv ✗
init(v) is wrong, bug in configuration
case 3: sv ✓
Q(v) is too strong, weaken it
case 1: v should not be a CB-root
skip this counterexample
case 2: su or sv ✗
I(u) or Q(v) is too weak, strengthen it
case 3: su , sv and s′v ✓
Q(v) is too strong, weaken it
case 4: s′v ✗
f(u,v) is wrong, use repair algorithm skip this counterexample
VCCBedge is violated: su ∈ Q(u), sv ∈ I(v),
case 1: (u, v) should not be a CB-edge case 2: su or sv ✗
Q(u) or I(v) is too weak, strengthen it
/ Q(v) s′v = sv ⊕ f(u,v) (su ) ∈
case 3: su , sv and s′v ✓
Q(v) is too strong, weaken it
case 4: s′v ✗
f(u,v) is wrong, use repair algorithm
VCCBroot is violated (first conjunct): sv = init(v) ∈ / Q(v)
VCCBroot is violated (second conjunct): su ∈ I(u), sv ∈ Q(v), s′v = sv ⊕ f(u,v) (su ) ∈ / Q(v)
Figure 8: Debugging and Repair Process: Counterexample shows the VC violation in the first column, “sv ✓” in the second column indicates the user’s belief that route sv is a plausible route that be selected by v, and “sv ✗” indicates the user’s belief that sv is an implausible route that cannot be selected by v; the last column shows the cause and suggested action for each case.
18
from AS1 and AS3, respectively, and only allows routes with such communities to be imported to as2dept1. However, the operator makes a mistake in the configuration at as2dept1, such that it only permits routes with community 3:2. The operator wishes to verify that any routes that originate from AS2 can reach as2dept1. The operator first specifies QAS2 as the set of any reachable route, i.e., {s | s ̸= ∞} and IAS2 as the set of all routes, i.e., R (shown as step 1 in Figure 10). This results in a disconnected CB-graph, and the counterexamples of CB-edge-check at the edges (as2dist1,as2dept1) and (as2dist2-as2dept1) show that routes without community 3:2 are dropped at these edges. Thus, the operator can refine QAS2 and IAS2 to include routes with community 3:2 (shown as step 2 in Figure 10). However, this time, invariance fails; the counterexample at the edge (as1border2, as2border1) shows that a route with community 1:2 but without community 3:2 is imported at AS2, thus violating the invariant IAS2 . Because the operator believes that the route with community 1:2 is plausible in AS2, they can then refine QAS2 and IAS2 to include both communities 1:2 and 3:2 (step 3 in Figure 10). This results again in a disconnected CB-graph. The counterexamples of CB-edge-check show that routes with community 1:2 but without community 3:2 are dropped. This time, since routes with community 1:2 is plausible in AS2, the operator knows that the configurations are wrong. Therefore, the operator repairs the configuration at both edges (as2dist1, as2dept1) and (as2dist2, as2dept2) either manually or automatically, and when suitably repaired, all checks will pass after the repair.
Figure 9: Topology of a campus network taken from the Batfish tutorial [43]. should be weakened to include s′v . However, if s′v is not plausible (case 3), then the transfer function f(u,v) is considered erroneous and should be repaired. Violation of VCProp . Now, consider a failure where VCProp is violated. The first case is that the counterexample route sv is not plausible, i.e., sv is a spurious counterexample. In this case, the user can strengthen Q(v) to exclude sv during refinement. This is similar to classic counterexample guided abstraction refinement (CEGAR) [18]. However, if sv is plausible, then CB-V ER has found a bug for property Y (v). The user could either accept the reported bug, or weaken the property to Y ′ (v) and (incrementally) verify VCProp again. Violations of VCCBroot and VCCBedge . CB-V ER can fail in phase 2 if there does not exist any connected CB-graph according to VCCBroot and VCCBedge (identified in phase 1), i.e., if some nodes in the network are found to be unconnected to any CB-root via CB-edges. For an unconnected node v, VCCBroot is invalid at v, and VCCBedge is invalid for every incoming edge to v. However, unlike in phase 1 failures, not every invalid VC requires an action for repair: only that at least one of the VCs is repaired (to connect the node). Users rarely need to repair VCCBroot ; in practice CB-roots are expected to be the destination itself or border routers with direct announcements to external destinations. For repairing VCCBedge , the user can examine the node’s incoming edges and diagnose why VCCBedge fails for all of them. Repairing all the failures may not be necessary to connect the node but can provide better fault tolerance. The repair process for fixing VCCBedge is similar to that for VCInv .
D
E
Details on Benchmarks
We describe details about the formal specifications on synthetic fattree and Internet2 benchmarks in this section. Fattrees networks. We generate fattrees parameterized by the number of pods, k. The number of nodes is 1.25k2 , and the number of edges is k3 . Nodes of fattrees are divieded into edge-nodes (top-of-the-rack nodes), aggregation-nodes and core nodes, and edge-nodes and aggregation-nodes must belong to certain pods [4]. For Hijack, we add an extra "hijacker" node connecting with all the core-nodes. Our network model requires us to choose a destination when we verify any property. We always use edge0_0, the first edge-node in the first pod, as the destination. In the formulas below, we refer this destination as an constant d. The destination has an initial route with zero path length and an internal destination prefix. In Hijack, we further give the hijacker-node an arbitrary initial route with an internal destination, to "hijack" the internal routes. Also, our fattree network uses eBGP only; every node is assigned a different AS number.
Error Debugging Process: an Example
Figure 9 shows the topology of a campus network taken from Batfish tutorial [43]. Figure 10 shows an example of the debugging process based on the network in Figure 9. Suppose the network operator modifies the configuration by adding communities 1:2 and 3:2 when routes are imported to AS2 19
Step 1
Interface
Failed check and location
Cause
Action
QAS2 = {s | s ̸= ∞},
CB-edge-check at edges (as2dist1, as2dept1) and (as2dist2, as2dept1)
as2dept1 will drop route without community 3:2
Refine QAS2 and IAS2
Invariance at edge (as1border2, as2border1)
as2border1 can select a route without community 3:2 (but with 1:2)
Refine QAS2 and IAS2
CB-edge-check at edges (as2dist1, as2dept1) and (as2dist2, as2dept1)
as2dept1 wrongly dropped routes with community 1:2
Repair f(as2dist1,as2dept1) and f(as2dist2,as2dept1)
IAS2 = R ( QAS2 =
2
4
s
QAS2 = s IAS2 = s
)
∧ 3 : 2 ∈ tag(s) ) s=∞
( IAS2 =
3
s ̸= ∞
s
∨ 3 : 2 ∈ tag(s)
s ̸= ∞ ∧
1 : 2 ∈ tag(s)
!
∨ 3 : 2 ∈ tag(s)
s=∞ ∨
!
1 : 2 ∈ tag(s)
∨ 3 : 2 ∈ tag(s)
same as above
all checks pass!
Figure 10: Error debugging process: an example (for the network in Fig. 9). Reachability. In Reachability benchmark the policies between routers are simply forward any routes (that is, a single permit action). The properties to be verified are:
Valley-free. In ValleyFree we check the valley-free property in fattrees, i.e., no valley path (up-down-up path) is selected. To ensure this property, we modify the policies so that:
Y (v) = {s | s ̸= ∞}.
• If a route is advertised through a “down” link (core to aggregation or aggregation to edge), a community tag 1:0 will be added.
We specify interfaces as follows: I(v) = {s | s = ∞ ∨ s ̸= ∞}
• Routes with community tag 1:0 will be dropped along “up” links (aggregation to core or edge to aggregation).
Q(v) = {s | s ̸= ∞}
We verify that each node will be reachable (reachability), and nodes that connect with destination with only “up” links (we call such nodes the uphill nodes, and write uphill(d) as the set of all the uphill nodes when destination is d) will not select a route with community tag 1:0.
Path length. In PathLength benchmark the policies are the same as Reachability. We want to verify a stronger property that each router will select the shortest path to destination finally: Y (v) = {s | s ̸= ∞ ∧ len(s) = dist(v)}
Y (v) = {s | s ̸= ∞ ∧ (v ∈ uphill(d) ⇒ 1 : 0 ∈ / comm(s))}
where dist(v) is the distance between node v and the destination, and len(s) is the path length field in BGP route s. To prove this property, we need to specify that:
where comm(s) is the field of community tags of the BGP route s. Similar with Reach and AS-Length, due to asynchrony, a route with tag 1:0 is allowed to be selected before convergence, but such routes must not be shortest route. The interfaces should be specified as lp(s) = 100 ∧ len(s) ≥ dist(v) ! I(v) = s s = ∞ ⇒ len(s) = dist(v) ∧ v ∈ uphill(d) ∧ ⇒1:0∈ / comm(s) ( ) s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) = dist(v) Q(v) = s ∧ (v ∈ uphill(d) ⇒ 1 : 0 ∈ / comm(s))
1. The local preference of routes are the same as the default value (100), so that longer paths do not have higher local preference to be selected; 2. Before convergence, the router may select another route, but the length must not be less than the distance dist(v). Therefore, the interfaces for PathLength are I(v) = {s | s = ∞ ⇒ lp(s) = 100 ∧ len(s) ≥ dist(v)} Q(v) = {s | s ̸= ∞ ∧ lp(s) = 100 ∧ len(s) = dist(v)} 20
Hijack. In Hijack we add a hijacker connecting with all core nodes as an external node that can advertise any route from outside. The policies within the fattree are the same as those in Reachability property (a single permit action). However, the import policies at core nodes from the hijacker will drop the route if it has an internal prefix. Also, the hijacker-node does not accept any route from the fattree (by dropping routes from core nodes). We want to verify that no route coming from hijacker should be selected (route filtering property). To check whether a route is from hijacker or not, we utilize the AS path field in BGP — for a BGP route s, we use ASPath(s) as the set of AS numbers in its AS path field. We also use IntPrefixes as the set of internal prefixes and HijackAS as the AS number of hijacker. We specify the properties as
No-martians. In NoMartians, we verify that no routes with a martian prefix (which is a list of certain IP prefixes) can be selected by an internal node. We give the destination (which is an external node) arbitrary initial route. We then verify that ( {s | s ̸= ∞ ⇒ prefix(s) ∈ / MartianPrefix} v ∈ InternalNode Y (v) = {s | True} v ∈ ExternalNode
( {s | s ̸= ∞ ∧ HijackAS ∈ / ASPath(s)} v ̸= hijacker Y (v) = {s | True} v = hijacker
The interfaces are easy. The are specified the same as the property itself. I(v) = Q(v) = Y (v)
The interfaces are specified as follows (note that I(hijacker) = Q(hijacker):
Internal reachability. In InternalReachability, we verify that any route advertised by an internal node will be selected by other internal nodes (actually, Internet2’s policies between internal nodes do not drop or modify routes). We still give an arbitrary initial route for the destination. We verify that ( {s | s ̸= ∞} v ∈ InternalNode Y (v) = {s | True} v ∈ ExternalNode
( {s | s = ∞ ∨ HijackAS ∈ / ASPath(s)} I(v) = {s | s ̸= ∞ ∧ prefix(s) ∈ IntPrefixes} ( {s | s ̸= ∞ ∧ HijackAS ∈ / ASPath(s)} Q(v) = {s | s ̸= ∞ ∧ prefix(s) ∈ IntPrefixes}
The interfaces are specified as {s | s ̸= ∞ ⇒ BTE ∈ comm(s)} v ∈ InternalNodes ∧ BTE ∈ comm(init(d)) {s | s = ∞} I(v) = Q(v) = v ∈ ExternalNodes ∧ BTE ∈ comm(init(d)) {s | True} BTE ∈ / comm(init(d))
v ̸= hijacker v = hijacker v ̸= hijacker v = hijacker
with interfaces Internet2 network. The Internet2 network has 10 internal nodes (sometimes we also refer as core nodes) and 283 external nodes. We consider multiple destination; in BlockToExternal and InternalReachability the destination could be any internal node, while in NoMartians the destination could be any external node. In either case, we use d as a symbolic variable representing the destination. The CB-graph will be generated and checked on connectedness for each concrete destination.
I(v) = {s | True} Q(v) = Y (v)
Block-to-external. In BlockToExternal property we want to verify that internal routes with a BTE community will not be advertised to the external peers. In configuration, the destination has an initial route, which could contain BTE community or not. We verify that for external neighbors (v ∈ ExternalNodes), no route is selected if the initial route of the destination contains a BTE community: ( {s | s = ∞} Y (v) = {s | True}
v ∈ ExternalNodes ∧ BTE ∈ comm(init(d)) otherwise 21