Preview abstract
Cloud and AI/ML workloads are posing unprecedented new requirements on the wide-area network: it must combine strict availability, massive growth, and feature agility. It became increasingly clear that traditional WAN designs were ill-equipped to adapt to these requirements.
We present Google's Global Network (GGN), a major architectural redesign of our WAN that evolves B2 and B4 into a single, modular, and highly available software-defined network. The architecture is designed around three pillars: (1) A modular design of functional domains with well-defined APIs; (2) a physically sharded and regionalized core for fault isolation and horizontal scaling; (3) a vendor-agnostic hardware strategy based on open standards. We share the multi-year deployment journey of GGN, including a safe, host-steered migration strategy, and demonstrate its ability to improve network availability and reaction time to failures, setting a foundation for a planet-scale modern WAN. View details
Proceedings of the 38th International Conference on Computer Aided Verification (CAV 2026)
Preview abstract
Operating a network is a daunting task. Operating one at a global scale, with stringent service objectives and requirements to be available during maintenance and failures, is even more so. At Google, we operate such a network. This paper details our experience applying formal methods to some of the networking protocols that are developed and maintained by in-house engineers. These protocols centrally route network traffic to respond to changes in demand, react to network failures, and allow for maintenance and upgrades.
We used formal methods to target a class of bugs stemming from unclear specifications, unintended system interactions, and logical errors at the specification level. We show how we modeled our protocols using an off-the-shelf model checker and a custom harness to scale the model horizontally. We were able to recreate several recent bugs and verify that the fixes implemented were correct. Finally, we present a method called state projection that we used to increase confidence in the coverage of our models, which we added to the TLC model checker for TLA+. We created 7 different TLA+ models and showed that they were effective at recreating bugs and verifying our fixes to those bugs.View details
Preview abstract
Private WANs are increasingly important to the operation of enterprises, telecoms, and cloud providers. For example, B4, Google’s private software-defined WAN, is larger and growing faster than our connectivity to the public Internet. In this paper, we present the five-year evolution of B4. We describe the techniques we employed to incrementally move from offering best-effort content-copy services to carrier-grade availability, while concurrently scaling B4 to accommodate 100x more traffic. Our key challenge is balancing the tension introduced by hierarchy required for scalability, the partitioning required for availability, and the capacity asymmetry inherent to the construction and operation of any large-scale network. We discuss our approach to managing this tension: i) we design a custom hierarchical network topology for both horizontal and vertical software scaling, ii) we manage inherent capacity asymmetry in hierarchical topologies using a novel traffic engineering algorithm without packet encapsulation, and iii) we re-architect switch forwarding rules via two-stage matching/hashing to deal with asymmetric network failures at scale.View details