Several recent studies have indicated that human configuration error is a leading cause of network downtime. Network operators need better verification techniques to ensure that routers are configured correctly. Distributed dependencies in wide-area routing cause small configuration mistakes or oversights to spur complex errors, which sometimes have devastating effects on global connectivity. These errors are often difficult to debug because they are sometimes only exposed by a specific message arrival pattern or failure scenario.

The state-of-the art for router configuration checking typically consists of logging changes to the configuration and rolling back to a previous version in the event that a problem should arise. This approach is inadequate because (1) it assumes that the previous configuration was correct in the first place and (2) it relies on the coincidence of configuration change and the appearance of an anomaly, rather than a systematic cause-and-effect analysis. In an effort to develop more systematic techniques for validating BGP configuration, we propose a systematic approach to configuration checking that is based on verifying conformance to the following set of high-level properties:

• Validity: Are bogus paths being advertised?
• Visibility: Is BGP advertising every path that it should be?
• Safety: Will BGP converge to a unique, stable answer?
• Determinism: Do the best routes that BGP selects depend on the order in which routing messages arrive?
• Information-flow control: Is BGP leaking "private" information to other ASes?

We present a tool that network operators can use to test BGP configuration for some common, elusive, and catastrophic errors. The tool checks configuration on an AS-wide level against a set of rules. These rules statically analyze the router configuration files and verify that specific constraints are satisfied. While the rules that the tool tests are by no means exhaustive, we have designed our tool in a way that allows for easy extensibility. We hope that the NANOG community will apply the tool to their own configuration files and suggest new rules and features that should be incorporated.

While static analysis can catch many configuration errors, simulation and emulation are typically necessary to determine the precise scenarios that could expose runtime errors. Based on these observations, we propose the design of a BGP verification tool that uses a combination of static and dynamic analysis, present examples where it could be applied in practice, and describe future research challenges.

About the Presenters
Nick Feamster is a graduate student in the Networks and Mobile Systems group at the MIT's Computer Science and Artificial Intelligence Laboratory (formerly LCS) under the supervision of Professor Hari Balakrishnan. He is interested in wide-area networking, network measurement, and security. His current research focuses on verification techniques for BGP and interdomain traffic engineering. He is an NSF Graduate Research Fellow and the recipient of the Best Student Paper awards at the USENIX Security Symposium in 2001 and 2002. Nick received his S.B. and M.Eng. degrees in Electrical Engineering and Computer Science from MIT in 2000 and 2001, respectively.