#  Lightyear: Using Modularity to Scale BGP Control Plane Verification

Alan Tang
University of California, Los Angeles  Ryan Beckett
Microsoft  Karthick Jayaraman
Microsoft  Todd Millstein
UCLA / Intentionet  George Varghese
UCLA

###### Abstract

Current network control plane verification tools cannot scale to large
networks, because of the complexity of jointly reasoning about the behaviors
of all nodes in the network. In this paper we present a _modular_ approach to
control plane verification, whereby end-to-end network properties are verified
via a set of purely _local_ checks on individual nodes and edges. The approach
targets the verification of safety properties for BGP configurations and
provides guarantees in the face of both arbitrary external route announcements
from neighbors and arbitrary node/link failures. We have proven the approach
correct and also implemented it in a tool called Lightyear. Experimental
results show that Lightyear scales dramatically better than prior control
plane verifiers. Further, we have used Lightyear to verify three properties of
the wide area network of a major cloud provider, containing hundreds of
routers and tens of thousands of edges. To our knowledge no prior tool has
been demonstrated to provide such guarantees at that scale. Finally, in
addition to the scaling benefits, our modular approach to verification makes
it easy to localize the causes of configuration errors and to support
incremental re-verification as configurations are updated.

##  1 Introduction

Today, routing and forwarding in networks are controlled using low-level
configuration on individual routers. Researchers have developed many
techniques to analyze these configurations in order to verify that they meet a
given specification of the intended end-to-end network behavior. For example,
Minesweeper [4] models network behavior as SMT constraints, ARC [11] and
Tiramisu [1] model network behavior as a graph, and Plankton [24] uses
explicit-state model checking.

Despite their different approaches, these prior tools share one important
limitation: they model and reason about network behavior _monolithically_.
Specifically, they analyze the network and its configuration as a whole,
exhaustively exploring all possible control-plane behaviors of the network
that are induced by the complex interactions among all configuration
directives and protocols. The requirement that entire networks be analyzed as
a unit prevents these approaches from scaling to large networks, severely
limiting their practical applicability.

In this paper, we present a _modular_ approach to control plane verification.
Like the prior control-plane verifiers, Lightyear takes as input a network’s
configuration and a property to verify. However, Lightyear additionally
requires the user to provide a set of _local_ invariants that should hold on
the BGP policies of individual nodes and edges in the network. Lightyear then
automatically produces a set of _local_ checks on individual nodes and edges
that a) verify the user’s local invariants and b) ensure that these invariants
imply the given end-to-end property. We focus on BGP since it is ubiquitous,
and our approach targets a common class of _safety_ properties, which
intuitively ensure that “bad” routes never reach a particular node. For
example, our approach can express and modularly ensure that routers never
install routes to bogon addresses and that routes from one ISP are never
advertised to another one.

We have formalized our approach to modular control plane verification, proved
its correctness, and built a tool called Lightyear based on it. Our approach
can be viewed as a general approach for control plane _assume-guarantee_
reasoning—a technique that has previously been applied successfully to
software verification [16, 23] and to scale network data plane [14]
verification to colossal cloud networks. While in principle a user can provide
a different local invariant for each _location_ (node or edge) in the network,
clearly this is undesirable. Instead, we observe that in practice locations
can typically be partitioned into three sets, with all locations in a set
sharing the same local invariant. Intuitively, there are a small number of
locations whose job is to _establish_ an invariant (e.g., by tagging certain
traffic with a community), many locations that _maintain_ the invariant (e.g.,
by not stripping the community), and a small number of locations that _use_
the invariant to enforce a desired property (e.g., dropping announcements that
are tagged with the community). This reasoning naturally aligns with the
common partitioning of network nodes into _roles_ (e.g., border and core
routers) and is also analogous to modular reasoning in other settings, for
example for software [13].

Tool Feature | Minesweeper [4] | BagPipe [26] |  Plankton [24] |  ARC [11] | Lightyear
---|---|---|---|---|---
Tiramisu [1] |  Hoyan [28]
Analyzes all peer BGP routes | ● | ● | ○ | ○ | ●
Analyzes failures | ● | ○ | ● | ● | ●
Checks safety and liveness properties | ● | ◐ | ● | ● | ◐
Verification is fully automatic | ● | ● | ● | ● | ◐
Near linear scaling with network size | ○ | ○ | ○ | ○ | ●
Localizes bugs in configurations | ○ | ○ | ○ | ○ | ●
Table 1: Comparison of prior verification tools with Lightyear.

Lightyear’s approach offers several advantages over the prior work, as
summarized in Table 1:

Scalability  Lightyear performs a linear number of checks in the size (number
of nodes and edges) of the network, and the complexity of each check depends
only on the complexity of the configuration at individual nodes. Hence
Lightyear scales roughly linearly with the network size. This contrasts with
the prior approaches, which must reason about the _joint_ behavior of all
nodes’ policies. Lightyear’s local checks are also trivially parallelizable
and enable incremental re-checking when a router’s configuration changes.

Strong Guarantees  If all of Lightyear’s local checks are satisfied, then the
specified network property is guaranteed to hold for all possible external
route announcements from neighbors _and_ for all possible node/link failures.
Intuitively, the use of local checks enables this strong guarantee since each
check makes minimal assumptions about the rest of the network. As shown in the
first two rows of the table, of the prior work only Minesweeper [4] supports
reasoning about both external route announcements and failures.

Localization When prior approaches identify incorrect network behavior, the
resulting counterexample is a _global_ snapshot of the routing and forwarding
states of all routers and a packet that exhibits the violation in this state.
The operator still has the difficult job of analyzing this counterexample to
determine which router and policy is erroneous and how it is wrong. In
contrast, a local-check violation in Lightyear directly indicates which
network location is erroneous and what local invariant it violates.

To obtain these benefits, Lightyear makes two main tradeoffs, also shown in
the table. First, Lightyear supports reasoning about a restricted, but common,
class of network safety properties. Second, Lightyear’s modular approach
requires extra effort for users to specify the intended local network
invariants. However, networks are already designed in a modular and structured
fashion, so in practice these invariants tend to be simple and few in number.

To evaluate Lightyear, we perform three sets of experiments. First, we compare
the performance of Lightyear and Minesweeper on synthetically generated
networks of various sizes. Minesweeper’s time increases drastically in the
size of the network while Lightyear scales linearly. Second, we used Lightyear
to verify three end-to-end safety properties for BGP in a large cloud
provider’s wide-area network, which has hundreds of routers and tens of
thousands of BGP edges. To our knowledge no prior tool that reasons about all
possible external route announcements has been demonstrated at this scale.
Third, we run tests on a university network to show how well Lightyear can
localize violations.

In summary, we make the following contributions:

  1. 1.

We describe a novel solution to scaling control plane verification by checking
local invariants of individual routers.

  2. 2.

We formalize our modular approach, based on a formal model of BGP routing, and
prove correctness.

  3. 3.

We instantiate our approach in the tool Lightyear.

  4. 4.

We demonstrate Lightyear’s ability to scale to very large networks
experimentally.

##  2 Approach Overview

ISP1ISP2R1R2R3CustomerXNetwork

Figure 1: Example Network. Routes from ISP1 should not be sent to ISP2

In this section we illustrate how Lightyear works with the example shown in
Figure 1. In the example network, each edge represents a connection between
BGP speakers. The network contains three BGP routers: R1, R2, and R3. R1 and
R2 each have an ISP as an external neighbor. R3 is connected to an external
neighbor that is a customer. The network satisfies a standard _no-transit_
property, as shown in the figure: routes originating from ISP1 should not be
advertised to ISP2.

