Nick Feamster

Practical Correctness Verification for Wide-area Internet Routing

Several studies have shown that wide-area Internet routing is fragile,
with failures occurring for a variety of reasons. Routing fragility
is largely due to the flexible and powerful ways in which BGP can be
configured to perform various tasks, which range from
implementing the policies of commercial relationships to configuring
backup paths. Configuring routers in an AS is like writing a distributed
program, and BGP's flexible configuration and today's relatively
low-level configuration languages make the process error-prone. The
primary method used by operators to determine whether their complex
configurations are correct is to try them out in operation.

We believe that there is a need for a systematic approach to verifying
router configurations before they are deployed. This paper develops a
static analysis framework for configuration checking, and uses it in the
design of "rcc", a "router configuration checker". rcc takes as
input a set of router configurations and flags anomalies and errors,
based on a set of well-defined correctness conditions. We have used rcc
to check BGP configurations from 9 operational networks, testing nearly
700 real-world router configurations in the process. Every network we
analyzed had configuration errors, some of which were potentially
serious and had previously gone unnoticed. Our analysis framework and
results also suggest ways in which BGP and configuration languages
should be improved. rcc has also been downloaded by 30 network
operators to date.