Towards a Logic for Wide›Area Internet Routing
Nick Feamster and Hari Balakrishnan
MIT Laboratory for Computer Science
200 Technology Square, Cambridge, MA 02139
{feamster,hari}@lcs.mit.edu
Abstract
Interdomain routing is a massive distributed computing task that
propagates topological information for global reachability. Today’s
interdomain routing protocol, BGP4, is exceedingly complex be-
cause the wide variety of goals that it must meet including fast
convergence, failure resilience, scalability, policy expression, and
global reachability are accomplished by mechanisms that have
complicated interactions and unintended side effects. The com-
plexity of wide-area routing con guration and protocol dynamics
requires mechanisms for expressing wide-area routing that adhere
to a set of logical rules. We propose a set of rules, called the routing
logic, which can be used to determine whether a routing protocol
satis es various properties. We demonstrate how this logic can aid
in analyzing the behavior of BGP4 under various con gurations.
We also speculate on how the logic can be used to analyze exist-
ing con guration in real-world networks, synthesize network-wide
router con guration from a high-level policy language, and assist
protocol designers in reasoning about new routing protocols.
Categories and Subject Descriptors
C.2.2 [Computer-Communication Networks]: Routing proto-
cols, Protocol veri cation
General Terms
Design, Performance, Reliability
1. Motivation
Interdomain routing on the Internet is staggeringly complex.
Routers on the Internet participate in a massive distributed com-
puting task that propagates topological information for path selec-
tion. The complexity of the task results from the many distinct
goals that must be met: fast convergence to correct loop-free paths
to all destinations under static and dynamic conditions; resilience
to congestion, packet loss, and failures; scaling to large numbers
of networks and end hosts; and, above all, providing global con-
nectivity among autonomous, nancially competing and mutually
distrusting domains.
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
ACM SIGCOMM 2003 Workshops, August 25&27, 2003, Karlsruhe, Ger›
many.
Copyright 2003 ACM 1›58113›748›6/03/0008 ...$5.00.
BGP’s complexity stems not from its deceptively simple spec-
i cation [35], but rather from its dynamic behavior during opera-
tion, as well as the vast possibilities for con guration. Prior work
has highlighted many aspects of wide-area routing that result in the
following complex, unexpected, or undesirable properties:
• Poor integrity. BGP is vulnerable to masquerading, denial of
service, and data integrity attacks [5] and is also subject to
frequent miscon guration [29].
• Slow convergence. Path instability commonly results in de-
layed convergence [27], which is often slowed further by the
unintended side effects of other performance tweaks, such as
route ap dampening [30]. BGP’s performance under con-
gestion or routing instability is not well-understood.
• Divergence. BGP’s policy-based nature can give rise to con-
gurations that are guaranteed to diverge [20].
• Unpredictability. Because of the distributed, asynchronous
nature of BGP, precisely predicting the effects of a con gu-
ration change is extremely challenging [14].
• Poor control of information ow. Certain routing policies
or BGP implementations may expose information that is not
intended to be public knowledge, such as peering and tran-
sit relationships. For example, BGP routing messages ex-
pose information about topology and hierarchical relation-
ships among Internet service providers [15].
The complexity of routing con guration and protocol dynamics
mandates a mechanism for understanding and manipulating Inter-
net routing at a higher level of abstraction. We believe that the
time is ripe for a reconsideration of the current approach to inter-
domain routing, based on a more formal approach to the problem
and building on our experience as a community with BGP4 over
the past several years.
Previous work in wide-area protocol design has focused on spe-
ci c modi cations to BGP that x a particular problem but often
spur unintended negative side effects. Furthermore, designers of
new wide-area routing protocols require a mechanism that enables
them to reason about the circumstances under which the protocol
will behave correctly. To help reason about modi cations to ex-
isting routing protocols and to aid in the sound design of new ones
in the future, we propose that routing protocols be classi ed in
terms of the following properties, each of which expresses an im-
portant aspect of wide-area routing:
• Validity. The existence of a route to a destination implies that
a packet sent along the corresponding path will eventually
reach the intended destination.
Proceedings ot the ACM SIGCOMM 2003 Workshops 289 August 2003

