Bagpipe : Verified BGP Configuration Checking

To reliably and securely route traffic across the Internet, Internet Service Providers (ISPs) must configure their Border Gateway Protocol (BGP) routers to implement policies restricting how routing information can be exchanged with other ISPs. Correctly implementing these policies in lowlevel router configuration languages, with configuration code distributed across all of an ISP’s routers, has proven challenging in practice, and misconfiguration has led to extended worldwide outages and traffic hijacks. We present Bagpipe, a system that enables ISPs to concisely express their policies and automatically check that router configurations adhere to these policies. To check policies efficiently, Bagpipe introduces the initial network reduction, exploits modern satisfiability solvers by building on the Rosette framework for solver-aided tools, and parallelizes configuration checking across many nodes. To ensure Bagpipe correctly checks configurations, we verified its implementation in Coq, which required developing both a new framework for verifying solver-aided tools and also the first formal semantics for BGP based on RFC 4271. To validate the effectiveness of our verified checker, we ran it on the router configurations of Internet2, a nationwide ISP. Bagpipe revealed 19 violations of standard BGP router policies without issuing any false positives. To validate our BGP semantics, we performed random differential testing against C-BGP, a popular BGP simulator. We found no bugs in our semantics and one bug in C-BGP.