Formal semantics and automated verification for the border gateway protocol

Traffic is routed across the Internet by Autonomous Systems, or ASes, such as ISPs, corporations, and universities. To route traffic reliably and securely, ASes must configure their Border Gateway Protocol (BGP) routers to implement policies restricting how routing announcements can be used and exchanged with other ASes.It is challenging to correctly implement BGP policies in low-level configuration languages. Large ASes maintain millions of lines of frequently-changing configurations that run distributed across hundreds of routers [8, 16]. Router misconfigurations are common and have led to highly visible failures affecting ASes and their billions of users. For example, in 2009 YouTube was inaccessible worldwide for several hours due to a misconfiguration in Pakistan [2], and in 2010 and 2014 China Telecom hijacked significant but unknown fractions of international traffic for extended periods [4, 15, 11, 10]. Goldberg surveys several additional major outages and their causes [7]. We present the first mechanized formal semantics of the BGP specification RFC 4271 [14], and we show how to use this semantics to develop reliable tools and guidelines that help BGP administrators avoid router misconfiguration. In contrast to previous semantics [6, 3, 17], our semantics is fully formal (it is implemented in the Coq proof assistant), and it models all required features of the BGP specification modulo low-level details such as bit representation of update messages and TCP.