Motivation
Internet Service Providers (ISPs) rely on the Border Gateway Protocol (BGP) to exchange routing information, which is necessary to deliver traffic over the Internet. The BGP behavior of an ISP’s routers is determined by their configurations. Router misconfigurations have caused major monetary loss, performance degradation, service outages, and security violations. Some of the effects of misconfiguration are highly visible, such as the worldwide extended downtime of YouTube in 2009 and route hijacks by China Telecom in 2010 and 2014. Less visible is the high cost of developing and maintaining correct configurations, which requires checking invariants across hundreds of thousands of lines of configuration for all of an ISP’s routers.
Bagpipe enables ISP administrators to express BGP policies in a domain-specific specification language and verify that the ISP’s router configurations implement these policies.
We have evaluated Bagpipe on Internet2 and two other ISPs, with a combined total of over 240,000 lines of router configuration. We identified and expressed policies for these ISPs, and found 19 inconsistencies between the policies and the router configurations without issuing any false positives.
Bagpipe is open-source and hosted on GitHub.
Publications
“Formal Semantics & Verification for the Border Gateway Protocol” (Tech Report) by Konstantin Weitz, Doug Woos, Arvind Krishnamurthy, Michael D. Ernst, and Zachary Tatlock.
Download: PDF.
“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.
Download: PDF.
“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.
Download: PDF.
People
If you have any question, want to be kept up-to date, or just want to say hi, email us at weitzkon at cs dot uw dot edu.
