Bagpipe: Verified BGP configuration checking

Download: PDF, Bagpipe implementation.

“Bagpipe: Verified BGP configuration checking” by Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. University of Washington Department of Computer Science and Engineering technical report UW-CSE-16-01-01, (Seattle, WA, USA), Jan. 2016.
An overview appeared as “Formal Semantics and Automated Verification for the Border Gateway Protocol” by Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. In ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL 2016), (Florianópolis, Brazil), August 22, 2016.

Abstract

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 low-level 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.

Download: PDF, Bagpipe implementation.

BibTeX entry:

@techreport{WeitzWTEKT2016:TR,
   author = {Konstantin Weitz and Doug Woos and Emina Torlak and Michael
	D. Ernst and Arvind Krishnamurthy and Zachary Tatlock},
   title = {Bagpipe: Verified {BGP} configuration checking},
   institution = {University of Washington Department of Computer Science
	and Engineering},
   number = {UW-CSE-16-01-01},
   address = {Seattle, WA, USA},
   month = jan,
   year = {2016}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.