KATRA: Realtime Verification for Multilayer Networks

Ryan Beckett, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Abstract

We present a new verification algorithm to efficiently and incrementally verify arbitrarily layered network data planes that are implemented using packet encapsulation. Inspired by work on model checking of pushdown systems for recursive programs, we develop a verification algorithm for networks with packets consisting of stacks of headers. Our algorithm is based on a new technique that lazily “repairs” a decomposed stack of header sets on demand to account for cross-layer dependencies. We demonstrate how to integrate our approach with existing fast incremental data plane verifiers and have implemented our ideas in a tool called KATRA. Evaluating KATRA against an alternative approach based on equipping existing incremental verifiers to emulate finite header stacks, we show that KATRA is between 5x-32x faster for packets with just 2 headers (layers), and that its performance advantage grows with both network size and layering.

Original languageEnglish (US)
Title of host publicationProceedings of the 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022
PublisherUSENIX Association
Pages617-634
Number of pages18
ISBN (Electronic)9781939133274
StatePublished - 2022
Event19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022 - Renton, United States
Duration: Apr 4 2022Apr 6 2022

Publication series

NameProceedings of the 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022

Conference

Conference19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022
Country/TerritoryUnited States
CityRenton
Period4/4/224/6/22

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Control and Systems Engineering

Fingerprint

Dive into the research topics of 'KATRA: Realtime Verification for Multilayer Networks'. Together they form a unique fingerprint.

Cite this