Correctness Properties for Internet Routing∗
Nick Feamster Hari Balakrishnan
College of Computing Computer Science & AI Lab
Georgia Tech MIT
feamster@cc.gatech.edu hari@csail.mit.edu
Abstract
This paper motivates and presents a correctness specifi-
cation for Internet routing. This specification is based
on three properties—route validity, path visibility, and
safety. This specification may be of use to people de-
veloping tools to check routing configurations, to people
designing solutions to specific problems in the current sys-
tem, and to designers of new protocols and routing archi-
tectures, all of whom can benefit from knowing what it
means for Internet routing to be “correct”.
1 Introduction
Today’s Internet routing infrastructure is unacceptably
fragile. Among its shortcomings, it converges slowly [17]
(and sometimes not at all [14]); it is often misconfig-
ured [8, 18]; it is hard to control and predict [10]; and
it has weak security properties [22]. This fragility causes
communication on the Internet to be unreliable and un-
predictable.
Two important design goals for Internet routing, pol-
icy expressiveness and scalability, lead to this fragility.
Each goal is important because Internet service is not
the purview of a single administrative entity. Rather,
the Internet is composed of thousands of independently
operated networks that often compete with one another
for customers but must nonetheless cooperate to offer
global connectivity to hundreds of millions of hosts. This
“competitive cooperation” requires the ability to express
routing policy, which dictates which routes are advertised
to which neighbors, and which paths are used to send
packets to any given destination. The Internet’s scale (in
terms of number of total hosts, number of independently
operated networks, and the size of any given network)
requires that the Internet’s routing protocols also incor-
porate various scaling techniques.
In practice, multiple routing protocols are used to
achieve these goals. First, the Border Gateway Proto-
col (BGP) [24, 25], which is used in two different modes:
a network’s egress (or “border”) routers use external BGP
(eBGP) to exchange routes for external destinations (i.e.,
∗This research is supported in part by the National Science Foun-
dation under grants 0520241 and 0225660, and by a grant from
Cisco Corporation. The views expressed in this paper are not nec-
essarily those of these organizations.
those that are not contained within the current network)
with neighboring networks; internal BGP (iBGP) is used
to disseminate these routes within any given network.
Second, interior routing protocols (also called interior
gateway protocols, or IGPs) exchange routes for inter-
nal destinations. BGP route selection determines which
egress router each router sends traffic to. The IGP is then
responsible for determining the internal route from that
router to the appropriate egress router.
These two classes of routing protocols facilitate both
complex policy expression and scalability, but they also
interact with each other in unexpected and undesirable
ways. These interactions make reasoning about the be-
havior of the Internet routing system difficult. The lack
of any formal reasoning framework leads to ad hoc fixes to
observed problems that ultimately only worsen this com-
plexity. Today, network operators (who continually tweak
routing configuration and handle problems reactively af-
ter they occur) and protocol designers (who repeatedly
propose “point” solutions to various problems) have no
way of reasoning about whether their modifications to
Internet routing will operate as intended.
There are several possible ways to improve this situ-
ation, including fixing problems in the current architec-
ture, improving the ways in which current networks are
operated, and designing a more robust architecture for
the future. In all cases, however, we need a specification
of what it means for Internet routing to be “correct”, and
on ways to tell if the routing system is performing incor-
rectly or poorly. This paper presents three fundamental
correctness properties and defines them formally, with a
view toward developing a high-level correctness specifica-
tion for large-scale Internet routing.
Using the formal specification of these properties, we
derive various constraints that today’s Internet routing
protocols must satisfy to prevent these properties from
being violated. While, in this paper, we apply our correct-
ness specification undesirable interactions between iBGP
and IGP, we intend the specification to be useful for an-
alyzing any complex interactions that arise in scalable,
policy-based routing. Due to space limitations, we have
omitted proofs in this paper; proofs, as well as more de-
tailed discussions, are available in [7].
Our proposal for a routing specification is based on the
following properties:
1. Route validity, which states that if a router has a
1

