Abstract
On the surface, large data centers with about 100,000 stations and nearly a million routing rules are complex and hard to verify. However, these networks are highly regular by design; for example they employ fat tree topologies with backup routers interconnected by redundant patterns. To exploit these regularities, we introduce network transformations: given a reachability formula and a network, we transform the network into a simpler to verify network and a corresponding transformed formula, such that the original formula is valid in the network if and only if the transformed formula is valid in the transformed network.
Our network transformations exploit network surgery (in which irrelevant or redundant sets of nodes, headers, ports, or rules are "sliced" away) and network symmetry (say between backup routers). The validity of these transformations is established using a formal theory of networks. In particular, using Van Benthem-Hennessy-Milner style bisimulation, we show that one can generally associate bisimulations to transformations connecting networks and formulas with their transforms. Our work is a development in an area of current wide interest: applying programming language techniques (in our case bisimulation and modal logic) to problems in switching networks.
We provide experimental evidence that our network transformations can speed up by 65x the task of verifying the communication between all pairs of Virtual Machines in a large datacenter network with about 100,000 VMs. An all-pair reachability calculation, which formerly took 5.5 days, can be done in 2 hours, and can be easily parallelized to complete in
Our network transformations exploit network surgery (in which irrelevant or redundant sets of nodes, headers, ports, or rules are "sliced" away) and network symmetry (say between backup routers). The validity of these transformations is established using a formal theory of networks. In particular, using Van Benthem-Hennessy-Milner style bisimulation, we show that one can generally associate bisimulations to transformations connecting networks and formulas with their transforms. Our work is a development in an area of current wide interest: applying programming language techniques (in our case bisimulation and modal logic) to problems in switching networks.
We provide experimental evidence that our network transformations can speed up by 65x the task of verifying the communication between all pairs of Virtual Machines in a large datacenter network with about 100,000 VMs. An all-pair reachability calculation, which formerly took 5.5 days, can be done in 2 hours, and can be easily parallelized to complete in
Original language | English |
---|---|
Title of host publication | Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
Publisher | ACM |
Pages | 69-83 |
Number of pages | 15 |
ISBN (Print) | 978-1-4503-3549-2 |
DOIs | |
Publication status | Published - 11 Jan 2016 |
Event | 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - St. Petersburg, FL, United States Duration: 20 Jan 2016 → 22 Jan 2016 https://popl16.sigplan.org/home |
Publication series
Name | ACM SIGPLAN Notices |
---|---|
Publisher | ACM |
Number | 1 |
Volume | 51 |
ISSN (Print) | 0362-1340 |
ISSN (Electronic) | 1558-1160 |
Conference
Conference | 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
---|---|
Abbreviated title | POPL 2016 |
Country/Territory | United States |
City | St. Petersburg, FL |
Period | 20/01/16 → 22/01/16 |
Internet address |
Fingerprint
Dive into the research topics of 'Scaling Network Verification using Symmetry and Surgery'. Together they form a unique fingerprint.Profiles
-
Gordon Plotkin
- School of Informatics - Professor
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active