Trimmed abstract: “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, 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.

To provide evidence for the correctness and usefulness of our semantics: 1) we have extended and formalized the pen-and-paper proof by Gao & Rexford on the convergence of BGP, revealing necessary extensions to Gao & Rexford’s original configuration guidelines; 2) we have built the Bagpipe tool which automatically checks that BGP configurations adhere to given policy specifications, revealing 19 apparent errors in three ASes with over 240,000 lines of BGP configuration; and 3) we have tested the BGP simulator C-BGP, revealing one bug.”