Rethinking routing configuration: Beyond stimulus-response reasoning

Abstract

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. We propose a set of rules, called the routing logic, which can be used to determine whether a routing protocol satisfies various properties. Network operators need tools based on systematic fault detection techniques to ensure that BGP's operational behavior is consistent with the intended behavior (i.e., that the network is operating ``correctly''). We are designing a verification tool based on a new reasoning framework that helps operators and protocol designers reason about high-level properties of routing protocols.