Network Verification

Networks need to run reliably, efficiently, and without users noticing any problems, even as they grow. Keeping networks tuned this way requires the development of tools that improve the functioning of large-scale datacenter networks.

This project investigates a range of network verification tools that help network operators and architects design, operate, maintain, troubleshoot, and report on their large networks.

Specifically, the project explores three sub-areas:

Data-plane verification
Because networks forward packets according to their data plane, verification tools need to have data-plane intelligence built in, for pre- and post-deployment verification and bug detection.

Control-plane verification
Networks generate routing tables through protocols such as BGP (border gateway protocol). To analyze networks before they go into production, they need to be verified at this, the control-plane level.

Emulation
With emulation, network designers can find bugs in firmware and models; network operators can be trained before they are working on production systems. The goal of this product is to enable highly scalable, high-fidelity network emulation for those applications.

Deployed tools

We continue to develop and deploy a range of network verification tools.

SecGuru – checks network access restrictions of Network Security Groups
CrystalNet – emulates router BGP negotiation using virtual machines.
Network Logic Solver, NLS, – simulates, at scale, BGP negotiations.
RCDC – Reachability Checker in Data Centers, verifies, at scale, dataplanes in all of Microsoft’s datacenters with > 5B z3 queries per day.
VNetVerifier – reachability analysis tools for virtual network configurations.
Zen – microsoft/Zen: Zen is a constraint solving library for .NET. (opens in new tab)
NCVS – a system integrating most of the above tools to validate network repave operations.