Tiramisu: Fast and General Network Verification
Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, Aditya Akella

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware-Defined Networks and 5G · Network Packet Processing and Optimization · Network Traffic and Congestion Control
