P-Rex: fast verification of MPLS networks with multiple link failures

Jesper Stenbjerg Jensen, Troels Beck Krøgh, Jonas Sand Madsen, Stefan Schmid, Jiri Srba, Marc Tom Thorgersen

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

4 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
TitelProceedings of the 14th International Conference on emerging Networking EXperiments and Technologies
Antal sider11
ForlagAssociation for Computing Machinery
Publikationsdato2018
Sider217-227
ISBN (Trykt)978-1-4503-6080-7
ISBN (Elektronisk)978-1-4503-6080-7
DOI
StatusUdgivet - 2018
Begivenhed14th International Conference on emerging Networking EXperiments and Technologies - Heraklion, Greece, December 04-07, 2018. , Heraklion, Grækenland
Varighed: 4 dec. 20187 dec. 2018
Konferencens nummer: 14
https://conferences2.sigcomm.org/co-next/2018/#!/home

Konference

Konference14th International Conference on emerging Networking EXperiments and Technologies
Nummer14
LokationHeraklion, Greece, December 04-07, 2018.
LandGrækenland
ByHeraklion
Periode04/12/201807/12/2018
Internetadresse
NavnConference on Emerging Networking EXperiments and Technologies

Fingerprint

Switching networks
Labels
Routers
Query languages
Electric network analysis
Telecommunication networks
Polynomials

Citer dette

Jensen, J. S., Krøgh, T. B., Madsen, J. S., Schmid, S., Srba, J., & Thorgersen, M. T. (2018). P-Rex: fast verification of MPLS networks with multiple link failures. I Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (s. 217-227 ). Association for Computing Machinery. Conference on Emerging Networking EXperiments and Technologies https://doi.org/10.1145/3281411.3281432
Jensen, Jesper Stenbjerg ; Krøgh, Troels Beck ; Madsen, Jonas Sand ; Schmid, Stefan ; Srba, Jiri ; Thorgersen, Marc Tom. / P-Rex: fast verification of MPLS networks with multiple link failures. Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery, 2018. s. 217-227 (Conference on Emerging Networking EXperiments and Technologies).
@inproceedings{f6f0cd3331264f11810c8f3703acf470,
title = "P-Rex: fast verification of MPLS networks with multiple link failures",
abstract = "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.",
keywords = "MPLS networks, verification, case study, formal methods, pushdown automata",
author = "Jensen, {Jesper Stenbjerg} and Kr{\o}gh, {Troels Beck} and Madsen, {Jonas Sand} and Stefan Schmid and Jiri Srba and Thorgersen, {Marc Tom}",
year = "2018",
doi = "10.1145/3281411.3281432",
language = "English",
isbn = "978-1-4503-6080-7",
series = "Conference on Emerging Networking EXperiments and Technologies",
publisher = "Association for Computing Machinery",
pages = "217--227",
booktitle = "Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies",
address = "United States",

}

Jensen, JS, Krøgh, TB, Madsen, JS, Schmid, S, Srba, J & Thorgersen, MT 2018, P-Rex: fast verification of MPLS networks with multiple link failures. i Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery, Conference on Emerging Networking EXperiments and Technologies, s. 217-227 , 14th International Conference on emerging Networking EXperiments and Technologies, Heraklion, Grækenland, 04/12/2018. https://doi.org/10.1145/3281411.3281432

P-Rex: fast verification of MPLS networks with multiple link failures. / Jensen, Jesper Stenbjerg ; Krøgh, Troels Beck; Madsen, Jonas Sand; Schmid, Stefan; Srba, Jiri; Thorgersen, Marc Tom.

Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery, 2018. s. 217-227 (Conference on Emerging Networking EXperiments and Technologies).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - P-Rex: fast verification of MPLS networks with multiple link failures

AU - Jensen, Jesper Stenbjerg

AU - Krøgh, Troels Beck

AU - Madsen, Jonas Sand

AU - Schmid, Stefan

AU - Srba, Jiri

AU - Thorgersen, Marc Tom

PY - 2018

Y1 - 2018

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.

AB - 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.

KW - MPLS networks

KW - verification

KW - case study

KW - formal methods

KW - pushdown automata

UR - https://dl.acm.org/citation.cfm?doid=3281411.3281432

U2 - 10.1145/3281411.3281432

DO - 10.1145/3281411.3281432

M3 - Article in proceeding

SN - 978-1-4503-6080-7

T3 - Conference on Emerging Networking EXperiments and Technologies

SP - 217

EP - 227

BT - Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies

PB - Association for Computing Machinery

ER -

Jensen JS, Krøgh TB, Madsen JS, Schmid S, Srba J, Thorgersen MT. P-Rex: fast verification of MPLS networks with multiple link failures. I Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery. 2018. s. 217-227 . (Conference on Emerging Networking EXperiments and Technologies). https://doi.org/10.1145/3281411.3281432