Quantitative Analysis of MPLS Networks in AalWiNes: Shortest Trace Reachability Analysis of Weighted Pushdown Systems
Translated title
Quantitative Analysis of MPLS Networks in AalWiNes
Authors
Kristiansen, Dan ; Schou, Morten Konggaard
Term
4. term
Education
Publication year
2020
Submitted on
2020-06-08
Pages
58
Abstract
Moderne digital kommunikation afhænger af sikre, pålidelige og effektive computernetværk, men at konfigurere dem er svært og sker ofte manuelt. AalWiNes er et værktøj, der effektivt (i polynomiel tid) analyserer adfærden i MPLS-netværk—en type netværk, der styrer trafik med labels—selv når flere forbindelser fejler. Værktøjet besvarer spørgsmål ved at omsætte dem til nåbarhedsspørgsmål på pushdown-systemer, en formel model med en stak. Vi udvider AalWiNes med kvantitative egenskaber for netværksspor (de sekvenser af trin, som pakker kan følge) og implementerer en effektiv algoritme, der finder spor, som minimerer disse egenskaber, f.eks. korteste spor. Vi definerer også en algoritme til automatisk generering af MPLS-netværk og implementerer nye algoritmer til pushdown-nåbarhed i biblioteket PDAAAL, som AalWiNes bruger. Vores eksperimenter viser, at vi overgår det hidtidige førende værktøj, som AalWiNes brugte til pushdown-nåbarhed, og at vores korteste-spor-algoritme for vægtede pushdown-systemer kun giver en lille ekstra omkostning sammenlignet med uvægtet nåbarhed.
Modern digital communication depends on safe, reliable, and efficient computer networks, yet configuring them is hard and mostly manual. AalWiNes is a tool that efficiently (in polynomial time) analyzes the behavior of MPLS networks—networks that route traffic using labels—even when several links fail. It answers questions by translating them into reachability questions on pushdown systems, a formal model with a stack. We extend AalWiNes with quantitative properties of network traces (the sequences of steps packets can take) and implement an efficient algorithm to find traces that minimize these properties, such as shortest traces. We also define an algorithm to automatically generate MPLS networks and implement new pushdown-reachability algorithms in the PDAAAL library used by AalWiNes. Our experiments show that we outperform the state-of-the-art tool previously used by AalWiNes for pushdown reachability, and that our shortest-trace algorithm for weighted pushdown systems adds only a small overhead compared to unweighted reachability.
[This abstract was generated with the help of AI]
Keywords
MPLS ; Pushdown automata ; Network ; Verification ; AalWiNes
Documents