This paper presents our experience deploying TianYan on Alibaba Cloud's global production WAN, which is, to the best of our knowledge, the first system for verifying non-deterministic convergence on a global production WAN. In daily operation, we rely on simulation-based configuration verifiers that assume a single converged data plane to ensure reliability and performance. However, non-deterministic convergence—where a configuration yields different converged data planes—undermines verification accuracy and has caused a production incident, motivating the need to analyze non-deterministic convergence itself. At scale, this is challenging because the analysis space grows exponentially with the number of routers. TianYan addresses this challenge with a key insight: by leveraging routing similarity among routers within the same group—a common fault-tolerance practice—it reduces exponential complexity from the number of routers to the number of groups, enabling efficient convergence analysis. Over a year of deployment, TianYan identified non-deterministic convergence in ~2% of all prefixes, exposed unnoticed design flaws, and improved simulation-based verification accuracy through integration. We share representative cases and evaluation results from our production WAN, distilling key operational lessons and practical guidelines for managing nondeterminism at scale.
Xing Fang, Fangdan Ye, Yifei Yuan et al.· Conference on Applications,...· 0 citations
Distributed in-network programs are increasingly deployed in data centers for their performance benefits, but shifting application logic to switches also enlarges the failure domain. Ensuring their correctness before deployment is thus critical for reliability. While prior verification frameworks can efficiently verify programs running on a single switch, they overlook the common interactive behaviors in distributed settings, thereby missing related bugs that can cause system failures. This paper presents Procurator, a verification framework that efficiently captures interactive behaviors in distributed in-network programs. Procurator models each P4 pipeline as a reactive actor and unifies their interactions as message passing to capture interactive behaviors under an event-driven paradigm. To improve the verification efficiency, Procurator employs an intermediate representation (IR) pruner to reduce the execution space and a schedule-replay-based acceleration approach to avoid explicit exploration of long execution traces. Evaluation shows that Procurator uncovers 28 distinct bugs in twelve real-world distributed in-network systems, and achieves up to a 9.1X speedup over the state-of-the-art framework.
Mingyuan Song, Huan-Xing Shen, Jinghui Jiang et al.· Conference on Applications,...· 0 citations
Network verification checks whether forwarding behavior satisfies intended invariants. In interdomain settings, data-plane verification is challenging because forwarding configurations are private, while post-incident review requires repeatable, version-specific checking without costly online coordination. We present AegisPath, it replaces centralized verification with distributed witness generation to protect AS-local configurations, decouples witness generation from repeated auditing through a commit-and-prove design, uses zero-knowledge proofs to answer queries without revealing forwarding paths, and supports incremental updates. Experiments show that offline Secure Multi-Party Computation (SMPC) witness generation takes from thousands to over 104 seconds, online Zero-Knowledge (ZK) auditing remains sub-second, and incremental maintenance yields substantial speedups over full re-computation.
Mingjun Fang, Shuhao Zheng, Zonglun Li et al.· Asia-Pacific Workshop on Net...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
