Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks

Stefan Schmid, Jiri Srba

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

7 Citations (Scopus)

Abstract

While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.
Original languageEnglish
Title of host publicationIEEE INFOCOM 2018 - IEEE Conference on Computer Communications
Number of pages9
PublisherIEEE
Publication date2018
Pages1799-1807
ISBN (Print)978-1-5386-4129-3
ISBN (Electronic)978-1-5386-4128-6
DOIs
Publication statusPublished - 2018
Event2018 IEEE Conference on Computer Communications Workshops, INFOCOM 2018 - Honolulu, United States
Duration: 15 Apr 201819 Apr 2018

Conference

Conference2018 IEEE Conference on Computer Communications Workshops, INFOCOM 2018
CountryUnited States
CityHonolulu
Period15/04/201819/04/2018
SeriesI E E E Infocom. Proceedings
ISSN0743-166X

Fingerprint

Telecommunication networks
Polynomials
Automata theory
Complex networks
Transparency
Computational complexity
Testing
Compliance

Keywords

  • MPLS networks
  • formal verification
  • pushdown automata

Cite this

Schmid, S., & Srba, J. (2018). Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks. In IEEE INFOCOM 2018 - IEEE Conference on Computer Communications (pp. 1799-1807). IEEE. I E E E Infocom. Proceedings https://doi.org/10.1109/INFOCOM.2018.8486261
Schmid, Stefan ; Srba, Jiri. / Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks. IEEE INFOCOM 2018 - IEEE Conference on Computer Communications. IEEE, 2018. pp. 1799-1807 (I E E E Infocom. Proceedings).
@inproceedings{239f337651d742c8baaab0a9eda04fb1,
title = "Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks",
abstract = "While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.",
keywords = "MPLS networks, formal verification, pushdown automata",
author = "Stefan Schmid and Jiri Srba",
year = "2018",
doi = "10.1109/INFOCOM.2018.8486261",
language = "English",
isbn = "978-1-5386-4129-3",
series = "I E E E Infocom. Proceedings",
publisher = "IEEE",
pages = "1799--1807",
booktitle = "IEEE INFOCOM 2018 - IEEE Conference on Computer Communications",
address = "United States",

}

Schmid, S & Srba, J 2018, Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks. in IEEE INFOCOM 2018 - IEEE Conference on Computer Communications. IEEE, I E E E Infocom. Proceedings, pp. 1799-1807, 2018 IEEE Conference on Computer Communications Workshops, INFOCOM 2018, Honolulu, United States, 15/04/2018. https://doi.org/10.1109/INFOCOM.2018.8486261

Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks. / Schmid, Stefan; Srba, Jiri.

IEEE INFOCOM 2018 - IEEE Conference on Computer Communications. IEEE, 2018. p. 1799-1807 (I E E E Infocom. Proceedings).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

TY - GEN

T1 - Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks

AU - Schmid, Stefan

AU - Srba, Jiri

PY - 2018

Y1 - 2018

N2 - While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.

AB - While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.

KW - MPLS networks

KW - formal verification

KW - pushdown automata

UR - https://ieeexplore.ieee.org/document/8486261

U2 - 10.1109/INFOCOM.2018.8486261

DO - 10.1109/INFOCOM.2018.8486261

M3 - Article in proceeding

SN - 978-1-5386-4129-3

T3 - I E E E Infocom. Proceedings

SP - 1799

EP - 1807

BT - IEEE INFOCOM 2018 - IEEE Conference on Computer Communications

PB - IEEE

ER -

Schmid S, Srba J. Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS Networks. In IEEE INFOCOM 2018 - IEEE Conference on Computer Communications. IEEE. 2018. p. 1799-1807. (I E E E Infocom. Proceedings). https://doi.org/10.1109/INFOCOM.2018.8486261