Validating datacenters at scale

TLDR

The paper documents how formal methods and automated theorem proving can be used for network operation at scale, showing that network verification grounded in architectural constraints is integral to operating a reliable cloud. The authors developed the SecGuru and RCDC tools in Azure, employing local contracts and parallel checks without global snapshots, declarative configuration encodings, and automated theorem proving to derive intent from architectures and embed verification as prechecks, live monitoring, and policy evolution. SecGuru, deployed since 2013, is a pioneering industrial network verification tool that validates ACLs and, with RCDC, checks forwarding tables at Azure scale.

Abstract

We describe our experiences using formal methods and automated theorem proving for network operation at scale. The experiences are based on developing and applying the SecGuru and RCDC (Reality Checker for Data Centers) tools in Azure. SecGuru has been used since 2013 and thus, is arguably a pioneering industrial deployment of network verification. SecGuru is used for validating ACLs and more recently RCDC checks forwarding tables at Azure scale. A central technical angle is that we use local contracts and local checks, that can be performed at scale in parallel, and without maintaining global snapshots, to validate global properties of datacenter networks. Specifications leverage declarative encodings of configurations and automated theorem proving for validation. We describe how intent is automatically derived from network architectures and verification is incorporated as prechecks for making changes, live monitoring, and for evolving legacy policies. We document how network verification, grounded in architectural constraints, can be integral to operating a reliable cloud at scale.