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

TL;DR

FixRoute introduces a hybrid logical and numerical approach for analyzing and ensuring safe, optimal, and resilient Internet traffic routing, specifically addressing BGP protocol configurations and convergence issues.

Contribution

It combines logical satisfiability with numerical optimization to analyze network parameters, enabling faster and more flexible traffic engineering solutions.

Findings

Faster than purely logical or numerical methods

Able to analyze parameter sensitivity and trade-offs

Supports resilience assessment to network failures

Abstract

The performance of networks that use the Internet Protocol 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 {\em logical} satisfiability criteria with traditional {\em 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, trade-offs 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.