Relational Network Verification

Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David P. Walker, Ennan Zhai

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

Abstract

Relational network verification is a new approach for validating network changes. In contrast to traditional network verification, which analyzes specifications for a single network snapshot, it analyzes specifications that capture similarities and differences between two network snapshots (e.g., pre- and post-change snapshots). Relational specifications are compact and precise because they focus on the flows and paths that change between snapshots and then simply mandate that all other network behaviors "stay the same", without enumerating them. To achieve similar guarantees, single-snapshot specifications would need to enumerate all flow and path behaviors that are not expected to change in order to enable checking that nothing has accidentally changed. Such specifications are proportional to network size, which makes them impractical to generate for many real-world networks.We demonstrate the value of relational reasoning by developing Rela, a high-level relational specification language and verification tool for network changes. Rela compiles input specifications and network snapshot representations to finite state automata, and it then verifies compliance by checking automaton equivalence. Our experiments using data from a global backbone with over 103 routers find that Rela specifications need fewer than 10 terms for 93% of the complex, high-risk changes. Rela validates 80% of the changes within 20 minutes.

Original languageEnglish (US)
Title of host publicationACM SIGCOMM 2024 - Proceedings of the 2024 ACM SIGCOMM 2024 Conference
PublisherAssociation for Computing Machinery, Inc
Pages213-227
Number of pages15
ISBN (Electronic)9798400706141
DOIs
StatePublished - Aug 4 2024
Event2024 ACM SIGCOMM Conference, ACM SIGCOMM 2024 - Sydney, Australia
Duration: Aug 4 2024Aug 8 2024

Publication series

NameACM SIGCOMM 2024 - Proceedings of the 2024 ACM SIGCOMM 2024 Conference

Conference

Conference2024 ACM SIGCOMM Conference, ACM SIGCOMM 2024
Country/TerritoryAustralia
CitySydney
Period8/4/248/8/24

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Keywords

  • domain-specific language
  • network changes
  • network verification
  • regular language
  • relational specification
  • reliability

Fingerprint

Dive into the research topics of 'Relational Network Verification'. Together they form a unique fingerprint.

Cite this