Existing control-plane verifiers [4, 26, 11, 1, 24] would verify this no-
transit property by creating a representation of the possible data planes that
can result from the _entire network’s configuration_ and then searching this
representation for a counterexample to the no-transit property. However, we
observe that network configurations are highly structured and modular by
design, with each node having its own responsibilities that combine to ensure
desired global properties. In our running example, the no-transit property is
ensured using a common approach based on communities and depends only on the
following _node-local_ behaviors of individual BGP route maps:  (1) R1 tags
routes from ISP1 with community 100:1;  (2) R2 filters routes tagged with
100:1 when advertising to ISP2; and  (3) no router strips community 100:1 from
routes that it advertises.  Prior tools are not aware of this modular
structure and so cannot leverage it.

Figure 2: The architecture of Lightyear.

Figure 2 shows the architecture of Lightyear. Like prior control-plane
verifiers, it takes as input the network configuration and an end-to-end
property to verify. However, Lightyear additionally requires the user to
provide _network invariants_ that specify a condition for routes to satisfy at
each _location_ in the network — either installed at a particular node or sent
along a particular edge. As we show below, these network invariants directly
capture relevant information about the modular structure of the
configurations. From these inputs Lightyear generates a set of local checks on
individual nodes in the network and uses an SMT solver to verify each one. If
all of these local checks succeed, then the end-to-end property is guaranteed
to hold, for all possible external route announcements from neighbors _and_
for all possible link and node failures in the network. Otherwise, Lightyear
provides counterexamples for each failed local check.

Type | Location(s) | Logical Formula | Description
---|---|---|---
End-to-end Property | R2 $\rightarrow$ ISP2 | $\neg\texttt{FromISP1}(r)$ | No routes sent to ISP2 come from ISP1
| ISP1 $\rightarrow$ R1 | $\mathtt{True}$ | ISP1 can send our network any route
| R2 $\rightarrow$ ISP2 | $\neg\texttt{FromISP1}(r)$ | No routes sent to ISP2 come from ISP1
Network Invariants | Other |  $\texttt{FromISP1}(r)$ $\Rightarrow\texttt{100:1}\in\textrm{Comm}(r)$ | Routes from ISP1 are tagged with community 100:1
| ISP1 $\rightarrow$ R1 |  $\left(\mathtt{True}\wedge r^{\prime}=\texttt{Import}(\mathrm{ISP1}\rightarrow\mathrm{R1},r)\right)$
$\Rightarrow\left(\texttt{FromISP1}(r^{\prime})\Rightarrow\text{100:1}\in\textrm{Comm}(r^{\prime})\right)$
| R2 $\rightarrow$ ISP2 |  $\left(\left(\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)\right)\wedge r^{\prime}=\texttt{Export}(\mathrm{R2}\rightarrow\mathrm{ISP2},r)\right)$
$\Rightarrow\neg\texttt{FromISP1}(r^{\prime})$
| Other Edge $E$ |  $\left(\left(\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)\right)\wedge r^{\prime}=\texttt{Export}(E,r)\right)$
$\Rightarrow\left(\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)\right)$
Generated Checks |  |  $\left(\left(\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)\right)\wedge r^{\prime}=\texttt{Import}(E,r)\right)$
$\Rightarrow\left(\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)\right)$
Table 2: Using Lightyear to prove the no-transit property from figure 1. The
user-provided global property and local invariants are show in green.
Lightyear-generated local verification checks are shown in blue.

In the rest of this section, we show how Lightyear modularly verifies the no-
transit property for the network in figure 1; relevant information is
summarized in Table 2.

End-to-end Property  In Lightyear, the end-to-end property of interest is
specified as a pair of a particular location in the network and a predicate on
the routes reaching that location. As shown in the first line of the table,
the no-transit property specifies that no route on the edge from R2 to ISP2
should originate at ISP1. To enable the expression of rich properties,
Lightyear allows users to define _ghost attributes_ that conceptually update
message headers with additional fields. This is a common technique in software
verification, where additional variables are introduced that do not affect the
computation but allow for easier property specification [9]. In the table,
$\texttt{FromISP1}(r)$ is a boolean ghost variable that is defined by the user
to be false in all originated routes, set to true by the import filter on R1
from ISP1, and left unchanged by all other filters.

Network Invariants  While in principle the user could specify a different
invariant for each network location, in practice locations can be partitioned
into a small number of equivalence classes, each playing a different role in
ensuring the end-to-end property. In our running example, there are three
equivalence classes, which correspond exactly to the three node-local
behaviors described earlier that ensure the no-transit property. Table 2 shows
the three associated local invariants. First, no assumption is made about the
routes coming from ISP1 to R1, so the associated predicate is True. Second,
routes coming from R2 to ISP2 should not come from ISP1. Note that this
invariant is identical to the end-to-end property, which is common but need
not be the case. Third, all other locations in the network should satisfy the
key correctness invariant: routes from ISP1 must be tagged with the community
100:1. Notably, this three-part decomposition is analogous to the modular
verification of software [13], which typically involves a _precondition_ that
is assumed to hold initially, a _postcondition_ to be proven, and one or more
_inductive invariants_ that hold throughout each execution and are sufficient
to imply the postcondition.

Generated Checks  Given this information from the user, Lightyear
automatically generates local checks to validate the given network invariants.
Notably, each local check pertains to a single BGP filter of a single network
router. Together these checks implement a form of _assume-guarantee reasoning_
[16, 23]: each location’s network invariant is proven under the assumption
that the local invariant of its directly connected locations hold. As we
formalize later, together these checks imply that all of the local invariants
of all locations in the network are respected.

The bottom of Table 2 shows the local checks that Lightyear automatically
generates for our running example. The first check ensures that the import
filter at R1 on the edge from ISP1 to R1 establishes the key invariant
$\texttt{FromISP1}(r)\Rightarrow\text{100:1}\in\textrm{Comm}(r)$. Since that
filter tags all routes with community 100:1, the check is easily provable by
an SMT solver. The second check ensures that the key invariant is sufficient
to ensure that routes from ISP1 are not exported on the edge from R2 to ISP2.
Since the export filter at R2 on that edge drops all routes that are tagged
with 100:1, the check passes. The third set of checks ensure that the key
invariant is preserved by all other import and export filters in the network.
Since these filters never strip community 100:1 from a route, the checks
pass.111There are also some analogous checks for originated routes, but they
are omitted here for simplicity. Lastly (not shown in the figure), Lightyear
generates a local check that the invariant on the edge from R2 to ISP2 implies
the end-to-end property. This check is trivially since the two properties are
identical.

In summary, Lightyear’s approach to control-plane verification leverages the
modular structure that is already present in the network configurations. By
requiring the user to make this structure explicit through a set of local
invariants at each location, Lightyear soundly reduces checking an end-to-end
network property to a set of checks that each pertain to a single BGP import
or export filter. This approach has numerous benefits over the prior,
monolithic approaches. First, our approach is highly scalable, since the
number of checks is linear in the number of edges in the BGP network graph.
Second, Lightyear’s modular checks provide an extremely strong guarantee,
covering both all possible external route announcements from neighbors and all
possible failure scenarios. Third, the modular approach naturally supports
incremental verification when a node is updated: only the local checks
pertaining to that node must be re-checked. Finally, modularity has large
benefits for error localization and understanding: the failure of a local
check directly pinpoints the erroneous import or export filter and the local
invariant that it fails to satisfy.

