| Title | Scalable verification of Border Gateway Protocol configurations with an SMT solver |
| Publication Type | Conference Paper |
| Year of Publication | 2016 |
| Authors | Weitz K, Woos D, Torlak E, Ernst MD, Krishnamurthy A, Tatlock Z |
| Conference Name | OOPSLA 2016, Object-Oriented Programming Systems, Languages, and Applications |
| Pagination | 765-780 |
| Date or Month Published | November |
| Conference Location | Amsterdam |
| 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. \par 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 \emphinitial 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. \par 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. |
| Downloads | https://www.youtube.com/watch?v=eKB5Vj0PsIk talk video
https://bagpipe.uwplse.org Bagpipe homepage
|
| Citation Key | WeitzWTEKT2016 |
