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

doi:10.1145/3281411.3281432

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

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

28 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies
Number of pages	11
Publisher	Association for Computing Machinery
Publication date	2018
Pages	217-227
ISBN (Print)	978-1-4503-6080-7
ISBN (Electronic)	978-1-4503-6080-7
DOIs	https://doi.org/10.1145/3281411.3281432
Publication status	Published - 2018
Event	14th International Conference on emerging Networking EXperiments and Technologies - Heraklion, Greece, December 04-07, 2018. , Heraklion, Greece Duration: 4 Dec 2018 → 7 Dec 2018 Conference number: 14 https://conferences2.sigcomm.org/co-next/2018/#!/home

Conference

Conference	14th International Conference on emerging Networking EXperiments and Technologies
Number	14
Location	Heraklion, Greece, December 04-07, 2018.
Country/Territory	Greece
City	Heraklion
Period	04/12/2018 → 07/12/2018
Internet address	https://conferences2.sigcomm.org/co-next/2018/#!/home

Series	Conference on Emerging Networking EXperiments and Technologies

Keywords

MPLS networks
verification
case study
formal methods
pushdown automata

Access to Document

10.1145/3281411.3281432

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Jensen, Jesper Stenbjerg ; Krøgh, Troels Beck ; Madsen, Jonas Sand et al. / 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. pp. 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",

note = "14th International Conference on emerging Networking EXperiments and Technologies, CoNEXT'18 ; Conference date: 04-12-2018 Through 07-12-2018",

url = "https://conferences2.sigcomm.org/co-next/2018/#!/home",

}

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. in Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery, Conference on Emerging Networking EXperiments and Technologies, pp. 217-227 , 14th International Conference on emerging Networking EXperiments and Technologies, Heraklion, Greece, 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 et al.
Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery, 2018. p. 217-227 (Conference on Emerging Networking EXperiments and Technologies).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-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

N1 - Conference code: 14

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

T2 - 14th International Conference on emerging Networking EXperiments and Technologies

Y2 - 4 December 2018 through 7 December 2018

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. In Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies . Association for Computing Machinery. 2018. p. 217-227 . (Conference on Emerging Networking EXperiments and Technologies). doi: 10.1145/3281411.3281432

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

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this