##  3 Formal Model of BGP

In this section we define a model of BGP in terms of traces and axioms on
traces. This model is used in the next section to make Lightyear’s approach
precise and to prove its correctness.

###  3.1 BGP Topologies and Policies

We model a network’s BGP configuration as consisting of two parts: a topology
and a policy. A BGP network topology is a tuple of the form
$(\textsc{Routers},\textsc{Externals},\textsc{Edges})$, where:

  1. 1.

Routers is the set of routers for which the user provides configurations.

  2. 2.

Externals is the set of external routers. That is, there is no provided
configuration, but each such router is an eBGP or iBGP peer with at least one
router in Routers.

  3. 3.

Edges is the set of directed edges corresponding to BGP peering sessions.

The network topology forms a graph with Routers $\cup$ Externals as the set of
nodes and Edges as the set of edges. We will use the notation $A\rightarrow B$
to refer the directional edge ($A$, $B$) in the topology.

A BGP _route_ (or _route advertisement_) is modeled as a tuple

$(\text{Prefix, ASPath, NextHop, LocalPref, MED, Comm})$

where:

  1. 1.

NextHop, LocalPref, and MED are integer values

  2. 2.

Prefix is a pair consisting of an IP address and a length, both of which are
integer values

  3. 3.

ASPath and Comm are lists of integer values

Let Routes denote the set of all routes. We will use $\textrm{Comm}(r)$ to
refer to the Comm field of the route $r$, $\textrm{Prefix}(r)$ to refer the
prefix of $r$, and so on. Real BGP messages contain a few other attributes as
well, which could be incorporated into this model in the future. Lightyear
also allows routes to be extended with additional “ghost” attributes, such as
the FromISP1 attribute from section 2; they are described in Section 4.5.

We model the BGP network policy as consisting of three functions, which can be
derived from the BGP and route-map configurations of each router:

  1. 1.

$\texttt{Import}:\textsc{Edges}\times\textsc{Routes}\rightarrow\textsc{Routes}\cup\\{\textsc{Reject}\\}$

  2. 2.

$\texttt{Export}:\textsc{Edges}\times\textsc{Routes}\rightarrow\textsc{Routes}\cup\\{\textsc{Reject}\\}$

  3. 3.

$\texttt{Originate}{}:\textsc{Edges}\rightarrow\mathbb{P}(\textsc{Routes})$

For an edge $A\rightarrow B$ and a route $r$, $\texttt{Import}(A\rightarrow
B,r)$ either returns the route produced when applying the import filter at $B$
to the route $r$ sent from $A$ or returns Reject if the import filter rejects
the route. $\texttt{Export}(A\rightarrow B,r)$ either returns the route
produced when applying the export filter at $A$ to the route $r$ sent to $B$
or returns Reject if the export filter rejects the route.
$\texttt{Originate}(A\rightarrow B)$ returns the set of routes that are
originated at $A$ and sent to $B$.

###  3.2 BGP Traces

We model the semantics of BGP as a set of allowed _traces_. Our semantics is a
variant of that from the Bagpipe tool [26], but simplified for our setting.

A trace is a sequence of _events_. In BGP, there are three types of events:
recv, slct, and frwd. For $r\in\textsc{Routes},R\text{
and}N\in\textsc{Routers},\text{ and }R\rightarrow N\in\textsc{Edges}$:

  1. 1.

$\texttt{recv}(N\rightarrow R,r)$ occurs when $R$ receives route $r$ from
neighbor $N$

  2. 2.

$\texttt{slct}(R,r)$ occurs when $R$ selects $r$ as the best route for a
destination and installs it

  3. 3.

$\texttt{frwd}(R\rightarrow N,r)$ occurs when $R$ forwards route $r$ to the
neighbor $N$

We denote the set of all traces as Traces.

A _valid_ trace is one that could occur for a given topology and policies,
according to the BGP semantics. We formalize the notion of trace validity as a
set $\textsc{Valid}\subseteq\textsc{Traces}$ of traces that satisfy specific
properties. However, our formalization deliberately over-approximates the set
of such traces — we include some traces that are not actually legal according
to the BGP semantics. Doing so has two advantages. First, over-approximation
simplifies our formalism considerably yet is still sound for reasoning about
safety properties, which is our focus. For example, our formalism does not
need to model the route selection process at all, instead assuming that any
received route can potentially be selected. Second, over-approximation allows
us to reason about failures “for free,” as the set of traces that we consider
valid includes all of those that could occur under any failure scenario (see
Section 4.4).

We consider a trace $A_{1},A_{2},\dots,A_{n}$ to be valid, and hence part of
the set Valid, if it satisfies the following properties, for all $1\leq k\leq
n$:

  1. 1.

If $A_{k}=\texttt{recv}(N\rightarrow R,r)$, then either:

    1. (a)

$N\in\textsc{Externals}$, or

    2. (b)

there exists $j<k$ such that $A_{j}=\texttt{frwd}(N\rightarrow R,r)$

  2. 2.

If $A_{k}=\texttt{slct}(R,r)$, then there exists $j<k$,
$r^{\prime}\in\textsc{Routes}$, and
$N\in\textsc{Routers}\cup\textsc{Externals}$ such that
$A_{j}=\texttt{recv}(N\rightarrow R,r^{\prime})$ and
$r=\texttt{Import}(N\rightarrow R,r^{\prime})$

  3. 3.

If $A_{k}=\texttt{frwd}(R\rightarrow N,r)$, then either:

    1. (a)

$r\in\texttt{Originate}(R\rightarrow N)$, or

    2. (b)

there exists $j<k$ and $r^{\prime}\in\textsc{Routes}$ such that
$A_{j}=\texttt{slct}(R,r^{\prime})$ and $r=\texttt{Export}(R\rightarrow
N,r^{\prime})$

Intuitively these properties require basic consistency among the events in a
trace: a received route at $R$ from $N$ must be preceded by a forwarding of
that route from $N$ to $R$ (unless $N$ is external); a selected route must be
the result of applying an import filter to a received route; and a forwarded
route from $R$ to $N$ must either originated at $R$ or be the result of
applying the appropriate export filter to a selected route at $R$.

##  4 Lightyear

Lightyear takes as input three things: the router configurations, a network
property to be verified, and invariants for each location (node or edge) in
the network. Lightyear then generates and performs a set of local checks on
individual BGP filters in the network. If all checks succeed, that implies
that the given network property holds. Otherwise, a counterexample is
produced, which points the user to a specific location whose network invariant
could not be proven.

This section makes Lightyear’s approach precise. We describe the tool’s three
inputs, show the local checks that Lightyear generates from these inputs, and
prove the correctness of the approach. Finally, we describe two important
extensions to this formal model, respectively to reason about arbitrary
network failures and to enable users to provide additional ghost route
attributes.

###  4.1 Inputs

Lightyear’s first input, the network configurations, is standard. As described
previously, the configurations are used to build the BGP topology as well as
the policy functions.

The second input is the network property. Lightyear focuses on a common class
of safety properties, which requires that all route announcements that can
reach a particular location satisfy certain constraints. Many network policies
fall into this class of safety properties, for example bogon filtering;
ensuring that a network only advertises routes to its own destinations; no-
transit policies (see Section 2); and forms of isolation between nodes or
groups of nodes. Such properties can also express complex constraints among
BGP attributes, for example that prefixes in a specific range always have a
particular local preference or MED value.

