Tiramisu: Fast and General Network Verification

TL;DR

Tiramisu is a novel multilayer graph-based verification tool that enables rapid and general verification of complex network control plane policies, significantly outperforming existing methods.

Contribution

We introduce Tiramisu, a new multilayer hedge graph abstraction that combines graph traversal and ILPs for fast, comprehensive network policy verification.

Findings

Verifies policies in under 0.08 seconds for small networks

Verifies policies in under 0.12 seconds for large networks

Achieves 10-600X speedup over existing verification tools

Abstract

Today's distributed network control planes support multiple routing protocols, filtering mechanisms, and route selection policies. These protocols operate at different layers, e.g. BGP operates at the EGP layer, OSPF at the IGP layer, and VLANs at layer 2. The behavior of a network's control plane depends on how these protocols interact with each other. This makes network configurations highly complex and error-prone. State-of-the-art control plane verifiers are either too slow, or do not model certain features of the network. In this paper, we propose a new multilayer hedge graph abstraction, Tiramisu, that supports fast verification of the control plane. Tiramisu uses a combination of graph traversal algorithms and ILPs (Integer Linear Programs) to check different network policies. We use Tiramisu to verify policies of various real-world and synthetic configurations. Our experiments show that Tiramisu can verify any policy in < 0.08 s in small networks (~35 devices) and < 0.12 s in large networks (~160 devices), and it is 10-600X faster than state-of-the-art without losing generality.