Title: Formal Semantics and Scalable Verification for the Border Gateway Protocol using Proof Assistants and SMT Solvers
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, Internet Service Providers (ISPs) must configure their Border Gateway Protocol (BGP) routers to implement policies restricting 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 challenging in practice, and misconfiguration has led to extended worldwide outages and traffic hijacks.
We present Bagpipe, the first system that enables ISPs to declaratively specify control-plane policies and that automatically verifies that router configurations implement such policies using an SMT solver.
We evaluated the expressiveness of Bagpipe's policy 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.
To ensure Bagpipe correctly checks configurations, we verified its implementation in Coq, which required developing both the first formal semantics for BGP based on RFC~4271; and SpaceSearch, a new framework for verifying solver-aided tools.
We provide evidence for the correctness and usefulness of our BGP semantics by verifying Bagpipe, formalizing Gao and Rexford's pen-and-paper proof on the stability of BGP (this proof required a necessary extension to the original proof), and performing random differential testing of C-BGP (a BGP simulator) revealing 2 bugs in C-BGP, but none in our BGP semantics.
We provide evidence for the general usefulness of SpaceSearch, by building and verifying two solver-aided tools. The first tool is Bagpipe, the second tool, SaltShaker, checks that RockSalt's x86 semantics for a given instruction agrees with STOKE's x86 semantics. SaltShaker identified 7 bugs in RockSalt and 1 bug in STOKE. After these systems were patched by their developers, SaltShaker verified the semantics' agreement on 15,255 instructions in under 2h.