APKeep: Realtime Verification for Real Networks
Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, Hao Li
Abstract
Realtime network verification ensures the correctness of network by incrementally checking data plane updates in real time (e.g., < 1ms per rule update). Even state-of-the-art methods can already achieve sub-millisecond verification time, such speed is achieved mostly for pure IP forwarding devices, and is unrealistic for real-world networks, due to two reasons.
(1) Their network models cannot express the forwarding behavior of real devices, which have various functions including IP forwarding, ACL, NAT, policy-based routing, etc. (2) Their update algorithms do not scale in space and/or time: multifield rules (e.g., ACL rules) can make these tools run out of memory and/or incur long verification time. To scale realtime verification to real networks, we propose APKeep based on a new modular network model that is expressive for real devices, and propose new algorithms that can achieve low memory cost and fast update speed at the same time. Our experiments show that for real-world update traces consisting of IP forwarding rules and ACL rules, existing methods either run out of memory or incur a prohibitively long verification time, while APKeep still achieves a sub-millisecond verification time. We also show that APKeep can verify an update of NAT rule mostly in less than 1 millisecond.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 4af99469-a0b1-414c-b6e0-8466e3e2a5c1Cited by top-tier papers14
- Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device VerificationQiao Xiang, Chenyang Huang, Ridi Wen, Yuxin Wang et al.SIGCOMM 2023 · 26 citations
- A Scalable and Dynamic ACL System for In-Network DefenseChanghun Jung, Sian Kim, Rhongho Jang, David Mohaisen et al.CCS 2022 · 17 citations
- Crescent: Emulating Heterogeneous Production Network at ScaleZhaoyu Gao, Anubhavnidhi Abhashkumar, Zhen Sun, Weirong Jiang et al.NSDI 2024 · 15 citations
- NDD: A Decision Diagram for Network VerificationZechun Li, Peng Zhang, Yichi Zhang, Hongkun YangNSDI 2025 · 11 citations
- KATch: A Fast Symbolic Verifier for NetKATMark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais et al.PLDI 2024 · 9 citations
Builds on1
Related papers
- Atlas: Towards Real-Time Verification in Large-Scale Networks via a Native Distributed ArchitectureMingxiao Ma, Yuehan Zhang, Jingyu Wang, Bo He et al.EuroSys 2025 · 3 citations
- EPVerifier: Accelerating Update Storms Verification with Edge-PredicateChenyang Zhao, Yuebin Guo, Jingyu Wang, Qi Qi et al.NSDI 2024 · 7 citations
- Katra: Realtime Verification for Multilayer NetworksRyan Beckett, Aarti GuptaNSDI 2022
- Liveness Verification of Stateful Network FunctionsFarnaz Yousefi, Anubhavnidhi Abhashkumar, Kausik Subramanian, Kartik Hans et al.NSDI 2020 · 20 citations
- Tiramisu: Fast Multilayer Network VerificationAnubhavnidhi Abhashkumar, Aaron Gember-Jacobson, Aditya AkellaNSDI 2020 · 146 citations
