We present the first mechanized formal semantics of BGP based on the BGP specification RFC 4271, 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 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; 2) we have tested the BGP simulator C-BGP, revealing one bug; and 3) we are currently extending and formalizing the pen-and-paper proof by Gao & Rexford on the convergence of BGP, revealing necessary extensions to Gao & Rexford’s original configuration guidelines.
[ bib | project | paper ] Back
This file was generated by bibtex2html 1.97.