Formally, a network property is a pair $(\ell,P)$ where:

$(\ell,P)\in(\textsc{Routers}\cup\textsc{Edges})\times\mathbb{P}(\textsc{Routes})$

$\ell$ is a location, either a router or an edge, and $P$ is a set of routes
matching a particular constraint. In practice, users directly specify a
logical constraint on route attributes that represents $P$. For example, users
might specify the location $(R1\rightarrow R2)$ and a constraint
$\text{1:1}\in\textrm{Comm}(r)$, specifying the property that routes sent on
the edge $R1\rightarrow R2$ should always have the community 1:1.

Each network property $(\ell,P)$ corresponds to a property of all possible
valid traces, as defined in the previous section — all routes that can reach
location $\ell$ must satisfy $P$. Formally, a network satisfies a property
$(\ell,P)$ if for all
$T\in\textsc{Valid},r\in\textsc{Routes},R,N\in\textsc{Routers}$

  * •

if $\ell=R$ and $\texttt{slct}(R,r)\in T$, then $r\in P$

  * •

if $\ell=R\rightarrow N$ and $\texttt{frwd}(R\rightarrow N,r)\in
T\lor\texttt{recv}(R\rightarrow N,r)\in T$, then $r\in P$

Finally, Lightyear’s third input is a set of network invariants, one per
location in the given network. Formally, the network invariants are modeled as
a set of pairs denoted $I$:

$I\subseteq(\textsc{Routers}\cup\textsc{Edges})\times\mathbb{P}(\textsc{Routes})$

Each element of the set has the form $(\ell,P)$, where $\ell$ is a location
and $P$ is a set of routes, as in the network property defined above. The
semantics of each pair is a property of traces, analogous to the semantics of
network properties shown above.

We require that there exist exactly one pair in $I$ per location in the given
network, and we use the notation $I_{\ell}$ to denote the set $P$ of routes
associated with location $\ell$ in $I$. We also require that $I_{R\rightarrow
N}=\textsc{Routes}$ for each edge $R\rightarrow N$ where
$R\in\textsc{Externals}$. In other words, we make no assumption about routes
coming from external neighbors but rather assume that any route may be
advertised.

###  4.2 Local Checks

Given the network configuration, network property $(\ell,P)$, and network
invariants $I$, Lightyear generates the following local checks for each edge
$A\rightarrow B$ in the network topology:

  1. 1.

Import: For all $r,r^{\prime}\in\textsc{Routes}$, if
$r=\texttt{Import}(A\rightarrow B,r^{\prime})$ and $r^{\prime}\in
I_{A\rightarrow B}$, then $r\in I_{B}$.

  2. 2.

Export: For all $r,r^{\prime}\in\textsc{Routes}$, if
$r=\texttt{Export}(A\rightarrow B,r^{\prime})$ and $r^{\prime}\in I_{A}$, then
$r\in I_{A\rightarrow B}$.

  3. 3.

Originate: For all $r\in\textsc{Routes}$, if
$r\in\texttt{Originate}(A\rightarrow B)$, then $r\in I_{A\rightarrow B}$.

If the router $B$ is external then the import check is not performed, and
similarly if the router $A$ is external then the export and originate checks
are not performed. In our implementation of Lightyear, the local checks are
performed by modeling import and export filters using SMT constraints and
invoking an SMT solver to validate each check or provide a counterexample.

Finally, Lightyear checks that the network invariants $I$ imply the network
property $(\ell,P)$. This is done simply by requiring that $I_{\ell}\subseteq
P$, i.e. that the network invariant for $\ell$ implies the network property
$P$. Again this check is performed with an SMT solver.

###  4.3 Correctness

In this section we prove that Lightyear’s modular approach to control-plane
verification is correct.

First we state and prove the key lemma, which says that the local checks are
sufficient to ensure that the network invariants $I$ hold, for all valid
traces.

Lemma: Given a BGP topology and policy as well as network invariants $I$, let
$C$ be the set of Import, Export, and Originate checks that Lightyear
generates. If all checks in $C$ pass, then for all
$T\in\textsc{Valid},r\in\textsc{Routes},R,N\in\textsc{Routers}$:

  * •

if $\texttt{slct}(R,r)\in T$, then $r\in I_{R}$

  * •

if $\texttt{frwd}(R\rightarrow N,r)\in T\lor\texttt{recv}(R\rightarrow N,r)\in
T$, then $r\in I_{R\rightarrow N}$

Proof: The proof is by induction on the length of the (partial) trace $T$.

Base case: For a partial trace of length 0, there are no events, so the
statement is vacuously true.

Inductive case: Suppose $T=A_{1},A_{2},\dots,A_{k+1}$. We assume by induction
that the statement is true for $A_{1},A_{2},\dots,A_{k}$. We do a case
analysis on the event $A_{k+1}$:

Case $A_{k+1}=\texttt{recv}(N\rightarrow R,r)$, so we have to show that $r\in
I_{N\rightarrow R}$. By the trace validity axioms, either:

  1. 1.

$N\in\textsc{Externals}$. In this case we know that $I_{N\rightarrow
R}=\textsc{Routes}$, so $r\in I_{N\rightarrow R}$.

  2. 2.

There exists $j<k+1$ such that $A_{j}=\texttt{frwd}(N\rightarrow R,r)$. Then
by the inductive hypothesis we have that $r\in I_{N\rightarrow R}$.

Case $A_{k+1}=\texttt{slct}(R,r)$, so we have to show that $r\in I_{R}$. From
the trace validity axioms, we know that there exists
$j<k+1,r^{\prime}\in\textsc{Routes}$, and
$N\in\textsc{Routers}\cup\textsc{Externals}$ such that
$A_{j}=\texttt{recv}(N\rightarrow R,r^{\prime})$ and
$r=\texttt{Import}(N\rightarrow R,r^{\prime})$. From the inductive hypothesis,
we know that $r^{\prime}\in I_{N\rightarrow R}$. Therefore by the Import check
in $C$ for $N\rightarrow R$, we can conclude that $r\in I_{R}$.

Case $A_{k+1}=\texttt{frwd}(R\rightarrow N,r)$, so we have to show that $r\in
I_{R}$. By the trace validity axioms, either:

  1. 1.

$r\in\texttt{Originate}(R\rightarrow N)$. Then from the Originate check in $C$
for $R\rightarrow N$ we have that $r\in I_{R\rightarrow N}$.

  2. 2.

There exists $j<k+1$ and $r^{\prime}\in\textsc{Routes}$ such that
$A_{j}=\texttt{slct}(R,r^{\prime})$ and $r=\texttt{Export}(R\rightarrow
N,r^{\prime})$. From the inductive hypothesis, we have that $r^{\prime}\in
I_{R}$. Then from the Export check in $C$ for $R\rightarrow N$, we can
conclude that $r\in I_{R\rightarrow N}$.

Now we prove the correctness theorem for Lightyear, which says that
Lightyear’s checks are sufficient to ensure that the given network property
holds, for all valid traces.

Theorem: Given a BGP topology and policy, a network property $(\ell,P)$, and
network invariants $I$, let $C$ be the set of Import, Export, and Originate
checks that Lightyear generates. If all checks in $C$ pass and
$I_{\ell}\subseteq P$, then for all
$T\in\textsc{Valid},r\in\textsc{Routes},R,N\in\textsc{Routers}$:

  * •

