Reduction-based Analysis of BGP Systems with BGPVerif

被引：0
|
作者：
Wang, Anduo [1 ]
Gurney, Alexander J. T. [1 ]
Han, Xianglong [1 ]
Cao, Jinyan [1 ]
Talcott, Carolyn
Loo, Boon Thau [1 ]
Scedrov, Andre [1 ]
机构：
[1] Univ Penn, Philadelphia, PA 19104 USA
来源：
ACM SIGCOMM COMPUTER COMMUNICATION REVIEW | 2012年 / 42卷 / 04期
关键词：
Verification; Management; Border gateway protocol; reduction; formal analysis;
D O I：
10.1145/2377677.2377695
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Today's inter-domain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfiguration by individual autonomous systems (ASes). Existing configuration analysis techniques are either manual and tedious, or do not scale beyond a small number of nodes due to the state explosion problem. To aid the diagnosis of misconfigurations in real-world large BGP systems, this paper presents BGPVerif, a reduction based analysis toolkit. The key idea is to reduce BGP system size prior to analysis while preserving crucial correctness properties. BGPVerif consists of two components, Net Reducer that simplifies BGP configurations, and Net Analyzer that automatically detects routing oscillation. BGPVerif accepts a wide range of BGP configuration inputs ranging from real-world traces (Rocketfuel network topologies), randomly generated BGP networks (GT-ITM), Cisco configuration guidelines, as well as arbitrary user-defined networks. BGPVerif illustrates the applicability, efficiency, and benefits of the reduction technique, it also introduces an infrastructure that enables networking researchers to interact with advanced formal method tool.
引用
收藏
页码：89 / 90
页数：2
相关论文
共 50 条
  • [21] Adaptive reduction-based multigrid for nearly singular and highly disordered physical systems
    Brannick, J.
    Frommer, A.
    Kahl, K.
    MacLachlan, S.
    Zikatanov, L.
    Electronic Transactions on Numerical Analysis, 2010, 37 : 276 - 295
  • [22] Flow-based Mode Changes: Towards Virtual Uniprocessor Models for Efficient Reduction-based Schedulability Analysis of Distributed Systems
    Jayachandran, Praveen
    Abdelzaher, Tarek
    2009 30TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2009, : 281 - 290
  • [23] Reduction-Based Creative Telescoping for Algebraic Functions
    Chen, Shaoshi
    Kauers, Manuel
    Koutschan, Christoph
    PROCEEDINGS OF THE 2016 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC 2016), 2016, : 175 - 182
  • [24] Speculative Reduction-Based Scalable Redundancy Identification
    Mony, Hari
    Baumgartner, Jason
    Mishchenko, Alan
    Brayton, Robert
    DATE: 2009 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, VOLS 1-3, 2009, : 1674 - +
  • [25] Dimensionality reduction-based spoken emotion recognition
    Zhang, Shiqing
    Zhao, Xiaoming
    MULTIMEDIA TOOLS AND APPLICATIONS, 2013, 63 (03) : 615 - 646
  • [26] A Reduction-based Approach Towards Scaling Up Formal Analysis of Internet Configurations
    Wang, Anduo
    Gurney, Alexander J. T.
    Han, Xianglong
    Cao, Jinyan
    Loo, Boon Thau
    Talcott, Carolyn
    Scedrov, Andre
    2014 PROCEEDINGS IEEE INFOCOM, 2014, : 637 - 645
  • [27] Reduction-Based Robustness Analysis of Linear Predictor Feedback for Distributed Input Delays
    Ponomarev, Anton
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2016, 61 (02) : 468 - 472
  • [28] An input/output model reduction-based optimization scheme for large-scale systems
    Luna-Ortiz, E
    Theodoropoulos, C
    MULTISCALE MODELING & SIMULATION, 2005, 4 (02): : 691 - 708
  • [29] Reduction-Based Problem Mapping for Quantum Computing
    Hu, Shaohan
    Liu, Peng
    Chen, Chun-Fu
    Pistoia, Marco
    Gambetta, Jay
    COMPUTER, 2019, 52 (06) : 47 - 57
  • [30] Dimensionality reduction-based spoken emotion recognition
    Shiqing Zhang
    Xiaoming Zhao
    Multimedia Tools and Applications, 2013, 63 : 615 - 646
12345