route to a destination, then a usable path corre-
sponding to that route exists in the underlying topol-
ogy. If route validity is violated, then end users
could experience a failure of end-to-end connectiv-
ity, because routers could forward packets along non-
existent paths.
2. Path visibility, which states that if there is a usable
path between two nodes, then the routing protocol
will propagate information about that path. A fail-
ure of path visibility could disrupt end-to-end com-
munication by preventing two connected nodes from
learning routes between one another.
3. Safety, which states that the routing protocol con-
verges to a stable route assignment, regardless of
the order in which routing messages are exchanged.
A routing protocol that violates safety will induce
persistent route oscillations, causing routing changes
that are unrelated to changes in topology or policy.
This paper defines and investigates these properties and
demonstrates how they can deepen our understanding of
network routing. This correctness specification addresses
static properties of network routing, not dynamic behav-
ior (i.e., its response to changing inputs, convergence
time, etc.). Internet routing, like any distributed pro-
tocol, may experience periods of transient incorrectness
in response to changing inputs, but we are concerned with
persistent misbehavior.
2 Preliminaries
Before introducing the correctness properties themselves,
we first introduce some basic terminology for routing. We
explain these terms in the context of Internet routing and
BGP. We first define paths and routes in terms of a graph
G = (V,E), where the nodes in V = {v1, . . . , vN} corre-
spond to IP-level nodes (i.e., routers and end hosts) and
the edges in E corresponds to IP-level links between those
nodes.
2.1 Paths and Routes
We now define two basic terms—path and route—and
explain how they are related.
Definition 2.1 (Path) A path is a sequence of nodes
P = (v0, . . . , vn), where vi ∈ G for all 0 ≤ i ≤ n.
The definition of a path does not constrain how the se-
quence of nodes is actually constructed. As such, a path
might represent a sequence of directly connected IP-layer
nodes or endpoints of a tunnel.1 Note that deleting some
nodes from a path still results in a path.
1A tunnel is a sequence of nodes that all forward packets to
some intermediate node (i.e., the tunnel’s “exit”), rather than the
ultimate destination. A tunnel may be implemented by a variety
of mechanisms, such as IP-in-IP encapsulation [6], Multiprotocol
Label Switching (MPLS) [4, 21], etc.
In contrast to a path, a route is information that al-
lows nodes in G to construct paths to destinations. The
destination d may refer either to a single node or a group
of nodes (named, for example, by an IP prefix). The
purpose of a routing protocol is to propagate routes for
destinations. Collectively, the routes to d that the nodes
in G ultimately select define the path from any node in G
to that destination. All of our definitions presume that
the handle for a destination, d, cannot be manipulated
(e.g., our definitions do not consider the effects of IP pre-
fix aggregation [13, 23]).
Definition 2.2 (Route) A route is a mapping (d →
vi), where d is a destination, and vi ∈ G is a node en
route to the destination d.
We say that vi ∈ d if the destination d includes vi. A route
(d → vi) received by vj indicates that, if vj has a packet
to send to some node at destination d, it can forward
that packet to vi, which in turn ought to have a route to
d (whereupon this process repeats until the data reaches
d). One can think of a route (d → vi) being used at node
vj as inducing a path, (vj , . . . , vi), where either vj and
vi are directly connected or where the actual nodes along
that path segment are determined by the connectivity
between those nodes, as established by the IGP or using
tunnels. We will formalize the notion of induced paths in
Section 2.2.
Note that Definition 2.2 can apply to any routing pro-
tocol, not just to BGP. In an IGP, the node vi is typically
the router that is immediately connected at the IP layer.
In BGP, however, (particularly in iBGP) the next hop
may be several IP-layer hops away. In BGP, a node that
receives a route (d → v) but is not directly connected to
v must rely on the IGP for reachability to v.
2.2 Induced Paths
We can think of paths as being induced by routes. That
is, while there exist many sequences of nodes between
any node v0 and a node in some destination d, the path
that traffic will actually take from v0 en route to d is de-
termined by the routes that the nodes in G select. In
many routing protocols, including BGP, no single node
has knowledge about the entire sequence of nodes that
traffic traverses en route to d; rather, the nodes that the
routes select collectively induce a path to d. We are in-
terested in making statements about those induced paths.
We now formalize the concept of induced paths and de-
scribe a special class of induced paths called consistent
paths.
Definition 2.3 (Induced path) Let rvj (d) be the route
that node vj selects en route to d (i.e., it is a mapping
(d → vk) for some other vk ∈ G. Then, the path induced
by route rv0(d) : (d → vi), Pv0(rv0 (d)), is:
Pv0(rv0 (d)) =



φ if v0 has no route to d
v0 if v0 ∈ d
(v0, Pv1(rv1 (d))) otherwise
2