Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver

Download: PDF, slides (Keynote), talk video, Bagpipe homepage.

“Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver” by Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. In OOPSLA 2016, Object-Oriented Programming Systems, Languages, and Applications, (Amsterdam), Nov. 2016, pp. 765-780.
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 NetPL 2016: ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL 2016), (Florianópolis, Brazil), Aug. 2016.
A previous version appeared as “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.

Abstract

Internet Service Providers (ISPs) use the Border Gateway Protocol (BGP) to announce and exchange routes for delivering packets through the internet. ISPs must carefully configure their BGP routers to ensure traffic is routed reliably and securely. Correctly configuring BGP routers has proven challenging in practice, and misconfiguration has led to worldwide outages and traffic hijacks.

This paper presents Bagpipe, a system that enables ISPs to declaratively express BGP policies and that automatically verifies that router configurations implement such policies. The novel initial network reduction soundly reduces policy verification to a search for counterexamples in a finite space. An SMT-based symbolic execution engine performs this search efficiently. Bagpipe reduces the size of its search space using predicate abstraction and parallelizes its search using symbolic variable hoisting.

Bagpipe's policy specification language is expressive: we expressed policies inferred from real AS configurations, policies from the literature, and policies for 10 Juniper TechLibrary configuration scenarios. Bagpipe is efficient: we ran it on three ASes with a total of over 240,000 lines of Cisco and Juniper BGP configuration. Bagpipe is effective: it revealed 19 policy violations without issuing any false positives.

Download: PDF, slides (Keynote), talk video, Bagpipe homepage.

BibTeX entry:

@inproceedings{WeitzWTEKT2016,
   author = {Konstantin Weitz and Doug Woos and Emina Torlak and Michael
	D. Ernst and Arvind Krishnamurthy and Zachary Tatlock},
   title = {Scalable Verification of {Border} {Gateway} {Protocol}
	Configurations with an {SMT} Solver},
   booktitle = {OOPSLA 2016, Object-Oriented Programming Systems,
	Languages, and Applications},
   pages = {765-780},
   address = {Amsterdam},
   month = nov,
   year = {2016}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.