TitleScalable verification of Border Gateway Protocol configurations with an SMT solver
Publication TypeConference Paper
Year of Publication2016
AuthorsWeitz K, Woos D, Torlak E, Ernst MD, Krishnamurthy A, Tatlock Z
Conference NameOOPSLA 2016, Object-Oriented Programming Systems, Languages, and Applications
Date or Month PublishedNovember
Conference LocationAmsterdam
AbstractInternet 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.
Downloadshttps://www.youtube.com/watch?v=eKB5Vj0PsIk talk video https://bagpipe.uwplse.org Bagpipe homepage
Citation KeyWeitzWTEKT2016