TY - GEN
T1 - Relational Network Verification
AU - Xu, Xieyang
AU - Yuan, Yifei
AU - Kincaid, Zachary
AU - Krishnamurthy, Arvind
AU - Mahajan, Ratul
AU - Walker, David P.
AU - Zhai, Ennan
N1 - Publisher Copyright:
© 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.
PY - 2024/8/4
Y1 - 2024/8/4
N2 - 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.
AB - 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.
KW - domain-specific language
KW - network changes
KW - network verification
KW - regular language
KW - relational specification
KW - reliability
UR - http://www.scopus.com/inward/record.url?scp=85202288883&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85202288883&partnerID=8YFLogxK
U2 - 10.1145/3651890.3672238
DO - 10.1145/3651890.3672238
M3 - Conference contribution
AN - SCOPUS:85202288883
T3 - ACM SIGCOMM 2024 - Proceedings of the 2024 ACM SIGCOMM 2024 Conference
SP - 213
EP - 227
BT - ACM SIGCOMM 2024 - Proceedings of the 2024 ACM SIGCOMM 2024 Conference
PB - Association for Computing Machinery, Inc
T2 - 2024 ACM SIGCOMM Conference, ACM SIGCOMM 2024
Y2 - 4 August 2024 through 8 August 2024
ER -