Formal Semantics and Automated Verification for the Border Gateway Protocol

Formal Semantics and Automated Verification for the Border Gateway Protocol
复制标题

边界网关协议的形式语义和自动验证

DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Krishnamurthy
A. Krishnamurthy
中科院分区：
--
文献类型：
--
作者：
Konstantin Weitz;Doug Woos;Emina Torlak;Michael D. Ernst;A. Krishnamurthy

文献摘要

被引文献

相似文献

流量是由自治系统或ASE（例如ISP，公司和大学）在互联网上进行的。并与其他ASE交换。在数百个路由器上分布的经常变化的配置[8，16]很常见，并导致高度可见的失败，影响了ASES及其数十亿个用户。由于巴基斯坦的配置错误[2]，并在2010年和2014年中国电信劫持了大量但未知的国际交通分数[4、15、11、10]。 。它将BGP规范的所有必需功能模型模型低级详细信息，例如更新消息的位表示和TCP。由Gao＆Rexford在BGP的融合中，向Gao＆Rexford的原始配置指南揭示了必要的扩展； BGP配置符合给定的策略规范，在三个ASE中揭示了19个明显的错误，其中超过240,000行BGP配置；我们已经测试了BGP模拟器C-BGP，揭示了一个错误。
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. 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.