if $\ell=R$ and $\texttt{slct}(R,r)\in T$, then $r\in P$

  * •

if $\ell=R\rightarrow N$ and $\texttt{frwd}(R\rightarrow N,r)\in
T\lor\texttt{recv}(R\rightarrow N,r)\in T$, then $r\in P$

Proof: There are two cases:

  1. 1.

$\ell=R$ and $\texttt{slct}(R,r)\in T$. From the earlier lemma we have that
$r\in I_{\ell}$, and since $I_{\ell}\subseteq P$ it follows that $r\in P$.

  2. 2.

$\ell=R\rightarrow N$ and $\texttt{frwd}(R\rightarrow N,r)\in
T\lor\texttt{recv}(R\rightarrow N,r)\in T$. Again from the earlier lemma we
have that $r\in I_{\ell}$, and since $I_{\ell}\subseteq P$ it follows that
$r\in P$.

###  4.4 Fault Tolerance

A significant benefit of Lightyear’s approach to control-plane verification is
that it supports reasoning about failures “for free.” That is, if all of
Lightyear’s checks pass, then the given network property is guaranteed to hold
not only in the failure-free case but also in the presence of _arbitrary_ node
and link failures.

The fact that Lightyear soundly reasons about failures is a consequence of our
over-approximate notion of trace validity (Section 3.2). Specifically, any
trace that is feasible according to the given BGP topology and passes the
import/export filters along the corresponding path is considered valid. Hence,
every trace that can occur under any failure scenario is already considered
valid. By our correctness theorem, all of these traces satisfy the property
$(\ell,P)$.

One potential downside of using an over-approximate notion of trace validity
is that it could cause Lightyear to incur false positives — signaling errors
when none exist. Notably, trace validity does not take into account the BGP
preference relation, but rather assumes that any received route could be
installed at a router. However, our notion of validity is quite natural for
the class of properties that Lightyear supports, namely those that ensure that
certain “bad” events never occur. Indeed, when given correct invariants,
Lightyear did not incur any false positives in our evaluation (Section 6).

###  4.5 Ghost Attributes

As described in Section 4.1, a property that Lightyear verifies is described
as a set of routes that can reach a particular location. By default, that set
can be described as a predicate on the attributes of a route $r$, for example
$\text{1:1}\in\textrm{Comm}(r)$. However, many natural properties cannot be
described using solely route attributes. For example, in our no-transit
example from Section 2 we would like to specify that the route $r$ does not
originate at ISP1.

To increase Lightyear’s expressiveness, we allow users to define their own
ghost attributes, which conceptually extend each route with additional fields.
For example, the $\texttt{FromISP1}(r)$ ghost attribute from Section 2 is used
to indicate whether $r$ originated from ISP1. A ghost attribute is defined by
specifying the set of values that the attribute can take, along with updates
to the Import, Export, and Originate functions that make up the given
network’s policy (Section 3.1).

In the case of $\texttt{FromISP1}(r)$, the user would declare it as a boolean
attribute and provide the following updates to the network policy functions
(see Figure 1):

  * •

the import filter on the edge ISP1 $\rightarrow$ R1 sets FromISP1 to true

  * •

the import filter on the edge ISP2 $\rightarrow$ R2 sets FromISP1 to false

  * •

all other import and export filters leave FromISP1 unchanged

  * •

all originated routes have FromISP1 set to false

Many other natural network properties can be expressed using ghost attributes.
For example, it is possible to define a WaypointR attribute that is true only
for routes that have been processed by a particular router $R$. This can be
done by specifying that filters on $R$ set WaypointR to true, origination as
well as import filters from external neighbors at other routers set WaypointR
to false, and filters between the routers in the network leave WaypointR
unchanged.

Ghost attributes do not affect our description of Lightyear or proof of its
correctness above at all, as they do not depend on the specific set of
attributes that are in a route.

##  5 Implementation

Lightyear uses Batfish [10] to parse network configurations and determine the
topology and policy. Since Batfish converts the configurations into a vendor-
independent format, this allows Lightyear to handle configurations from
numerous different vendors, such as Cisco and Juniper.

Properties and invariants are specified as Python functions mapping routers
and edges to BGP route constraints. Our implementation allows users to define
one boolean ghost variable, with Python functions to specify how route import,
export, and origination should affect the variable’s value. Currently we allow
ghost variables to be transformed based on the location in the network, but
not based on other route attributes. For example, users can specify that an
import filter changes the value of a variable to true, but users cannot
specify that the filter transforms the variable to true if the prefix is
$10.0.0.0/8$. This is not a fundamental limitation but simplifies our
implementation and has been sufficient for our use cases.

The code for generating local checks from the user-provided invariants is
written in Python. The local checks rely on the symbolic modeling of BGP
policies [4]. Specifically, BGP route announcements are modeled as symbolic
variables, and BGP route maps in the configurations are modeled as SMT
constraints on these symbolic variables, and the Z3 SMT solver [7] is used to
perform the local checks. Minesweeper’s symbolic analysis supports many common
features of BGP route maps, like communities, local preference, and MEDs, as
well as other configurable aspects of BGP like route origination. However, it
does not support reasoning about AS-path filtering, which is necessary for one
of our use cases. For that, we use an alternate backend for symbolic route
analysis from Batfish that is based on binary decision diagrams (BDDs) [3].

There are many possible optimization opportunities to exploit in the future.
For example, the local checks are easily parallelizable — separate processes
can be created to perform checks from multiple routers at the same time.
Another possibility is performing a single local check for policies duplicated
in multiple routers. Despite lacking these sorts of optimizations, Lightyear
was still able to scale to verify properties of the wide-area network of a
major cloud provider, as we show in the next section.

##  6 Evaluation

In this section, we present three sets of experiments. First we compare the
differences in scaling between Lightyear and Minesweeper [4] on synthetically
generated networks of various sizes. We use Minesweeper since it is a state-
of-the-art tool that is capable of checking the kinds of properties that we
target, which require reasoning about all possible external route
announcements. Second, we use Lightyear to verify three different properties
of the wide-area network (WAN) of a major cloud provider, which has hundreds
of routers and tens of thousands of edges. To our knowledge, Lightyear is the
first tool that can scale to verify these kinds of properties on a network of
that size. These experiments were performed on a system with 32GB of RAM and 8
cores, though no explicit parallelism was used. Third, we show how the output
from Lightyear can aid in understanding and localizing errors in a university
network.

###  6.1 Scaling Experiments

Routers | Edges |  Lightyear Time |  Minesweeper Time
---|---|---|---
10 | 100 |  4s |  4s
20 | 400 |  13s |  340s
30 | 900 |  26s |  581s
40 | 1600 |  50s |  X
50 | 2500 |  74s |  X
60 | 3600 |  114s |  X
70 | 4900 |  152s |  X
80 | 6400 |  205s |  X
90 | 8100 |  256s |  X
100 | 10000 |  327s |  X

Table 3: Comparison of runtimes between Lightyear and Minesweeper for
synthetic networks of various sizes. X denotes a time that exceeds two hours.
The time does not include time taken to parse configurations into the Batfish
vendor-independent format.

