New Evolution of Hoyan: Enhancing Scalability, Usability, and Accuracy for Alibaba's Global WAN Verification

The network verification system Hoyan has been deployed for Alibaba Cloud's wide-area network (WAN) for years and achieved considerable success in preventing misconfiguration-caused network incidents. However, recent years have seen the emergence of new challenges in scalability, usability, and accuracy for Hoyan. This paper presents the new evolution of Hoyan to address these challenges. First, to support the large increase in the number of routers and prefixes on our WAN, Hoyan's simulation has evolved from a centralized fashion to a distributed framework, which improves the efficiency by 5 times and can scale to 𝑂 (10 4 ) routers, millions of prefixes, and billions of flows. Second, to improve Hoyan's usability in checking route change intents, we developed a specification language RCL, which supports the easy specification and automatic verification of route change intents. Third, to ensure high accuracy, we enhanced Hoyan's accuracy diagnosis framework, which helped us identify and fix dozens of implementation and modeling issues. Hoyan is used on a daily basis for our WAN. It supports 𝑂 (100) verification requests each week, prevents 𝑂 (10) incidents each year, and helps reduce the percentage of misconfiguration-caused network incidents from 56% to 5%.