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 条
  • [41] Delay Composition Algebra: A Reduction-based Schedulability Algebra for Distributed Real-Time Systems
    Jayachandran, Praveen
    Abdelzaher, Tarek
    RTSS: 2008 REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2008, : 259 - 269
  • [42] A new reduction-based LQ control for dynamic systems with a slowly time-varying delay
    Masakazu Haraguchi
    Acta Mechanica Sinica, 2009, 25 (04) : 529 - 537
  • [43] Dimension reduction-based significance testing in nonparametric regression
    Zhu, Xuehu
    Zhu, Lixing
    ELECTRONIC JOURNAL OF STATISTICS, 2018, 12 (01): : 1468 - 1506
  • [44] On the Optimization of Lattice Reduction-Based Approximate MAP Detection Using Randomized Sampling in MIMO Systems
    Bai, Lin
    Li, Qiaoyu
    Choi, Jinho
    Yu, Quan
    2013 INTERNATIONAL CONFERENCE ON ICT CONVERGENCE (ICTC 2013): FUTURE CREATIVE CONVERGENCE TECHNOLOGIES FOR NEW ICT ECOSYSTEMS, 2013, : 136 - 140
  • [45] Reduction-based stabilization of nonlinear discrete-time systems through delayed state measurements
    Mattioni, Mattia
    Moreschini, Alessio
    Monaco, Salvatore
    Normand-Cyrot, Dorothee
    IFAC PAPERSONLINE, 2020, 53 (02): : 5851 - 5856
  • [46] Structural uncertainty analysis with the multiplicative dimensional reduction-based polynomial chaos expansion approach
    Zhang, Xufang
    Pandey, Mahesh D.
    Luo, Haoyang
    STRUCTURAL AND MULTIDISCIPLINARY OPTIMIZATION, 2021, 64 (04) : 2409 - 2427
  • [47] Nonlinear model reduction-based induction motor aggregation
    Zhang, Gang
    Du, Zhengchun
    Ni, Yu
    Li, Chongtao
    INTERNATIONAL TRANSACTIONS ON ELECTRICAL ENERGY SYSTEMS, 2016, 26 (02): : 398 - 411
  • [48] Probabilistic surrogate models for uncertainty analysis: Dimension reduction-based polynomial chaos expansion
    Son, Jeongeun
    Du, Yuncheng
    INTERNATIONAL JOURNAL FOR NUMERICAL METHODS IN ENGINEERING, 2020, 121 (06) : 1198 - 1217
  • [49] On the Convergence of Reduction-based and Model-based Methods in Proof Theory
    Dowek, Gilles
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 205 : 137 - 144
  • [50] Reduction-based stabilization of time-delay nonlinear dynamics
    Mattioni, Mattia
    Monaco, Salvatore
    Normand-Cyrot, Dorothee
    2018 IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2018, : 3471 - 3476
12345