Reasoning about BGP's Behavior


The routing logic rules can be used to 
prove theorems about these properties.

Verifying that an arbitrary route reflector configuration satisfies validity is NP-complete. 

Route reflectors that re-advertise all eBGP-learned routes will satisfy validity. 

Certain fixes to other problems (e.g., safety) can violate information-flow policy.