A Unified Logic and Numerical Tool for Provably Safe Internet Traffic Engineering

FixRoute and RouteShepherd

Abstract

The performance of networks that use the Internet Protocol stack is sensitive to precise configuration of many low level parameters on each network device. These settings govern the action of dynamic routing protocols, which direct the flow of traffic; in order to ensure that these dynamic protocols all converge to produce some ’optimal’ flow, each parameter must be set correctly. Multiple conflicting optimization objectives, nondeterminism, and the need to reason about different failure scenarios make the task particularly complicated. We present a fast and flexible approach for the analysis of a number of such management tasks presented in the context of BGP routing. The idea is to combine logical satisfiability criteria with traditional numerical optimization, to reach a desired traffic flow outcome subject to given constraints on the routing process. The method can then be used to probe parameter sensitivity, tradeoffs in the selection of optimization goals, resilience to failure, and so forth. The theory is underpinned by a rigorous abstraction of the convergence of distributed asynchronous message-passing protocols, and is therefore generalizable to other scenarios. Our resulting hybrid engine is faster than either purely logical or purely numeric alternatives, making it potentially feasible for interactive production use.

Contributions

FixRoute provides a means for assessing tradeoffs between different objectives in network management. Previous attempts at automating management tasks have sought to incorporate many objectives into a fixed strategy. The problem with this approach is that it does not match the typical modes by which networks are actually managed, where the tradeoffs are contextual, and it may be difficult to express a single strategy that encompasses all needs. It is not feasible to ask a network operator to use a system where the first step is to write a complex optimization formula, even if we can then solve it exactly. In contrast, our approach enables operators to experiment with the interplay of these objectives, within a sound conceptual design underpinned by a proven mathematical formalism.

Publications

People

Portrait of Behnaz Arzani

Behnaz Arzani

Principal Researcher