P-Rex: Fast Verification of MPLS Networks with Multiple Link
Failures

D 2018

P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures

JENSEN, Jesper S., Troels B. KROEGH, Jonas S. MADSEN, Stefan SCHMID, Jiří SRBA et. al.

Základní údaje

Originální název

P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures

Autoři

JENSEN, Jesper S. (208 Dánsko), Troels B. KROEGH (208 Dánsko), Jonas S. MADSEN (208 Dánsko), Stefan SCHMID (756 Švýcarsko), Jiří SRBA (203 Česká republika, garant, domácí) a Marc T. THORGERSEN (208 Dánsko)

Vydání

USA, Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT'18), od s. 217-227, 11 s. 2018

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Kód RIV

RIV/00216224:14330/18:00106628

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-6080-7

DOI

http://dx.doi.org/10.1145/3281411.3281432

UT WoS

000455383800019

Klíčová slova anglicky

MPLS networks; formal verification; pushdown automata

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 3. 5. 2019 14:59, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Future communication networks are expected to be highly automated, disburdening human operators of their most complex tasks. However, while first powerful and automated network analysis tools are emerging, existing tools provide very limited (and inefficient) support of reasoning about failure scenarios. We present P-Rex, a fast what-if analysis tool, that allows us to test important reachability and policy-compliance properties even under an arbitrary number of failures, in polynomial-time, i.e., without enumerating all failure scenarios (the usual approach today, if supported at all). P-Rex targets networks based on Multiprotocol Label Switching (MPLS) and its Segment Routing (SR) extension and comes with an expressive query language based on regular expressions. It takes into account the actual router tables, and is hence well-suited for debugging. We also report on an industrial case study and demonstrate that P-Rex supports rich queries, performing what-if analyses in less than 70 minutes in most cases, in a 24-router network with about 100,000 forwarding rules.

Citovat

JENSEN, Jesper S., Troels B. KROEGH, Jonas S. MADSEN, Stefan SCHMID, Jiří SRBA a Marc T. THORGERSEN. P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures. In Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT'18). USA: ACM, 2018, s. 217-227. ISBN 978-1-4503-6080-7. Dostupné z: https://dx.doi.org/10.1145/3281411.3281432.

@inproceedings{1506128,
   author = {Jensen, Jesper S. and Kroegh, Troels B. and Madsen, Jonas S. and Schmid, Stefan and Srba, Jiří and Thorgersen, Marc T.},
   address = {USA},
   booktitle = {Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT'18)},
   doi = {http://dx.doi.org/10.1145/3281411.3281432},
   keywords = {MPLS networks; formal verification; pushdown automata},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {USA},
   isbn = {978-1-4503-6080-7},
   pages = {217-227},
   publisher = {ACM},
   title = {P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures},
   url = {https://dl.acm.org/citation.cfm?id=3281432},
   year = {2018}
}

TY  - JOUR
ID  - 1506128
AU  - Jensen, Jesper S. - Kroegh, Troels B. - Madsen, Jonas S. - Schmid, Stefan - Srba, Jiří - Thorgersen, Marc T.
PY  - 2018
TI  - P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures
PB  - ACM
CY  - USA
SN  - 9781450360807
KW  - MPLS networks
KW  - formal verification
KW  - pushdown automata
UR  - https://dl.acm.org/citation.cfm?id=3281432
L2  - https://dl.acm.org/citation.cfm?id=3281432
N2  - Future communication networks are expected to be highly automated, disburdening human operators of their most complex tasks. However, while first powerful and automated network analysis tools are emerging, existing tools provide very limited (and inefficient) support of reasoning about failure scenarios. We present P-Rex, a fast what-if analysis tool, that allows us to test important reachability and policy-compliance properties even under an arbitrary number of failures, in polynomial-time, i.e., without enumerating all failure scenarios (the usual approach today, if supported at all). P-Rex targets networks based on Multiprotocol Label Switching (MPLS) and its Segment Routing (SR) extension and comes with an expressive query language based on regular expressions. It takes into account the actual router tables, and is hence well-suited for debugging. We also report on an industrial case study and demonstrate that P-Rex supports rich queries, performing what-if analyses in less than 70 minutes in most cases, in a 24-router network with about 100,000 forwarding rules.
ER  -

JENSEN, Jesper S., Troels B. KROEGH, Jonas S. MADSEN, Stefan SCHMID, Jiří SRBA a Marc T. THORGERSEN. P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures. In \textit{Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT'18)}. USA: ACM, 2018, s.~217-227. ISBN~978-1-4503-6080-7. Dostupné z: https://dx.doi.org/10.1145/3281411.3281432.

Podrobný výpis o publikaci