Workshop on Internet Routing Evolution and Design, October 2003
Rethinking Routing Configuration: Beyond Stimulus-Response Reasoning
Nick Feamster
BGP Configuration Today
BGP-speaking routers make routing decisions and propagate routing messages based on local configura-
tion in the hope that the resulting path assignments will provide stable, global connectivity. BGP routing
involves local decisions made by routers based on flexible policies, which means that BGP’s behavior is
largely defined by its configuration. Controlling BGP’s behavior by manipulating router configuration is a
double-edged sword: its flexibility allows operators to use BGP to accomplish a wide range of tasks, but it
also means that misconfigurations can, and do, cause significant problems. Even one misconfiguration can
cause a complex sequence of errors that adversely affect global connectivity and are difficult to debug.
Today, network operators, protocol designers, and researchers typically reason about BGP’s behavior
by observing the effects of a particular configuration on a live network. The state-of-the-art for router
configuration typically involves logging configuration changes and rolling back to a previous version when a
problem arises. The lack of a formal reasoning framework means that router configuration is time-consuming
and ad hoc. Furthermore, today’s routing configuration is based on the manipulation of low-level mechanisms
(e.g., access control lists, import and export filters, etc.), which makes routing configuration tedious, error-
prone, and difficult to reason about.
Network operators need tools based on systematic verification techniques to ensure that BGP’s operational
behavior is consistent with the intended behavior (i.e., that the network is operating “correctly”). We propose
a verification tool based on a new reasoning framework that helps operators and protocol designers reason
about high-level properties of routing protocols. Eventually, routing configuration should be based on design
patterns that facilitate high-level tasks by more accurately specifying the operator’s intent. Understanding
what high-level properties should be checked in today’s configuration will help us move in that direction.
A New Reasoning Framework
We previously proposed that routing protocols be classified in terms of the following properties:
• Validity. The existence of a route to a destination implies that a packet sent along the corresponding
path will reach its intended destination.
• Visibility. The existence of a valid path to a destination from some origin implies that the origin knows
about a route for that path.
• Safety. Given a set of routes and policies, a route assignment exists such that no participant wants to
change its route in response to other participants’ routes (Griffin et al.’s Stable Paths Problem).
• Determinism. Given a set of possible routes and a set of policies, the routing protocol should always
converge to the same predictable set of routes.
• Information-Flow Control. Routing messages should not expose more information than is necessary to
achieve the above requirements, subject to some information flow policy.
For each property, we define rules that, if satisfied, imply that the property is satisfied. We call this set
of properties, together with the rules to reason about them, the routing logic. The routing logic facilitates
a more effective approach to verifying routing protocol configuration. Thinking about BGP’s behavior in
terms of the routing logic allows us to identify the ways that configuration affects each of these properties
and to express the constraints that are sufficient to guarantee that these properties are satisfied.
Routing Configuration in the Future: Systematic, Verifiable, Simple
Because BGP’s correctness depends almost entirely on how it is configured, network engineers need a
thorough, methodical process for verifying that a candidate router configuration will behave correctly, before
deploying that configuration on a live network. We propose a systematic approach to configuration checking
that is based on verifying conformance to the high-level properties of the routing logic. For each property, we
determine the aspects of configuration that affect these high-level properties and define specific constraints
that can be checked against router configuration using static analysis techniques.