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.

Basic information

Original name

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

Authors

JENSEN, Jesper S. (208 Denmark), Troels B. KROEGH (208 Denmark), Jonas S. MADSEN (208 Denmark), Stefan SCHMID (756 Switzerland), Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution) and Marc T. THORGERSEN (208 Denmark)

Edition

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

Publisher

ACM

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

RIV identification code

RIV/00216224:14330/18:00106628

Organization unit

Faculty of Informatics

ISBN

978-1-4503-6080-7

DOI

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

UT WoS

000455383800019

Keywords in English

MPLS networks; formal verification; pushdown automata

Tags

core_A, firank_A

Tags

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

Abstract

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.
Displayed: 17/11/2024 14:56