First we compared Lightyear and Minesweeper tools on synthetic test cases. We
use a BGP full mesh where each router is connected to one external neighbor
through eBGP and all other routers through iBGP. This leads to a total of
$N^{2}$ edges in a network of size $N$. The policy of the network was kept
relatively simple, with each eBGP connection using only prefix and community
filters. We checked a simple no-transit property similar to the example shown
in figure 1. The number of routers, the number of edges, and the run times are
shown in Table 3. Minesweeper does not terminate within two hours when run on
a network of size 40, while Lightyear verifies a network of size 100 in 5.5
minutes.

$10$$20$$30$$40$$50$$60$$70$$80$$90$$100$$0$$5{,}000{,}000$$10{,}000{,}000$$15{,}000{,}000$$20{,}000{,}000$Number
of RoutersCountNumber of Variables (Minesweeper)Number of Constraints
(Minesweeper)

(a) Number of variables and constraints generated by Minesweeper for synthetic
networks.

$10$$20$$30$$40$$50$$60$$70$$80$$90$$100$$0$$2{,}000$$4{,}000$Number of
RoutersCountMaximum Number of Variables (Lightyear)Maximum Number of
Assertions (Lightyear)

(b) The maximum number of variables and constraints in any single local check
generated by Lightyear.

$10$$20$$30$$0$$200$$400$$600$Number of RoutersTime (seconds)Constraint
Solving Time (Minesweeper)Total Time (Minesweeper)

(c) The amount of time used by Minesweeper to verify a property of synthetic
networks. Runtime for networks with 40 routers or more exceeds two hours. This
does not include time used to parse configurations.

$10$$20$$30$$40$$50$$60$$70$$80$$90$$100$$0$$100$$200$$300$Number of
RoutersTime (seconds)Constraint Solving Time (Lightyear)Total Time (Lightyear)

(d) The amount of time used by Lightyear to verify a property in synthetic
networks. This does not include time used to parse configurations.

Figure 3: Comparison between Lightyear and Minesweeper on synthetic networks
of various sizes.

Figure 3 provides more details on these results by comparing the number of SMT
variables and assertions (i.e., constraints) generated by each tool, as well
as the amount of time used to solve the SMT constraints compared to the total
computation time. As the network size increases, Minesweeper requires several
orders of magnitude more SMT variables and assertions than the maximum number
required by Lightyear for any local check. As a result, SMT solving time
dominates the run time of Minesweeper and is the limiting factor on its
ability to scale, while for Lightyear the solving time is a relatively small
portion of the total time.

Routers | Lightyear Time | Minesweeper Time
---|---|---
10 | 55s | 80s
20 | 145s | 523s
50 | 490s | X
100 | 792s | X

Table 4: Comparison of runtimes between Lightyear and Minesweeper for network
subsets of various size. X denotes a time that exceeds two hour

We also ran scalability experiments on subsets of the cloud provider’s WAN
network of various sizes. For each such subset we verified a property that
external route announcements for bogon routes are disallowed (see the first
use case in the next subsection). The results are shown in Table 4. The
computation times are greater than for the synthetic networks of similar size,
since the WAN configurations are more complex. Nonetheless, again Lightyear is
scaling very well, verifying the property for a network of 100 routers in
about 13 minutes, while Minesweeper times out after 2 hours. Further, as
described below, Lightyear scales to verify the no-bogons property on the
entire WAN in 240 minutes, while Minesweeper does not finish even after
running for 24 hours.

###  6.2 Cloud WAN

Type | Locations ($l$) | Logical Formula ($I_{l}$) | Description
---|---|---|---
End-to-end Property |  Any R in network |  $FromPeer(r)\implies$ $\textsc{Prefix}(r)\notin\textsc{Bogons }$ |  Bogon prefixes from peers should not be accepted
| $R\in\textsc{Routers}$ |  $FromPeer(r)\implies$ $\textsc{Prefix}(r)\notin\textsc{Bogons }$ | Bogon prefixes from peers should not be accepted at routers
Network Invariants |  Internal edges R1 $\rightarrow$ R2 |  $FromPeer(r)\implies$ $\textsc{Prefix}(r)\notin\textsc{Bogons }$ | Bogon prefixes from peers should not be sent along edges
| Other | $True$ | Edges to and from external peers are unconstrained
(a) The end-to-end property and network invariants that are needed to verify
that the network does not accept bogons from external peers.

Type | Locations ($l$) | Logical Formula ($I_{l}$) |  Description
---|---|---|---
End-to-end Property | $R\notin\textsc{Region}$ |  $FromRegion(r)\implies$ $\textsc{ Prefix}(r)\notin\textsc{ReusedIPs}$ |  Routers outside a region should not accept routes with reused addresses from that region
| $R\in\textsc{Region}$ |  $FromRegion(r)\ \land$ $\textsc{ Prefix}(r)\in\textsc{ReusedIPs }\implies$ $\textsc{RegionalComms}\cap\textrm{Comm}(r)=\\{C\\}$ |  Routes with reused addresses are tagged with a community for that region and no other region
Network Invariants | $R\notin\textsc{Region}$ |  $FromRegion(r)\implies$ $\textsc{ Prefix}(r)\notin\textsc{ReusedIPs}$ |  Routers outside a region should not accept routes with reused addresses from that region
| R1 $\rightarrow$ R2 | $I_{R1}$ |  Edges have same invariant as sending router
| E $\rightarrow$ R | $\textrm{Comm}(r)=\emptyset$ |  Edges from external peers have no communities
(b) The end-to-end property and network invariants that are needed to verify
that reused addresses are not accepted by any router outside the region. Since
the tool does not model community deletion, we assume that routes received
from external peers have no communities.

Type | Locations ($l$) | Logical Formula ($I_{l}$) |  Description
---|---|---|---
End-to-end Property |  Edges to peers R $\rightarrow$ P | $\neg FromPeer(r)$ |  Routers should not send routes received from a peer to another peer
| $R\in\textsc{Routers}$ |  $FromPeer(r)\implies$ $\texttt{AsPath}(r)\in\textsc{ValidPaths }\land$ $\textsc{Prefix}(r)\in\textsc{ValidPfxs}$ |  Routes from a peer should only have specific As Paths and prefixes
Network Invariants |  Internal edges R1 $\rightarrow$ R2 | $I_{R1}$ |  Edges inside network have same invariant as sending router
|  Edges to peers R $\rightarrow$ P | $\neg FromPeer(r)$ |  Routers should not send routes received from a peer to another peer
| Other | True |  Other edges are unconstrained
(c) The end-to-end property and network invariants that are needed to verify
no transit between peers. When checking, $FromPeer$ here refers to a limited
set of peers with common policies

Table 5: End-to-end properties and network invariants for three use cases in
the WAN.

In this section, we show that Lightyear can scale to verify a range of
properties on the wide-area network (WAN) of a major cloud provider,
containing hundreds of routers and tens of thousands of edges. To our
knowledge no prior tool that verifies properties of all possible external
announcements from neighbors has been demonstrated to scale to such a size. We
describe three use cases in turn.

No Bogons: First, we verified that no router in the network installs a bogon
route advertised from an external neighbor. Bogons refer to address spaces
that are not used on the public internet and so should only be used
internally. The property to verify is as follows, for each node $R$ in the
network:

