When static verification is not enough: revealing BGP bugs at runtime
Operators go to great lengths to ensure their BGP networks are correct. Yet, despite their efforts, faults still happen due to software or hardware bugs which can often have detrimental network-wide consequences. Today, all operators can do is react to such failures, often only once it is already too late. We present GhostBuster, a runtime system which monitors the execution of BGP routers and verifies their compliance with the protocol specification. Concretely, GhostBuster checks whether observed outgoing BGP messages could have been produced by incoming ones. The key challenge in doing so is that BGP routers do not necessarily process incoming messages in order, forcing one to consider all possible reorderings of input messages. While this obviously does not scale, we show that one can solve this problem efficiently by reasoning about sets of messages instead of orderings. We fully implemented GhostBuster and use it to detect (confirmed and previously unknown) bugs in production routers. Our evaluation on simulated networks further confirms that GhostBuster is both scalable and accurate: it never falsely reports a bug while detecting over 60% of the bugs.