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
T2 - 2018 IEEE Conference on Computer Communications Workshops, INFOCOM 2018
Y2 - 15 April 2018 through 19 April 2018
ER -