INTRODUCTION

Major cloud providers are seeing sustained financial growth in response to mounting demand for reliable networking [Miller 2022]. This demand suggests a commensurate network infrastructure growth will take place to accommodate more and more users. These networks can already have hundreds of data centers, each with hundreds of thousands of devices running thousands of heterogeneous policies, and receiving thousands of updates a day [Jayaraman et al. 2019b]. Network operators program this infrastructure using distributed routing protocols, where each router in a network may run thousands of lines of configuration code. Despite operators' care, routine configuration updates have inadvertently rendered routers unreachable [Strickx and Hartman 2022] or violated isolation requirements that prevent flooding [Vigliarolo 2022].

To prevent costly errors, operators can use control plane verification to analyze their networks [Abhashkumar et al. 2020;Beckett et al. 2017aBeckett et al. , 2018Beckett et al. , 2019;;Fayaz et al. 2016;Gember-Jacobson et al. 2016;Lopes and Rybalchenko 2019;Prabhu et al. 2020;Weitz et al. 2016;Ye et al. 2020]. Until recently, research has focused on monolithic verification of the entire network at once, which is infeasible for large cloud provider networks. Such networks demand modular techniques that divide the network into components to verify in isolation. This approach has proven successful for software verification [Alur and Henzinger 1999;Flanagan and Qadeer 2003;Giannakopoulou et al. 2018;Grumberg and Long 1994;Henzinger et al. 1998] and network data plane verification [Jayaraman et al. 2019a]. We annotate the interfaces between network components with invariants that describe each component's routing behavior. Given the interfaces of a component's neighbors, we can verify that the component respects its own interface. When the interfaces imply a useful property, e.g., reachability or access control, we can conclude that the monolithic network satisfies that property.

We propose Timepiece, the first modular technique with abstract network interfaces to verify a wide range of properties (including route reachability). Kirigami [Alberdingk Thijm et al. 2022a] proposed an architecture for modular control plane verification, but restricted its interfaces to only exact routes. Lightyear [Tang et al. 2022] presented an alternative verification technique with more expressive interfaces, but can only check that a network never receives a route (e.g., for access control properties) -it cannot check reachability, a keen property of interest.

A temporal model. The basis of Timepiece's approach is a temporal model of network execution, where we reason over the states of nodes at all times. This model came as a surprise to us: one branch of prior work, starting with Minesweeper [Beckett et al. 2017a], sought to avoid the burden of reasoning over all transient states of the network by focusing on the stable states of the routing protocol once routing converges. Unfortunately, a naïve combination of modular reasoning and Minesweeper-style analysis of stable states is unsound. We discovered that the best way to recover soundness, while maintaining the system's generality, is to move to a temporal model. This temporal model appears to ask the verification engine to do a lot more work: the system must verify that all the messages produced at all times are consistent with a user-supplied interface for each network component. Nevertheless, because reasoning is modular, ensuring individual problems are small, the system scales with the size of the largest component rather than the size of the network. This modular reasoning is general and any symbolic method (e.g., symbolic simulation, model checking) could use it to verify individual components. We use a Satisfiability Modulo Theories (SMT)-based method in this work [Barrett and Tinelli 2018]. As a preview of modularity's benefits, Figure 1 shows the time it takes Timepiece to verify connectivity for variable-sized fattree topologies [Al-Fares et al. 2008] with external route announcements using the eBGP routing protocol, compared with a Minesweeper-style network-wide stable paths encoding.

Timepiece does require more work of users than monolithic, non-modular systems: users must supply interfaces that characterize the routes each network component may generate at each time. Still, these interfaces, once constructed, provide the typical benefits of interfaces in any software engineering context. First, they localize exactly where an error occurs: if a component is not consistent with its interface, then one must search only that component for the mistake, and a counterexample from the SMT solver can help pinpoint it. Second, router configurations change rapidly, and these changes are often the source of network-wide problems [Zhang et al. 2022]. Well-defined interfaces will be stable over time. As users update their configurations, they may easily recheck them against the stable, local interface for problems.

Inspired by temporal logic [Pnueli 1984], we developed a simple language to help users specify their interfaces. Through this language, users may state that they expect to see certain sets of routes always, eventually (by some specified time 푡, to be more precise), or until (some approximate specified time). Moreover, the interface language allows users to write abstract specifications that need not characterize irrelevant features of routes, and instead only what is necessary to prove a desired property. For instance, a user might specify a reachability property simply by stating a node must "eventually receive some route at time 푡," without saying which route it must receive. Our formal model is based on a synchronous semantics of time, where nodes receive updates in lockstep. As discussed in prior work [Daggitt et al. 2018], this simplifies reasoning over the routing behavior of networks which converge to unique solutions. One may extend this model to consider a bounded number of steps of delay at the cost of increasing the complexity of our invariants.

To summarize, the key contributions of this paper are:

• We demonstrate in depth why a natural, but naïve modular control plane analysis based on an analysis of stable states is unsound ( §2). • We develop a new theory for modular control plane analysis based on time ( §3). We prove it sound with respect to the semantics of a network simulator, and complete with respect to the closed network semantics (starting from fixed initial values). This theory is general, and can verify individual components using any verification method. • We define an SMT-based verification procedure to reason about all possible routes at all times, which can analyze networks with symbolic representations of, e.g., external announcements or destination routers. ( §4) • We design and implement a new, modular control plane verification tool, Timepiece, based directly on this procedure ( §5). We evaluate Timepiece and check a variety of policies at individual nodes in hundreds of milliseconds. Thanks to its embarrassingly parallel modular procedure, Timepiece scales to networks with thousands of nodes ( §6).

KEY IDEAS