• Visibility. The existence of a path to a destination from some
origin implies that that origin knows about a corresponding
route to the destination.
• Safety. Given a set of routes and a set of policies, an as-
signment of routes must exist such that no participant wants
to change its route in response to other participants’ routes
(Grif n and Wilfong’s Stable Paths Problem and General
Stable Paths Problem [20, 22]).
• Determinism. Given a set of possible routes and a set of poli-
cies, the routing protocol should always arrive at the same
predictable set of routes. This set of routes should be inde-
pendent of the order in which the possible routes arrive.
• Information- ow control. Routing messages should not ex-
pose more information than is necessary to achieve the above
requirements, subject to some information ow speci cation,
such as noninterference [17].1
For each property, we formally de ne a minimal set of rules that,
if satis ed, imply that the property is satis ed. We call this set
of rules, together with the logic to reason about them, the rout-
ing logic. The routing logic helps protocol designers reason about
new routing protocols and prove statements about modi cations to
existing ones. Our goal is to improve our understanding of the be-
havior of complex protocols using better tools than we currently
have.
This set of rules is by no means complete; indeed, we do not
consider issues like scalability or the ability to perform traf c load
balancing via traf c engineering. However, the logic can be used
to determine if any techniques used to achieve these goals affect
the chosen properties. We stress that the logic is a set of rules for
reasoning about properties of routing protocols, as opposed to a
speci cation of requirements. It may be possible (and even reason-
able) for a protocol to violate one or more of these properties under
certain circumstances; the logic simply provides a framework for
reasoning about when these violations arise.
As a simple example, observe that validity requires that some
route advertisement imply reachability to a superset of that destina-
tion. A protocol violates this property when a route advertisement
exists for a destination that is not reachable. One example of such
a violation is delayed convergence; another is the unreachability of
a subnet within an aggregated pre x.
We highlight how the routing logic can be used to reason about
both BGP con guration, as well as proposed modi cations to BGP
itself. We show that verifying that an arbitrary route re ector con-
guration satis es validity is NP-complete, and that several simple
protocol modi cations can guarantee route validity under certain
circumstances. We use the routing logic to analyze several pro-
posed modi cations to BGP; for example, we show that the Safe
Path Vector Protocol [21] modi cations to BGP improve safety but
can violate information ow policies.
BGP’s design and implementation makes reasoning about vari-
ous properties surprisingly dif cult. We show that BGP’s depen-
dence on other routing protocols such as IGP and its inability to
check route advertisements for consistency makes the protocol very
dif cult to reason about. In response, we propose that an alternative
architecture based on the routing logic may be able to circumvent
some of these problems.
Previous work has focused on speci c problems with BGP, with-
out considering broader implications or fundamental problems. In
1Noninterference requires that information (e.g., routing messages, peering
and transit relationships) at a particular security level does not affect how
the routing protocol is observed by entities at a lower security level. We
describe this further in Section 2.4.
this paper, we present a logic that concisely describes fundamental
problems in wide-area routing and provides insights for consider-
ing wide-area routing at a higher level of abstraction. We believe
this logic can enable con guration analysis to catch mistakes and
verify that certain properties are satis ed.
While this paper primarily focuses on the potential for the rout-
ing logic as an analysis tool, we also speculate on the potential
uses of the logic for synthesis of BGP con guration and new pro-
tocol designs. We believe that the logic can be used a framework
for high-level policy speci cation that preserves the semantics of
low-level con guration but has veri able properties. Additionally,
incorporating insights from the logic into routing protocol design
can speed convergence, detect routing pathologies more quickly,
enforce information ow control, and facilitate the design of wide-
area routing protocols that conform to high-level speci cations.
2. A Routing Logic
The routing logic presented in this section is a set of rules that
facilitates reasoning about whether, and under what circumstances,
a routing protocol satis es a particular property. While we believe
that the logic can be used to understand other types of routing pro-
tocols (e.g., for mobility, etc.), we limit our focus to interdomain
routing. We also examine the properties of the routing logic in the
context of BGP.
2.1 Overview and De nitions
After providing a brief overview of the routing logic, we present
the terminology for the logic and introduce the concept of hierar-
chical routing scopes.
2.1.1 Overview
The routing logic allows network operators and protocol design-
ers to reason about properties of routing protocols. To determine
whether a routing protocol satis es a particular property, the rout-
ing logic requires the following inputs: (1) a speci cation of how
the protocol behaves and (2) a speci cation of the protocol con-
guration. Protocol con guration entails both policy con guration
(i.e., which routes are preferred over others) and general con g-
uration, such as which routers exchange routing information with
each other. The routing logic then determines whether the routing
protocol satis es the conditions associated with that rule.
We also believe that the logic will be useful for automated con-
guration analysis and generation; we explore these possibilities in
Section 4. However, this type of automated reasoning requires ei-
ther a thorough abstract speci cation of BGP’s operation or a set
of suf cient conditions that can be more easily tested than the rules
themselves. Given the complex operations and dynamics of BGP,
the most immediate bene t of the logic is providing a framework
for deriving and reasoning about these suf cient conditions, as we
demonstrate in Section 3. However, as we discuss in Section 4,
alternative protocol designs (including simpli ed versions of BGP
itself) may lend themselves to automated analysis more easily.
Our current version of the routing logic does not incorporate any
notion of time. Because any distributed routing protocol will have
invalid routes while in a transient state, it would seem that the rules
for validity and visibility require a temporal dimension. However,
as we will discuss in Section 2.2, the validity rule highlights the
propagation of invalid routes (e.g., during path exploration), rather
than simply the existence of invalid routes in the system during
transient states (as might happen in OSPF during ooding and dis-
tributed shortest paths computation). Similarly, we apply the visi-
bility rule to examples of BGP in the steady-state. While including
time in the routing logic could facilitate reasoning about some rout-
Proceedings ot the ACM SIGCOMM 2003 Workshops 290 August 2003