Title: Formally Verified Solver Aided Tools for the Border Gateway Protocol
Advisors: Michael Ernst and Zach Tatlock
Supervisory Committee: Michael Ernst (co-Chair), Zach Tatlock (co-Chair), Silas Beane (GSR, Physics), and Arvind Krishnamurthy
Abstract: To reliably and securely route traffic across the Internet, In- ternet Service Providers (ISPs) must configure their Border Gateway Protocol (BGP) routers to implement policies re- stricting 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 chal- lenging in practice, and misconfiguration has led to extended worldwide outages and traffic hijacks.
We present Bagpipe, the first system that enables ISPs to declaratively express control-plane policies and that auto- matically verifies that router configurations implement such policies using an SMT solver. To ensure Bagpipe correctly checks configurations, we verified its implementation in Coq, which required developing both the first formal semantics of the BGP specification RFC 4271, and also a new framework for solver-aided tool verification (SearchSpace).
Our semantics models all required features of the BGP specification modulo low-level details such as bit representa- tion of update messages and TCP. Three case studies provide evidence for the correctness and general usefulness of our BGP semantics. 1) We verified the soundness of Bagpipe. 2) We formalized and extended the seminal pen-and-paper proof by Gao & Rexford on the convergence of BGP, revealing nec- essary extensions to Gao & Rexford’s original assumptions. 3) We tested the popular BGP simulator C-BGP against our semantics, revealing a bug in C-BGP.
SearchSpace is a technique to verify, by means of a proof assistant, tools that use SMT solvers. Three case studies will provide evidence for the general usefulness of SearchSpace. 1) We constructed and verified Bagpipe. 2) We will verify an SMT x86 semantics against a Coq x86 semantics (remains to be done). 3) We will verify a SMT based tool that checks the correctness of SQL rewrite rules (remains to be done).
We evaluated the expressiveness of Bagpipe’s specification language on 10 configuration scenarios from the Juniper TechLibrary, and evaluated the efficiency of Bagpipe on three ASes with a total of over 240,000 lines of Cisco and Juniper BGP configuration. Bagpipe revealed 19 policy violations without issuing any false positives.
We compare our work to the related work on: Solver Aided Tools, the BGP specification RFC 4271, Gao & Rexford’s proof of BGP convergence, the Stable Paths Problem (SPP), tools to help avoid BGP misconfiguration, and Software Defined Networking (SDN).