$(R,\\{r\ |FromPeer(r)\implies\textsc{Prefix}(r)\notin\textsc{Bogons}\\}$

Here, Bogons is a set of bogon prefixes, and the $FromPeer$ property is
defined with a ghost variable that is set to true on all edges coming from
external peers — external routers that have a different ASN from that of the
cloud network. Note that the property still allows routers to receive routes
to private addresses from iBGP and from eBGP sessions with other routers in
the same network.

The WAN enforces the property above by having BGP filters at edge routers that
drop announcements to bogon routes from external peers. This approach is
easily verified to be correct by Lightyear, using the network invariants shown
in Table 5(a). In this case, the network invariants are identical to the
network property, except that no assumptions are made on edges to and from
external peers. Lightyear’s checks on the entire WAN network took a total of
about 240 minutes, with the average check lasting only a fraction a second. We
attempted to use Minesweeper to verify the no-bogons property for all possible
external route announcements (but without considering failures), but it did
not finish even after 24 hours.

Proper IP Reuse: In the second use case, we used Lightyear to verify that
reused IPs are contained within a region. In the cloud network, some private
IPv4 addresses are reused in different regions. Traffic sent to these private
addresses must stay within the region. We verified this property for a single
region. Specifically the property to verify is as follows, for each router $R$
that is _not_ part of the region:

$(R,\\{r\ |\ FromRegion(r)\implies\textsc{
Prefix}(r)\notin\textsc{ReusedIPs}\\})$

Here $FromRegion(r)$ is a ghost variable that is set to true only on routes
coming from external routers in the particular region, and ReusedIPs is the
set of prefixes that are reused.

The WAN enforces this property by tagging routes for reused IP addresses with
a region-specific community $C$ when they are received from data centers.
Routers in the same region then accept routes tagged with that community,
while routers in other regions reject them. The network invariants that we
provided to Lightyear to verify this approach are shown in Table 5(b). One
subtlety is that routes to reused IP addresses in the region must not only
have the community $C$, but they also must not be tagged with the community of
any other region. Otherwise, the routes could be accidentally accepted by
those other regions. This property is enforced in the WAN by deleting all
communities on routes coming from the data centers, before adding the
community $C$. Unfortunately, neither the SMT modeling of routing from
Minesweeper nor the BDD modeling of routing from Batfish supports community
deletion. Therefore, we instead verify a weaker version of the proper IP reuse
property. Specifically, we make the assumption that external routes contain no
communities, as shown in the last row of Table 5(b), and Lightyear
successfully verifies proper IP reuse under this assumption.

No Transit: In the third use case, we verified that BGP routes from peers are
not exported to other peers. For edges from a router $R$ to a peer $P$, the
property to verify is as follows:

$(R\rightarrow P,\\{r\ |\ \neg FromPeer(r)\\})$

Again, $FromPeer(r)$ is defined with a ghost variable that is set to true only
on routes from certain peers. For this case, we did not check every peer but
focused on the peers using a common policy, which comprise most of the eBGP
connections.

Policy |  Mechanism
---|---
Some routes should not be sent to certain regions or continents |  Routes are tagged with communities and dropped upon entering region
Some customer routes are private and should not be advertised to peers |  Private routes are marked with a community by customers and dropped on edges to peers
Only specially tagged customer routes are advertised to certain partner services |  Routes are marked with a community by customers and those without community are dropped on edge to partner
Only customer routes can be advertised to peers (no transit between peers) |  Routes are marked by a community, and those without community are dropped at the edges to peers
All routes from peers must have the origin attribute IGP |  Routes from peers have their origin attribute set at the edge
Do not accept routes with private ASNs |  Routes that have private ASNs are dropped in all edge routers
Do not accept default route from peers |  Default route is dropped from peers in all edge routers
Do not accept our own routes from peers |  Routes owned by the network are dropped in all edge routers
Table 6: Example cloud network policies that can be expressed and checked with
Lightyear.

This property is enforced by the WAN using AS-path filtering. Specifically,
the configurations ensure that routes accepted from certain peers match
specific AS-path regular expressions and prefixes, and the edges to other
peers filter out those same routes. The network invariants used to verify this
approach are shown in Table 5(c). Here, ValidPaths is the set of AS paths that
are allowed for routes coming from certain peers, represented as a regular
expression. Similarly, ValidPfxs is the set of prefixes that are allowed for
routes coming from those peers. We ran this check primarily on the edge
routers responsible for peering. Lightyear successfully verified the no-
transit property.

Other Use Cases: As demonstrated above, Lightyear can verify complex policies
on real-world configurations at scale. Many other common properties of wide-
area networks fit within Lightyear’s expressiveness. For example, communities
are commonly used to mark routes based on where they can be advertised or how
they should be treated [8]. Some examples of these kinds of properties, which
can be expressed and verified in our approach, are listed in Table 6.

###  6.3 University Network

Our experiences running Lightyear on the campus network of a large university
show how the local counterexamples produced can aid in refining the network
invariants and localizing errors. We used Lightyear to verify the property
that only university-owned address blocks can be advertised to the ISPs. This
property is shown at the top of Table 7. Our initial assumption was that this
property only depends on prefix filtering done by the outbound filters on the
border routers, so we provided the network invariants shown in the middle of
the table. However, Lightyear produced counterexamples for the local checks on
the edges from the border routers to the ISPs, since the outbound filters
allow advertisements for other prefixes as long as they are tagged with the
well-known blackhole community [19], which tells the ISPs to blackhole that
traffic. However, by inspection we found that this mechanism was not being
used currently — the blackhole community is not added to any announcements.
Hence we were able to still prove the desired end-to-end property, using the
refined set of invariants shown at the bottom of Table 7, where SComms
represents the set of blackhole communities.

To demonstrate our approach’s utility in error localization, we used Lightyear
again after injecting three errors into the configurations:  (1) adding a
policy that attaches the blackhole community  (2) changing a policy from
removing communities to propagating them, and  (3) changing the filter at the
border router to allow a non-university address block.  Each of these errors
causes the local checks to fail for the edges using the erroneous routing
policy. Further, the counterexample provided by Lightyear for each error
provides the relevant information to understand the error, such as the prefix
being advertised and whether communities are being added or propagated. For
example, the first error causes the local check to fail because we cannot
prove that $\textrm{Comm}(r)\ \cap\textsc{ SComms}=\emptyset$ for all routes
$r$ that pass the filter, and the counterexample route includes the blackhole
community.

Type | Locations ($l$) | Logical Formula ($I_{l}$) |  Description
---|---|---|---
End-to-end Property |  Edges to ISP R $\rightarrow$ P | $\textsc{Prefix}(r)\in\textsc{UniPrefixes}$ |  University routers only send prefixes for its owned address blocks
Initial Network Invariants |  Edges to ISP R $\rightarrow$ P | $\textsc{Prefix}(r)\in\textsc{UniPrefixes}$ |  University routers only send prefixes for its owned address blocks
Other | True |  Other locations are unconstrained
Refined Network Invariants |  Edges to ISP R $\rightarrow$ P | $\textsc{Prefix}(r)\in\textsc{UniPrefixes}$ |  University routers only send prefixes for its owned address blocks
Edges from external $P\rightarrow R$ | True |  Routes from external neighbors are unconstrained
Other | $\textrm{Comm}(r)\ \cap\textsc{ SComms}=\emptyset$ |  Routes at other locations inside network are not tagged with specific communities
Table 7: The end-to-end property and network invariants needed to verify that
the university only advertises its own aggregated networks. Both the initial
guess and the refined invariants are shown.

##  7 Related Work

Control Plane Verification: The state-of-the-art approaches to network
control-plane verification were summarized earlier in Table 1. Unlike
Lightyear, these approaches are all monolithic — they require joint analysis
of the configurations of all nodes in the network — which dramatically limits
scalability. Most approaches therefore make tradeoffs in expressiveness, for
example giving up the ability to reason about all possible BGP announcements
from neighbors [11, 24, 1, 29]. In contrast, Lightyear’s modular approach only
requires reasoning about individual BGP route maps in isolation and so is
highly scalable. Lightyear also provides guarantees across all possible
external announcements and all failures. The tradeoff is that Lightyear
supports a more limited set of properties than prior approaches — safety
properties that hold of all routes that can reach a particular location — and
requires the user to specify local invariants.

Closest to our work is a recent technique for modular control-plane
verification called Kirigami [25]. Like our work, the approach provides a form
of assume-guarantee reasoning for the control plane using local invariants.
However, Kirigami makes a different set of tradeoffs than Lightyear, leading
to different strengths and weaknesses. Kirigami’s local invariants consist of
information about the exact routes that will arrive on a particular edge.
Because these invariants are fully concrete, Kirigami cannot reason about
arbitrary route announcements from neighbors, which is necessary for the
properties that Lightyear targets, for example no-transit properties. Kirigami
also does not reason about failures. On the other hand, Kirigami can verify
safety properties that Lightyear cannot, for example verifying the exact
number of hops that routes will take. Further, Kirigami is designed and
implemented on top of a generic control-plane representation [12] and so is
not restricted to checking BGP policies.

Another line of work has improved scalability of control-plane verification
through forms of abstraction [5, 6]. In these approaches, the full network is
still analyzed monolithically, but irrelevant or redundant configuration
information is abstracted away in order to simplify the analysis. Our work on
modularity is orthogonal to this line of work and in the future could be
potentially combined with it.

Data Plane Verification: Another class of network verification tools check
properties of the forwarding state of the network, rather than of the network
configurations [21, 17, 18, 27, 15, 2, 20]. These approaches also generally
require joint reasoning about the entire network forwarding state as a whole.
A recent exception is RCDC [14], which modularly verifies global reachability
contracts in a data center via local checks. However, the approach is specific
to the data center design and does not provide a general framework for
decomposing global property checks into local checks. There has also been work
on exploiting forms of abstraction, such as symmetries, to scale data-plane
verification [22].

Modular Verification: Assume-guarantee reasoning [16, 23] is the foundation
for modular verification in other domains, including hardware and software
verification. In this style, a global property is modularized by providing
each system component with local invariants that it must satisfy, under the
assumption that the other components satisfy their invariants. Lightyear
directly applies this methodology in order to generate the local checks that
each BGP policy must satisfy, and we have proven that our approach is sound.

Verification commonly requires the identification of _inductive invariants_ ,
properties that hold over some unbounded space of system states. For example,
reasoning about loops in traditional software requires the identification of a
_loop invariant_ that summarizes the behavior of the loop no matter how many
times it is executed [13]. Though our approach does not specifically require
such invariants, we have found that they arise naturally and enable the use of
the same local invariant for almost all network locations. In particular,
typically one or a small set of nodes establishes an inductive invariant (e.g
by attaching a community to certain routes), and then this invariant holds
throughout the network as long as the other nodes “do no harm” (e.g. they
never remove communities).

##  8 Conclusion

In this paper, we have described a modular approach to BGP control-plane
verification. In this approach, users provide not only an end-to-end property
to verify but also local network invariants on individual routers and edges.
Our tool Lightyear then derives a set of local checks that validate these
invariants and ensure that they imply the global property. We have proven the
approach correct, and we have shown that Lightyear can scale to very large
networks, including the wide-area network of a major cloud provider.

There are a number of avenues for future work. First, many optimizations are
possible, notably the use of parallelism to perform many local checks
simultaneously. Second, Lightyear currently only supports safety properties;
we believe that the underlying ideas can be extended to support modular
verification of liveness properties (e.g., reachability). Third, currently
Lightyear users must provide the per-location invariants that are used to
derive the local checks. We believe that it is possible to instead _learn_
these local invariants automatically in many common cases, for example when
properties are enforced via communities.

## References

  * [1] 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, Santa Clara, CA, February 2020. USENIX Association.
  * [2] Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker.  Netkat: Semantic foundations for networks.  In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, page 113–126, New York, NY, USA, 2014. Association for Computing Machinery.
  * [3] Batfish.  https://github.com/batfish/batfish.
  * [4] 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, SIGCOMM ’17, page 155–168, New York, NY, USA, 2017. Association for Computing Machinery.
  * [5] 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, SIGCOMM ’18, page 476–489, New York, NY, USA, 2018. Association for Computing Machinery.
  * [6] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker.  Abstract interpretation of distributed network control planes.  Proc. ACM Program. Lang., 4(POPL), dec 2019.
  * [7] Leonardo de Moura and Nikolaj Bjørner.  Z3: An efficient smt solver.  In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
  * [8] Benoit Donnet and Olivier Bonaventure.  On bgp communities.  SIGCOMM Comput. Commun. Rev., 38(2):55–59, mar 2008.
  * [9] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich.  The spirit of ghost code.  Formal Methods in System Design, 48(3):152–174, 2016.
  * [10] Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, 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, Oakland, CA, May 2015. USENIX Association.
  * [11] 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, SIGCOMM ’16, pages 300–313, New York, NY, USA, 2016. ACM.
  * [12] Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker.  NV: an intermediate language for verification of network control planes.  In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 958–973. ACM, 2020.
  * [13] Charles Antony Richard Hoare.  An axiomatic basis for computer programming.  Communications of the ACM, 12(10):576–580, 1969.
  * [14] 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.
  * [15] Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, and Charlie Kaufman.  Automated analysis and debugging of network connectivity policies.  Technical Report MSR-TR-2014-102, Microsoft, July 2014.
  * [16] C. B. Jones.  Specification and design of (parallel) programs.  In R. E. A. Manson, editor, Proceedings of IFIP ’83, pages 321–332. IFIP, North-Holland, 1983.
  * [17] Peyman Kazemian, George Varghese, and Nick McKeown.  Header space analysis: Static checking for networks.  In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, NSDI’12, pages 9–9, Berkeley, CA, USA, 2012. USENIX Association.
  * [18] Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey.  Veriflow: Verifying network-wide invariants in real time.  SIGCOMM Comput. Commun. Rev., 42(4):467–472, September 2012.
  * [19] Thomas King, Christoph Dietzel, Job Snijders, Gert Döring, and Greg Hankins.  BLACKHOLE Community.  RFC 7999, October 2016.
  * [20] 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, Oakland, CA, 2015. USENIX Association.
  * [21] 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\.
  * [22] Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese.  Scaling network verification using symmetry and surgery.  In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 69–83. ACM, 2016.
  * [23] Amir Pnueli.  In transition from global to modular temporal reasoning about programs.  In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 123–144. Springer, 1984.
  * [24] Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar.  Plankton: Scalable network configuration verification through model checking.  2020\.
  * [25] Tim Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker.  Kirigami, the verifiable art of network cutting, 2022.
  * [26] 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.  SIGPLAN Not., 51(10):765–780, October 2016.
  * [27] Hongkun Yang and Simon S Lam.  Real-time verification of network properties using atomic predicates.  IEEE/ACM Transactions on Networking, 24(2):887–900, 2015.
  * [28] Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca.  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, SIGCOMM ’20, page 599–614. Association for Computing Machinery, 2020.
  * [29] Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca.  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, SIGCOMM ’20, page 599–614, New York, NY, USA, 2020. Association for Computing Machinery.