A Systematic Approach to
BGP Configuration Checking
Nick Feamster and Hari Balakrishnan
M.I.T. Computer Science and Artificial Intelligence Laboratory
BGP Configuration Determines Its Behavior
Route injection, redistribution, aggregation
Import and export route maps
Access control lists, filtering
AS Path prepending
Route flap damping
BGP is a distributed program.
We need practical verification techniques.
Today: Stimulus-response Reasoning
"What happens if I tweak this import policy?"
"Let’s just readjust this IGP weight..."
"New customer attachment point? Some cut-and-paste will fix that!"
Some time later, some "strange behavior" appears.
Operators have a terrible "programming environment".
Configuration is ad hoc and painful.
Wastes operator time.
Suboptimal performance, angry customers.
Online error checking is insufficient.
Won’t catch misconfigured filters, redundant route reflectors, etc.
Verifying Configuration "Correctness"
Why? Unlike most protocols, BGP’s correctness
depends heavily on how it is configured.
How? Systematically, according to properties:
enumerate aspects of configuration that affect it
test that those aspects conform to certain rules
Limitations? Some aspects involve cooperation across
ASes; not really possible today.
That’s OK, plenty goes wrong inside of one AS, too.
Higher Level Reasoning About Configuration
Verify the behavior of a particular configuration.
Check "correctness properties".
Check that the configuration conforms to intended behavior.
More than a band-aid fix.
Useful for any router configuration language.
Specify configuration based on inte