This section introduces the stable routing model of network control planes, which serves as a foundation for many past network verification tools [Beckett et al. 2017a[Beckett et al. , 2018[Beckett et al. , 2019;;Prabhu et al. 2020]. It illustrates in depth why naïvely adopting this model for modular verification is unsound. It then introduces a new temporal model for control plane verification and provides the intuition for why the revised model is superior. This section is long but contains a substantial payoff: the essence of why a sound and general modular control plane analysis should be based off a temporal model of control plane behavior.

Background

To determine how to deliver traffic between two endpoints, routers (also called nodes) run distributed routing protocols such as BGP [Lougheed and Rekhter 1991], OSPF [Moy 1998], RIP [Hedrick 1988], or ISIS [Oran 1990]. Each node participating in a protocol receives messages (also called routes) from its neighboring nodes. After receiving routes from its neighbors, a node will select its "best" route-the route it will use to forward traffic.

Routing policies:

filter : drop all routes tag : tag routes internal allow : drop external routes routes and select the best among those received. For instance, RIP compares hop count; OSPF uses the shortest weighted-length path; and BGP uses a complex, user-configurable combination of metrics. Finally, each router sends its chosen route to its neighbors, possibly modifying the route along the way (for instance, by prepending its identifier to the path represented by the route).

Routing algebras. Routing algebras [Griffin and Sobrinho 2005;Sobrinho 2005] are abstract models that capture the similarities between different distributed routing protocols. Prior work on control plane verification [Beckett et al. 2017a;Giannarakis et al. 2020;Griffin et al. 2002] uses similar abstract models to formalize route computation. We adopt this standard abstract model of routing protocols, which specifies the following components.

• A directed graph 퐺 that defines the network topology's nodes (푉 ) and edges (퐸). We use lowercase letters (푢, 푣, 푤, etc.) for nodes and pairs (푢푣) to indicate directed edges. • A set 푆 of routes that communicate routing information between nodes. Routes abstract the routing announcements and metarouting information used in different routing protocols.

Depending on the problem under consideration, 푆 may be the set of Booleans B or natural numbers N (e.g., checking reachability or path length properties), a set of flags (e.g., checking access control), or a record with multiple fields (more complex policies and/or properties). • An initialization function I that provides an initial route I 푣 ∈ 푆 for each node 푣.

• A function F that maps edges to transfer functions. Each transfer function F (푒) = f 푒 transforms routes as they traverse the edge 푒. • A binary associative and commutative function ⊕ (a.k.a. merge or the selection function)

selects the best route between two options.

An idealized example. Many large cloud providers deploy data center networks to scale up their compute capacity. They connect those data centers to each other and the rest of the Internet via a wide-area network (WAN). To illustrate the challenges of modular network verification, we will explore verification of an idealized cloud provider network with WAN and data center components. Figure 2 presents a highly abstracted view of our network's topology. The data center network contains routers d and e where d connects to the corporate WAN and e connects to data center servers. The WAN consists of routers w and v. Router v connects to the data center as well as to a neighboring network n, which is not controlled by our cloud provider. 1The default routing policy uses shortest-paths. However, in addition, the network administrators want e to be reachable from all cloud-provider-owned devices (i.e., w, v, d), but not to be reachable from outsiders (i.e., n). They intend to enforce this property by tagging all routes originating from their network (푤) as "internal" (e.g., using BGP community tags [CISCO 2005]) and allowing those routes to traverse the de edge. Doing so should allow e to communicate with internal machines but not external machines. Furthermore, to protect nodes from outside interference, the cloud provider applies route filters to external peers to drop erroneous advertised routes that may "hijack" [Feamster and Balakrishnan 2005] internal routing.

Modelling the example. To model our example network, we define the network topology as the graph 퐺 pictured earlier. We assume all routers participate in an idealized variant of eBGP [Lougheed and Rekhter 1991], which is commonly used in both wide-area networks and data centers [Abhashkumar et al. 2021]. We abstract away some of the fields of eBGP routing announcements to define the set of routes 푆 as records with 3 fields: (i) an integer "local preference" that lets users overwrite default preferences, (ii) an integer path length, and (iii) a boolean tag field that is set to true if a route comes from an internal source and false otherwise. 푆 also includes ∞, a message that indicates absence of a route.

Let's consider what happens when starting with a specific route at WAN node w, ⟨100, 0, false⟩ (local preference 100, path length of 0, not tagged internal). The I function assigns w that route, and assigns the ∞ route to all other nodes.

The transfer function f 푒 increments the length field of every route by one across every edge 푒. In addition, edge wv sets the internal tag field to true and edge nv drops all routes (transforms them into ∞). Finally, edge de drops all routes not tagged internal/true.

The merge function ⊕ always prefers some route over the ∞ route, and prefers routes with higher local preference over lower local preference. If the local preference is the same, it chooses a route with a shorter path length. ⊕ ignores the tag field. For example, ⊕ operates as follows: ⟨100, 2, false⟩ ⊕ ∞ = ⟨100, 2, false⟩ ⟨100, 2, false⟩ ⊕ ⟨200, 5, true⟩ = ⟨200, 5, true⟩ ⟨200, 2, false⟩ ⊕ ⟨200, 5, true⟩ = ⟨200, 2, false⟩ Network simulation. A state of a network is a mapping from nodes to the "best routes" they have computed so far. One may simulate a network by starting in its initial state and repeatedly computing new states (i.e., new "best routes" for particular nodes). Well-behaved networks eventually converge to stable states where no node can compute a better route, given the routes provided by its neighbors.

To compute a new best route at a particular node, say v, we apply the f function to each best route computed so far at its neighbors w, n, and d, and then select the best route among the results and the initial value at v, using the merge (⊕) function. More precisely:

The table in Figure 3 presents an example simulation. At each time step, all nodes compute their best route given the routes sent by their neighbors at the previous time step. Our model assumes a synchronous time semantics for simplicity: this simulation is hence one possible asynchronous execution.foot_3 After time step 3, no node computes a better route-the system has reached a stable state. The picture in Figure 3 annotates each node in the diagram with the stable route it computes.

Network verification. Since the edge from d to e only allows routes tagged internal, 푤's route would not reach e if v were to receive a better route from n (e.g., if the route filter from 푛 was implemented incorrectly). In other words, the simulation demonstrates that the network correctly operates when n sends no route (∞). But what about other routes? Will 푓 푛푣 filter all routes from n correctly? SMT-based tools like Minesweeper [Beckett et al. 2017a] and Bagpipe [Weitz et al. 2016] can answer such questions by translating the routing problem into constraints for a Satisfiability Modulo Theory (SMT) solver to solve. An SMT-based encoding of our network could represent filter tag allow

∞ ⟨100, 0, false⟩ ⟨100, 1, true⟩ ⟨100, 2, true⟩ ⟨100, 3, true⟩ any possible external route announcement from n by representing its initial value with a symbolic variable: the solver can then search for a concrete route captured by this variable that violates our desired property, i.e., a stable state where e never receives a route from w.

The Challenge of Modular Verification

A system for modular verification will partition a network into components and verify each component separately, possibly in parallel. However, since routes computed at a node in one component depend on the routes sent by nodes in neighboring components, each component must make some assumptions about the routes produced by its neighbors.

Interfaces. In our case, for simplicity (though this is not necessary), we place every node in its own component and define for it an interface that attempts to overapproximate (or equal) the set of routes that the node might produce in a stable state. The interface for the network as a whole is a function 퐴 from nodes to sets of routes where 퐴(푥) is the interface for node 푥.

The person attempting to verify the network will supply these interfaces. Of course, interfaces may be wrong-that is, they might not include some route computed by a simulation (and hence might not be a proper overapproximation). Indeed, when there are bugs in the network, the interfaces a user supplies are likely to be wrong! The user expects the network to behave one way, producing a certain set of routes, but the network behaves differently due to an error in its configuration. A sound modular verification procedure must detect such errors and indicate if we must strengthen the interface to prove the property. On the other hand, a useful modular verification procedure should allow interfaces to overapproximate the routes produced, when users find it convenient. Overapproximations are sound for verifying properties over all routing behaviors of a network, and they often simplify reasoning, allowing users to think more abstractly.

Throughout the paper, we use predicates 휑 to define interfaces, where 휑 stands in for the set of routes {푠 | 푠 ∈ 푆, 휑 (푠)}. Returning to our running example, one might define the interface for w using the predicate 푠.lp = 100 ∧ 푠.len = 0 ∧ ¬푠.tag. Such an interface would include exactly the one route generated by w in our example: ⟨100, 0, false⟩. However, path length is unimportant in the current context; to avoid thinking about it, a user could instead provide a weaker interface representing infinitely many possible routes, such as 푠.lp = 100 ∧ ¬푠.tag. This interface relieves the user of having to figure out the exact path length (not so hard in this simple example, but potentially challenging in an arbitrary wide-area network), and instead specifies only the local preference and the tag. In general, admitting overapproximations make it possible for users to ignore any features of routing that are not actually relevant for analyzing the properties of interest.

The strawperson verification procedure. For a given node x, the component centered at x is the subgraph of the network that includes node x and all edges that end at x. Given a network interface 퐴, our strawperson verification procedure (SV ) will consider the component centered at each node x independently. Suppose a node x has neighbors 푛 1 , . . . , 푛 푘 . For that node x, SV checks that

This check is akin to performing one local step of simulation, checking that all possible inputs from neighbors produce an output route satisfying the interface. We might hope that by performing such a check on all components independently, we could guarantee that all nodes converge to stable states satisfying their interfaces. If that were the case, then we could verify properties by:

(1) Checking that all components guarantee their interfaces, under the assumption their neighbors do as well; and (2) Checking that the interfaces imply the network property of interest (e.g., reachability, access control, no transit).

The problem: execution interference. It turns out this simple and natural verification procedure is unsound: users can supply interfaces that, when analyzed in isolation, satisfy equation (1) above, but exclude stable states computed by simulation. Hence, the second verification step is pointless: a destination that appears reachable according to an interface may not be; conversely, a route that appears blocked may not be.

Let us reconsider the running example, where we assign w an initial route with local preference 100, and assume the external neighbor 푛 can send us any route (true). A user could provide the interfaces shown in Figure 4 to falsely conclude that 푒 will not receive a route from 푤. Here, it is easy to check that nodes n and w satisfy equation (1). Node n's interface is simply any route. Node w's route can be any route with a local preference of 100. 3The surprise comes at node v where its interface only includes routes that satisfy ¬푠.tag, i.e., routes not tagged as internal. Those routes have 푠.lp = 200 and may have any path length. But the route from w is tagged true along the edge 푤푣 -why is such a route erroneously excluded from v's interface? We show the component centered at v in Figure 5. When computing its stable state, v will compare the routes it receives from w and d: because all routes from w have a local preference set to 100 by f 푤푣 , whereas all routes from d have a better local preference of 200, v will always wind up selecting the route from d over the route from w.

But how then did d acquire these preferential routes tagged false? Such routes came in turn from v's interface. Figure 6 shows the component centered at d. What has happened is that v transmits its spurious routes to d, enabling d to justify its own spurious routes. d transmits these back again to v, where d's routes interact with the legitimate routes from w. Since w's routes have lower local preference, v discards them during computation of stable states. In a nutshell, our interface proposed routes that do not soundly overapproximate the legitimate routes from the true simulation, but our verification procedure accepted this bad interface as it circularly justified itself at v and d. How might we prevent this execution interference? Other approaches. We can modify this verification procedure to make it sound, but these solutions will limit the verification procedure's power or the expressiveness of the properties it can prove.

One approach is to limit every interface to exactly one route. Doing so avoids introducing any imaginary executions in the first place. Kirigami [Alberdingk Thijm et al. 2022a] takes this approach, but the cost is that a user analyzing their network must know exactly which routes appear at which locations. Computing routes exactly can be difficult in practice, and would seem unnecessary if all one cares about is a high-level property such as reachability. Moreover, it makes the interfaces brittle in the face of change-any change in network configuration likely necessitates a change in interface. A superior system would allow operators to define durable and abstract interfaces that imply key properties, and to check configuration updates against those interfaces.

Another approach is to limit the set of properties that the system can check to only those that say what does not happen in the network rather than what does happen. This is the approach Lightyear [Tang et al. 2022] takes. For instance, Lightyear can check that node a will not be able to reach node b, but not that a and b will have connectivity -a common requirement in networks.

A final approach is to statically order the components, and verify each component according to this ordering, using no information from the not-yet-verified components. By ordering v before d, we would need to satisfy v's invariant without routes from d (treating d's invariant as false)this would fail for the bad invariant 푠.lp = 200 ∧ ¬푠.tag using only routes from n and w. In practice, this is still unnecessarily conservative. The running example is overly simple as it shows routes propagated through a network in a single direction from left to right. In realistic networks, multiple destinations may broadcast routes in multiple directions at once. In such situations, there may be no way to order the components, and verification may not be possible.

The Solution: A Temporal Model

Our key insight is to change the model: rather than focus exclusively on the final stable states of a system, as a Minesweeper-style verifier would, we ensure that the model preserves the entirety of every step-by-step execution. To make this work, we need to add information to the model: a notion of logical time. By associating every route with the time at which a node computes it, we can (i) ensure that all routes at a particular time are properly considered, and their executions extended a time step, and (ii) ensure that we avoid collisions between routes computed at different times.

To verify such routing systems modularly, we once again must specify interfaces, but this time the interface for each node will specify the set of routes that may appear at any time. We write this now as an interface 퐴(푥)(푡) that takes both a node 푥 and a time 푡 and returns an overapproximation of the set of routes that may appear at 푥 at that time 푡. To check the interfaces, we use a verification procedure structured inductively with respect to time, as follows:

Because this procedure is structured inductively, we can prove, by induction on time, that all states at all times are included in their respective interfaces-the procedure is sound.

For brevity, we specify our interfaces using temporal operators. These operators are functions that take a time 푡 as an argument, compare it to an explicit time variable 휏, and return a predicate. We write G(푃) ("globally 푃") when a node's interface includes the routes that satisfy predicate 푃 for all times 푡. We write 푃 1 U 휏 푄 2 ("푃 1 until 푄 2 ") when a node may have routes satisfying 푃 1 until time 휏-1 and operator 푄 2 (휏) holds afterwards. Finally, we write F 휏 (푄) ("finally 푄") to mean that eventually at time 휏 routes start satisfying 푄 (휏).

Verifying correct interfaces. Figure 7 below presents an interface we may verify with this model.

Fig. 7. Running example with interfaces proving that if e has a route, it is tagged.

We again assume that n sends any route at any time, denoted by the interface: G(true). We assume w has a route with default local preference: G(푠.lp = 100). The interesting part is at nodes v and d where the interfaces state that there is always no route (e.g., at time 0), or a tagged route: G(푠 = ∞ ∨ 푠.tag). We can then prove a weak property about node e: if it receives a route, then the route will be tagged internal. We can prove node v's route satisfies its interface since f 푤푣 tags routes on import from node w, routes from n are correctly dropped, and routes from d must also have a tag per its interface. In fact, all the nodes satisfy their interface given their neighbors' interfaces.

Proving reachability. Figure 7's interfaces were too weak to prove that w can reach e. The problem is that they reason about all times (i.e., from time 0 onward), yet e will only eventually have a route from w at some time in the future. Consider now the stronger interfaces shown in Figure 8:

Fig. 8. Running example with interfaces proving e can reach w.

As before, we allow n and w to send any route. However, now nodes v and d declare that they will not have a route until a specified (logical) time, at which point they receive a tagged route. We give precise witness times for v and d's interfaces, as otherwise v could give d a non-null route (or vice-versa) that would violate the interface before its witness time. e's interface simply requires that e receives some route at the witness time (allowing arbitrary routes before the witness time). These interfaces are sufficient to prove that e will eventually receive a route to w, since d will eventually have a route tagged as internal, and hence e will allow it.

Debugging erroneous interfaces. Let us revisit the example where a user gave unsound interfaces using spurious routes with local preference 200. Figure 9 presents the equivalent temporal interfaces. Unlike before, the verification procedure detects an error: the interfaces at nodes v and d do not include the initial route ∞ at time 0. As a result, the user will receive a counterexample for time 푡 = 0 when verifying v or d. Suppose our imaginative user tries to circumvent this issue by also including the initial route in the interfaces for v and d with the interface:

However, doing so merely pushes the problem "one step forward in time"-there is no way to circumvent our temporal analysis. If d's route may be ∞, v's interface must also consider what routes it selects when that is the case, including tagged routes such as ⟨100, 1, true⟩. The user might receive a counterexample at time 푡 = 1 where v's route is the following:

where 퐴(푣)(1) does not contain the result ⟨100, 1, true⟩. This counterexample reveals the fact that there is an error in either the specification (as in this case) or the configuration (e.g., if a buggy configuration tagged routes from w false rather than true as expected).

Property

Added ghost state reachability to 푑 [Fogel et al. 2015] 1 bit to mark routes from 푑 isolation [Beckett et al. 2017a] 1 bit per isolation domain ordered waypoint [Kazemian et al. 2013]. 푙표푔 2 (푘) bits for 푘 waypoints unordered waypoint [Beckett et al. 2017a] 푘 bits for 푘 waypoints routing loops [Beckett et al. 2017a] up to |푉 | bits to track visited nodes no-transit [Beckett et al. 2016] mark with {peer, prov, cust} fault tolerance [Beckett et al. 2017a] up to |퐸| bits to track failed edges bounded path length [Lopes et al. 2015] integer length field

Properties and ghost state. Although our modular properties reference node-local routes, we can verify many end-to-end control plane properties using ghost state. Users may model routes with additional "ghost" fields (cf. ghost fields in Dafny [Leino 2010]) that play no role in a protocol's routing behavior, yet may capture end-to-end properties. For instance, suppose we added a boolean "ghost" field "fromw" to indicate if a route originated from node w (see Figure 10). We assume this field is initially true at w, false at all other nodes, and that transfer functions preserve its value. With this addition, we can now check that e receives a route from w and no other node.

Fig. 10. Running example augmented with a "fromw" ghost variable.

Ghost state allows us to specify and check many network properties; Table 1 presents a variety of other possibilities. For example, to check for routing loops, we can use a multi-set of visited nodes (up to |푉 |) and mark if a node is ever visited more than once. That said, while ghost state is general and flexible, it can only capture information about the history of a route at a single node and is thus not a panacea. For instance, properties involving the routes at more than one node, such as a formulation of local equivalence [Beckett et al. 2017a], where 휎 (푢)(푡) = 휎 (푣)(푡) for some arbitrary 푢, 푣 and 푡, is inexpressible using our verifier. We focus on properties of the network's control plane, without considering the data plane forwarding behavior. This rules out data plane properties such as load balancing and multipath consistency.

FORMAL MODEL WITH TEMPORAL INVARIANTS

Figure 11 presents the key definitions and notation needed to formalize our verification procedure. The notation follows from the previous section, e.g., a network instance 푁 = (퐺, 푆, I, F, ⊕) contains the key components introduced earlier. To refer to the route computed by a network simulator at node 푣 at time 푡, we use the notation 휎 (푣)(푡) (defined as before-see Figure 11).

Figure 12 presents our interfaces and language of temporal operators. As before, we use 퐴 to denote network interfaces. The temporal operators 푄 are syntactic sugar for functions from a time 푡 to a predicate. 휑 U 휏 푄 and F 휏 (푄) take a concrete natural number 휏 as a witness time parameter to compare against the argument time 푡. These witness times are absolute times, specifying the time steps since the initial time 0. We can nest U 휏 and F 휏 operators to represent arbitrarily-many intervals of time, e.g., F 2 (휑 1 U 4 G(휑 2 )) is a function that returns 푆 (true) given input time 0 or 1; 휑 1 given time 2 or 3; and 휑 2 given a time of 4 or more. We also lift set union, intersection and negation to succinctly combine temporal operators. In our evaluation ( §6), we found this (intentionally small) language sufficient to express a wide variety of reachability and security properties. A valid interface is an inductive invariant [Giannakopoulou et al. 2018]. Such interfaces satisfy the initial and inductive conditions specified in Figure 12. Valid interfaces may be used to prove node properties, as specified by the safety condition in Figure 12. As the network has a finite number of nodes, we can enumerate them to check these three conditions on every node in the network.

The most important property of our system is soundness: the simulation states are included in any interface 퐴 that satisfies the initial and inductive conditions. Theorem 3.1 (Soundness). Let 퐴 satisfy the initial and inductive conditions for all nodes. Then 퐴 always includes the simulation state 휎, meaning ∀푣 ∈ 푉 , ∀푡 ∈ N, 휎 (푣)(푡) ∈ 퐴(푣)(푡).

Proof. By induction on 푡. See [Alberdingk Thijm et al. 2022b] for the full proof. □

Since initial and inductive conditions suffice to prove that simulation states are included within interfaces, it is safe in turn to use interfaces to check node properties.

Corollary 3.2 (Safety). Let 퐴 satisfy the initial and inductive conditions for all nodes. Let 푃 satisfy the safety condition with respect to 퐴 for all nodes. Then ∀푣 ∈ 푉 , ∀푡 ∈ N, 휎 (푣)(푡) ∈ 푃 (푣)(푡).

Proof. From definitions. See [Alberdingk Thijm et al. 2022b]. □

A closed network is a network instance where all initial routes are fixed routes, such that all states of the network 휎 are captured by a concrete simulation. Our verification procedure is complete with Interfaces, Properties and Metavariables

Verification Conditions Initial condition for node 푣:

Safety condition for node 푣: respect to a closed network: for any closed network, there exists an interface that characterizes its simulation states exactly. One of the consequences of completeness is that our modular verification procedure is powerful enough to prove any property that we could prove via a concrete simulation.foot_5

Theorem 3.3 (Closed Simulation Completeness). Let 휎 be the state of the closed network. Then for all 푣 ∈ 푉 and 푡 ∈ N, 퐴(푣)(푡) = {휎 (푣)(푡)} satisfies the initial and inductive conditions for all nodes.

Proof. By construction of the interface. See [Alberdingk Thijm et al. 2022b]. □

SMT ALGORITHMS FOR VERIFICATION

We can check our initial, inductive and safety verification conditions (VCs) independently for every node in the network using off-the-shelf SMT solvers. To check an instance of a VC, the solver will attempt to prove the condition is valid (i.e., true for all choices of 푡 and 푠 1 , 푠 2 , . . . , 푠 푛 ) by checking whether the negation of our original VC is satisfiable. If the solver can satisfy the negation, it will provide us with a counterexample-the state(s) of the node(s) at a particular time such that the VC does not hold. Counterexamples to initial or inductive conditions indicate that the interface does not capture the network's behavior, while a counterexample to the safety condition indicates that the interface is not strong enough to prove the property. The latter case may occur because the property is simply not true (indicating a bug), or because we must strengthen the given interface to prove the property. If the negation is unsatisfiable, then we know the condition is valid.

Algorithm 1 The modular checking algorithm.

proc CheckMod(network (퐺, 푆, I, F, ⊕), interface 퐴, property 푃) for all 푣 ∈ 푉 do in parallel

A network instance's routes and behavior determines its encoding in SMT. For example, one could encode the route triples in §2 as integer variables lp and len and a Boolean variable tag, and use Presburger arithmetic to encode F and ⊕ with + and <. To model networks with external peers (like n), multiple routing destinations, or other sources of nondeterminism, we may use symbolic variables. For external peers, rather than treating n as having a specific initial route such as ∞, we may use a symbolic variable 푠 for I 푛 , and then ask the SMT solver to check the VCs for all choices of 푠. For multiple destinations, we can use a symbolic node variable to choose from a set of destination nodes when checking that any node in that set is reachable. We also can assume arbitrary preconditions for symbolic variables, e.g., enforcing that 푠 is not tagged with ¬푠.tag. These assumptions are not checked when we encode them to SMT.

The modular checking procedure. We present our modular checking procedure in Algorithm 1. The CheckMod procedure iterates over each node of the network and encodes the underlying formula (for the current node) of our three verification conditions by calling EncodeInitCond, EncodeIndCond and EncodeSafeCond as defined in ( 5), ( 6) and (7), respectively.foot_6 Note that we encode 푡 as an explicit symbolic variable: our temporal operators expand to a case analysis over this variable to determine what predicate holds on the particular node's route. We then ask the solver if every encoded formula is valid using IsValid. If IsValid returns false for any check, we ask for the relevant counterexample using GetCounterExample, which returns a variable assignment that violates the formula. Otherwise, we report success (퐴 and 푃 hold).

Encoding the initial and inductive conditions is roughly proportional in size to the complexity of the policy at the given node, which in turn is related to the in-degree of the node-denser networks that include nodes with higher in-degree are more expensive to check. Encoding the safety condition is proportional to the size of the formulae describing the interface and property (generally tiny). In addition to reducing the size of each SMT formula, the factoring of the problem into independent conditions makes it possible to check conditions on nodes simultaneously in parallel. We will discuss the performance implications of our procedure further in §6.

Handling counterexamples. When GetCounterExample returns a counterexample for a modular check, it specifies (a) routes of the node(s); (b) a concrete time; and (c) concrete values of any symbolic variables in the formula. These counterexamples can guide us in strengthening the invariants or pinpointing bugs. This is akin to other invariant-checking tools like Dafny [Leino 2010] where users must manually refine their invariants. Anecdotally, our practical approach to designing the interfaces in §6 was to start by choosing 퐴(푣)(푡) = 푃 (푣)(푡) (trivially satisfying our safety condition). A counterexample would then identify a time instance where 푣's invariant violated its initial or inductive condition. To resolve this violation, we often had to add a G(휑) invariant to capture additional behavior (e.g., no node receives a better route than the legitimate route). This "rule-of-thumb" suggests that counterexample-guided techniques [Clarke et al. 2000] may be capable of inferring invariants. We leave this as future work.

Incorporating delay. 휎 and 퐴 define a synchronous network semantics. As shown in prior work on routing algebras [Daggitt et al. 2018;Griffin and Sobrinho 2005], when F and ⊕ are strictly monotonic -informally, ⊕ prefers a route 푟 over any transferred route f 푒 (푟 ) -there will only be one converged state of the network, which our synchronous model will certainly capture. 6 In other cases, the synchronous model captures a possible execution of the network.

We may extend our model to consider routes up to a bounded number of units of delay. To account for one unit of delay, we can extend our inductive condition to check all routes sent in the last two time steps 푡 and 푡 + 1 satisfy the invariant at time 푡 + 2, becoming (changes in boxes):

We may extend the condition further to consider more units of delay. Doing so may also increase the complexity of our invariants.

IMPLEMENTATION

We implemented Timepiece's modular verification procedure as a library written in C#. The library allows users to construct models of networks and then modularly verify them. Like the network modelling framework NV [Giannarakis et al. 2020], Timepiece allows users to customize their models by providing the type of routes (which may involve integers, strings, booleans, bitvectors, records, optional data, lists, or sets) and the initialization, transfer and merge functions that process them. This modelling language makes it easy to add ghost state to routes, as described earlier. It is also possible to declare and use symbolic values in the model. Hence, one may reason about all possible prefixes or more generally about all possible external routing announcements.

Under the hood, Timepiece uses Microsoft's Zen verification library [Beckett and Mahajan 2020] to generate SMT formulas from higher-level C# data structures and pass these formulas to the Z3 SMT solver [De Moura and Bjørner 2008]. Timepiece thus supports any network model that Zen can encode to Z3. For example, to model a network running eBGP, we would adopt many of the modelling choices made in Minesweeper [Beckett et al. 2017a]. We can use integers and Presburger arithmetic to model path length, and bitvectors to model local preference and MED.

Timepiece uses multi-threading to run modular checks in parallel. 7 As each check is independent, the time to set up additional threads is the only overhead for parallelization.

EVALUATION

To evaluate Timepiece and illustrate its scaling trends, we generated a series of synthetic fattree [Al-Fares et al. 2008] data center networks and verified four variations on reachability properties. We also verified an isolation property on a real wide-area network configuration with over 100,000 lines of Junos configuration code. These two types of networks demonstrate Timepiece's performance for networks which are highly-connected (data centers) and have complex policies (WANs). Table 2 shows that writing the interfaces for each of our benchmarks is low-effort compared to the rest of the network in terms of lines of code. We generated interfaces for our experiments parametrically for any size of network, based on the distinct roles of nodes: for fattree networks, a node's pod and tier determined its role (5 roles, discussed later); for our wide-area network benchmark, we distinguished internal nodes from external neighbors (2 roles). As a node's role determined its invariant, it is easy to extend or update these networks (e.g., adding a new pod or external neighbor) and reuse the appropriate existing invariant for a node of that role.

To compare our implementation against a baseline, we implemented a monolithic, network-wide Minesweeper-style [Beckett et al. 2017a] procedure Ms and compared its performance against Timepiece. Ms analyzes stable states, which are independent of time. Given a property 푃 over stable states, Ms checks if 푃 always holds (is valid) given the stable states of the network. These states are encoded as a single formula over all nodes, as described in §2.1. To compare Ms with Timepiece, we first crafted properties for Timepiece, which employs timed invariants. We then erased the temporal details from these invariants to generate properties that Ms could manage. For instance, when Timepiece would verify properties of the form G(휑), F 푡 G(휑), or 휑 2 U 푡 G(휑), Ms would instead verify that the network's stable states satisfy 휑. 8We ran our benchmarks on a Microsoft Azure D96s v5 virtual machine with 96 vCPUs and 384GB of RAM. We used the machine's multi-core processor to run all modular checks in parallel, while monolithic checks necessarily ran on a single thread. We timed out any benchmark that did not complete in 2 hours. We report four times for each benchmark: (i) the total time until all Timepiece threads finished (Tp); (ii) the median node check time; (iii) the 99 th percentile node check time (99% of checks completed in less than this much time); and (iv) the total time taken by Ms.

Fattrees. We parameterize our fattree networks by the number of pods 푘: a 푘-fattree has 1.25푘 2 nodes and 푘 3 edges: Figure 13 shows an example 4-fattree used in our Vf benchmark. We considered multiples of 4 for 4 ≤ 푘 ≤ 40 to assess Timepiece's scalability: whereas we expected a monolithic verifier to time out on larger topologies, we hypothesized that Timepiece would scale to these networks. We present how verification time grows with respect to the number of nodes in each fattree in Figure 14. The figure shows verification time on the y-axis on a logarithmic scale.

We considered four different properties (explained below): reachability (Reach), bounded path length (Len), valley freedom (Vf) and route filtering (Hijack). We considered each property when routing to a single, fixed destination edge node dest (Sp), and routing to a dest edge node determined by a symbolic variable (Ap) -modelling all-pairs routing to any edge node. Our routes modelled the eBGP protocol in these networks. Table 3 summarizes the eBGP fields represented and how we modelled them in SMT. We model the major common elements of eBGP routing: a route destination as a 32-bit integer (representing an IPv4 prefix); administrative distance, local preference, multi-exit discriminators as 32-bit integers (encoded as bitvectors); eBGP origin type as a ternary value; the AS path length as an (unbounded) integer; and BGP communities as a set of strings.

Witness times. Our temporal operators include witness times to specify the time when a node 푣 has a route. To prove that 푣 eventually has a route to the destination node dest at time 푡, we must show that one of 푣's neighbors sent it such a route at an earlier time 푡 -1. The exact time 푣 obtains a route thus depends on where dest is relative to 푣. This breaks down to five cases (or roles), following the fattree's structure, depending on whether 푣 is: (i) the 푑푒푠푡 node (0 hops, has a route at 푡 = 0); (ii) an aggregation node in dest's pod (1 hop, has a route at 푡 = 1); (iii) a core node, or an edge node in dest's pod (2 hops, 푡 = 2); (iv) an aggregation node in another pod (푡 = 3); or (v) an edge node in another pod (푡 = 4). The largest choice of 푡 is hence 4, the diameter of the fattree. These cases mirror those identified for local data center invariants in [Jayaraman et al. 2019a]. We use a function dist (푣) to encode these cases for each node 푣.

Reach. Reach demonstrates the simplest possible routing behavior and serves as a useful baseline. The policy simply increments the path length of a route on transfer. We initialized one destination edge node with a route to itself, and all other nodes with no route (∞). Our goal is to prove every node eventually has a route to the destination (i.e., its route is not ∞). More precisely, because our network has diameter 4, each node 푣 should acquire a route in 4 time steps.

Interfaces for these benchmarks mirror the simplicity of the policy and property. If a node's route 푠 ≠ ∞ at time 푡, then its neighbors will in turn have a route 푠 ≠ ∞ at time 푡 + 1.

SpReach's policy and property are so simple that Tp is actually slightly slower than Ms, as shown in Figure 14a. We conjecture the Ms encoding reduces to a particularly easy SAT instance. That said, we can already see that individual checks in Timepiece take only a fraction of the time that Ms takes, with 99% of node checks completing in at most 1.1 seconds, even for our largest benchmarks. For ApReach, Figure 14e shows that, perhaps from the burden of modelling the symbolic dest, Ms times out at 푘 = 8. Tp verifies our largest benchmark (푘 = 40, with 2,000 nodes) in 5.5 minutes, with 99% of individual node checks taking under 9 seconds.

Len. Our next benchmark uses the same policy as Reach, but considers a stronger property: every node eventually has a route of at most 4 hops to the destination.

To prove this property, our interfaces specify that path lengths in routes should not exceed the distance to the destination: 푠.len ≤ dist (푣). In addition, because local preference influences routing, we fix the local preference to the default for all routes when present: 푠.lp = 100.

eventually the route appears Reasoning over path lengths requires Z3 to use slower bitvector and integer theories. Figure 14b shows that monolithic verification times out at 푘 = 12 for SpLen. By contrast, modular verification is able to solve 푘 = 40 in just over 20 minutes, with 99% of nodes verified in under 43 seconds. Figure 14f shows that monolithic verification is not even possible for ApLen at 푘 = 4; Tp completes for ApLen 푘 = 40 in around 66 minutes, with 99% of nodes verified in 2.4 minutes.

Vf. Vf extends Reach with policy to prevent up-down-up (valley) routing [Beckett et al. 2016[Beckett et al. , 2017b;;Pepelnjak 2018], where routes transit an intermediate pod. To implement this policy, we add a BGP community 퐷 along "down" edges in the topology (i.e., from a core node or from an aggregation node to an edge node), and drop routes with 퐷 on "up" edges (see Figure 13). For brevity, we write "푠.down" to mean "퐷 ∈ 푠.tags". We test the same reachability property as Reach.

The legitimate routes in the fattree all start as routes travelling up from the destination node's pod, e.g., the nodes in green (푎 16 , 푎 17 , 푒 19 ) in Figure 13. We refer to these nodes as "adjacent nodes" with a shorthand adj(푣): they transmit routes to the core nodes (and thereby to the rest of the network) along their up edges. These edges will drop the routes if 푠.down, so we require that adj(푣) → ¬푠.down. To ensure this, we add conjuncts to our interfaces requiring that nodes' final routes are no better than the shortest path's route: 푠.lp = 100 ∧ 푠.len = dist (푣). This ensures our inductive condition holds after every node has a route: otherwise, a core node (for instance) could offer a spurious route with 푠.len < 1 ∧ 푠.down to an adjacent node.

no better routes appear ∧ adj(푣) → ¬푠.down adjacent nodes will share routes Figure 14c shows that Ms verifies up to 푘 = 8 before timing out. As with SpLen, Tp time grows gradually in proportion to the number of nodes, topping out at 6.6 minutes for 푘 = 40, with all node checks completing in under 20 seconds. Figure 14g shows that for all-pairs routing, monolithic verification times out again at 푘 = 12, whereas Tp hits the 2-hour timeout at 푘 = 36. We conjecture this may be due to the added complexity of encoding adj(푣) when the destination is symbolic.

Hijack. Hijack models a fattree with an additional "hijacker" node ℎ connected to the core nodes. ℎ represents a connection to the Internet from outside the network, which may advertise any route. We add a boolean ghost state tag to 푆 for this policy to mark routes as external (from ℎ) or internal. The destination node will advertise a route with 푠.prefix = 푝, where 푝 is a symbolic value representing an internal address: the core nodes will then drop any routes from ℎ for prefix 푝, but allow other routes through. Apart from this filtering, routing functions as in the Reach benchmarks. For this network, we verified that every internal node eventually has a route for prefix 푝 and which is not via the hijacker (¬푠.tag), assuming nothing about the hijacker's route (퐴 Hijack (ℎ) ≡ G(true)).

The Hijack interface is straightforward. We must simply re-affirm that nodes with internal prefixes never have external routes: 푠.prefix = 푝 → ¬푠.tag. Once nodes have received a route from the destination at time dist (푣), they should keep that route forever, and hence their route will have both 푠.prefix = 푝 and ¬푠.tag.

퐴 Hijack (푣) ≡ F dist (푣) G(푠.prefix=푝 ∧ ¬푠.tag) route will be internally reachable ⊓ G(푠.prefix=푝 → ¬푠.tag) no hijack route is ever used

In SpHijack, monolithic verification times out at 푘 = 8, whereas modular verification time scales to 푘 = 40. 99% of nodes complete their checks in under 3 seconds, with our longest check taking 10.7 seconds at 푘 = 40. As with our other benchmarks, verification time grows linearly with respect to the in-degree of each node (which determines the size of the SMT encoding of our inductive condition). Figure 14h shows similar patterns for the all-pairs case, with no monolithic benchmark completing on time, and modular verification taking at most 36.6 minutes.

Wide-area networks. To better investigate Timepiece's scalability for other types of networks, we evaluated it on the Internet2 [Internet2 2013] wide-area network.foot_10 Internet2's configuration files are one of the few publicly available examples of the complex policies of wide-area and cloud provider networks, as described in Propane [Beckett et al. 2016]. These files contain 1,552 Junos routing policies, which filter routes by tag or prefix and tag routes according to customer priorities (e.g., commercial vs. academic peers). We converted the configuration files to Timepiece's model by extracting the policy details using Batfish [Fogel et al. 2015]. The resulting network has over 200 nodes: 10 internal nodes within Internet2's AS and 253 external peers. We did not model all components of Internet2's routing policies: we focused on IPv4 and BGP routing, and treated some complex behaviors as "havoc" (soundly overapproximating the true behavior). 10 We do not know Internet2's intended routing behavior: because of this, we cannot be certain that a counterexample found by Timepiece represents a real violation of the network's behavior; nonetheless, we may still use this network to assess how well Timepiece enables modular verification.

It appears that Internet2 uses a BTE community tag to identify routes that must not be shared with external neighbors. We checked that, if the internal nodes initially have any possible route, then no external neighbor of Internet2 should ever obtain a route with the BTE tag set, assuming the external neighbors do not start with such routes.

Our interface is the property, i.e., ∀푣. 퐴 BlockToExternal (푣) ≡ 푃 BlockToExternal (푣). Modular checking remains fast despite the network's more complex policies: on a 6-core Macbook Pro with 16GB of RAM, modular verification completes in 38.3 seconds, with a median check time of 0.6 seconds and a 99 th percentile check time of 4.2 seconds. Monolithic verification does not complete after 2 hours.

RELATED WORK

Our work is most closely related to other efforts in control plane verification [Abhashkumar et al. 2020;Alberdingk Thijm et al. 2022a;Beckett et al. 2017aBeckett et al. , 2018Beckett et al. , 2019;;Fogel et al. 2015;Gember-Jacobson et al. 2016;Giannarakis et al. 2020;Lopes and Rybalchenko 2019;Prabhu et al. 2020;Tang et al. 2022;Weitz et al. 2016;Ye et al. 2020]. We separate these tools into classes based on the specifics of one's verification problem.

SMT-based verification. For networks which are small (in the tens of nodes), SMT-based tools such as Minesweeper [Beckett et al. 2017a] or Bagpipe [Weitz et al. 2016] offer ease-of-use, generality, and symbolic reasoning. Minesweeper supports a broad range of properties including reachability, waypointing, no blackholes and loops, and device equivalence.

Simulation-based verification. For larger networks that do not necessitate incremental recomputation after device update nor fully symbolic reasoning, one can use simulation-based tools [Beckett et al. 2019;Fogel et al. 2015;Giannarakis et al. 2020;Lopes and Rybalchenko 2019;Prabhu et al. 2020;Ye et al. 2020]. Some of these tools also employ symbolic reasoning in limited ways to provide useful capabilities. For example, inspired by effective work on data plane analysis [Khurshid et al. 2013], Plankton [Prabhu et al. 2020] first analyzes configurations to identify IP prefix equivalence classes. Identified equivalence classes may be treated symbolically in the rest of the computation. Plankton might be able to reason symbolically about other attributes, but doing so would require additional custom engineering to find the appropriate sort of equivalence class ahead of time (e.g., for BGP AS paths or communities). Timepiece can represent any or all route fields symbolically (e.g., for external actors), or determine the behavior of I, F and ⊕ functions using symbolic variables (e.g., for all-pairs properties). The solver effort is then passed off to the underlying SMT engine.

Scalable SMT-based verification. Fewer tools exist for networks which are large and where symbolic reasoning is important. Bonsai exploits symmetry to derive smaller abstractions of a network [Beckett et al. 2018], but does not work if the network has topology or policy asymmetries or one considers failures (which break topological symmetries). Other tools exploit modularity in network designs. Kirigami [Alberdingk Thijm et al. 2022a] verifies networks using assumeguarantee reasoning, but requires interfaces to specify the exact routes passed between any two components. As such, it is impossible to craft interfaces that are robust to minor changes in network policies. Lightyear [Tang et al. 2022] allows users to craft more general interfaces, but can only prove properties that capture the absence of some "bad" route (e.g., our BlockToExternal property). Lightyear does not model route interaction (e.g., selecting routes by path length), which we do via our ⊕ function: Lightyear's verification queries are therefore smaller, as it can check invariants on every edge independently. We conjecture (but have not proven) that Lightyear verifies properties that Timepiece expresses as G(휑), but not properties requiring U 푡 or F 푡 temporal operators.

Other efforts in network analysis. Daggitt et al. also use a timed model [Daggitt et al. 2018], but focus on convergence properties of routing protocols. We analyze properties that depend upon a network's topology and configuration such as reachability.

Other inspirations for our work are SecGuru and RCDC [Jayaraman et al. 2019a] in data plane verification. Unlike our work, they use non-temporal invariants, which they extract from the network topology and assume as ground truth for policies on individual devices. Whereas our experiments likewise used the topology to define local invariants, our verification procedure checks that these invariants are in fact guaranteed by the other devices in the network.

Compositional reasoning. Our work is inspired by the success of automated methods for compositional verification of concurrent systems -a recent handbook chapter [Giannakopoulou et al. 2018] provides many useful pointers to the rich literature on this topic. Automated methods using compositional reasoning have been successfully applied in many application domains -concurrent programs (e.g., [Flanagan and Qadeer 2003;Gupta et al. 2011;Owicki and Gries 1976]), hardware designs (e.g., [Henzinger et al. 2000;Kurshan 1988;McMillan 1997], reactive systems (e.g., [Alur and Henzinger 1999]) -and for a range of properties including safety and liveness, as well as for refinement checking. [Lomuscio et al. 2010] applies assume-guarantee reasoning for verifying stability of network congestion control systems. Many such applications use temporal logic for specifying properties, as well as assumptions and guarantees at component interfaces [Pnueli 1984]. One main challenge is to come up with suitable assumptions that are strong enough to prove the properties of interest. Toward this goal, Timepiece uses a language of temporal invariants inspired by temporal logic to support checking local (i.e., per-router) properties. However, it carefully limits the expressiveness of this language, e.g., by not allowing arbitrary nesting of temporal operators, while allowing efficient verification of the proof obligations using SMT solvers.

Another main difference is that unlike most existing methods, Timepiece uses time as an explicit variable 푡 in the language of invariants. This serves two distinct but related purposes. First, 푡 provides a well-founded ordering to ensure that our proof rule is sound. Second, using 푡 explicitly in the language of invariants avoids choosing some static ordering over the components, which could be otherwise used to break a circular chain of dependencies between their assumptions (cf. the Circ rule in [Giannakopoulou et al. 2018]). Unfortunately, it is not always possible to determine a static ordering, especially in cases where we consider multiple destinations at once symbolically.

Others have used induction over time [Misra and Chandy 1981] or over traces in specific models such as compositions of Moore/Mealy machines [Henzinger et al. 2002;McMillan 1997] and reactive modules [Alur and Henzinger 1999;Henzinger et al. 2000] to prove soundness of circular assumeguarantee proof rules. However, to the best of our knowledge, no prior efforts use time explicitly in the language of assumptions. Although handling time explicitly could be more costly for decision procedures, in practice we use abstractions (via temporal operators) that result in fairly compact formulas. Our evaluations show that these formulas can be handled well by modern SMT solvers.

There have also been many efforts that automatically derive assumptions for compositional reasoning [Giannakopoulou et al. 2018]. Representative techniques include computing fixed points over localized assertions called split invariants [Cohen and Namjoshi 2007], learning-based methods [Cobleigh et al. 2003], and counterexample-guided abstraction refinement [Bobaru et al. 2008;Elkader et al. 2018]. We can view our interfaces as split invariants, since they refer to only the local state of a component. However, we depend on the users to provide them as annotations.

Modular verification of distributed systems. There have been many prior efforts [Desai et al. 2018;Hawblitzel et al. 2015;Jung et al. 2015;Ma et al. 2019;Padon et al. 2016;Sergey et al. 2018;Yao et al. 2021] for modular verification of distributed systems -see a recent work [Sergey et al. 2018] for other useful pointers. In general, they handle much richer program logics or computational models than the network routing algebras we target; hence the required assumptions and verification tasks are more complex, and often require interactive theorem-proving. The synchronous semantics of network routing algebras [Daggitt et al. 2018] that underlies our work is more closely related to hardware designs modelled as compositions of finite state machines (FSMs), where a component FSM's state at time 푡 + 1 depends on its state at time 푡 and new inputs at time 푡 + 1, some of which could be outputs from other FSM components, i.e., their state at time 푡. No existing efforts for such models (e.g., [Henzinger et al. 2002;McMillan 1997]) consider time explicitly in the assumptions.

CONCLUSION

Ensuring correct routing is critical to the operation of reliable networks. To verify today's hyperscale networks, we need modular control plane verification techniques that are general, expressive and efficient. We propose Timepiece, a radical new approach for verifying control planes based on a temporal foundation, which splits the network into small modules to verify efficiently in parallel. To carry out verification, users provide Timepiece with local interfaces using temporal operators. We proved that Timepiece is sound with respect to the network semantics and complete for closed networks, and argue that its temporal foundation is an excellent choice for modular verification.