Tiramisu: Fast Multilayer Network Verification

Authors: 

Anubhavnidhi Abhashkumar, University of Wisconsin - Madison; Aaron Gember-Jacobson, Colgate University; Aditya Akella, University of Wisconsin - Madison

Abstract: 

Today's distributed network control planes are highly sophisticated, with multiple interacting protocols operating at layers 2 and 3. The complexity makes network configurations highly complex and bug-prone. State-of-the-art tools that check if control plane bugs can lead to violations of key properties are either too slow, or do not model common network features. We develop a new, general multilayer graph control plane model that enables using fast, property-customized verification algorithms. Our tool, Tiramisu can verify if policies hold under failures for various real-world and synthetic configurations in < 0.08s in small networks and < 2.2s in large networks. Tiramisu is 2-600X faster than state-of-the-art without losing generality.

NSDI '20 Open Access Sponsored by NetApp

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {246278,
author = {Anubhavnidhi Abhashkumar and Aaron Gember-Jacobson and Aditya Akella},
title = {Tiramisu: Fast Multilayer Network Verification },
booktitle = {17th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 20)},
year = {2020},
isbn = {978-1-939133-13-7},
address = {Santa Clara, CA},
pages = {201-219},
url = {https://www.usenix.org/conference/nsdi20/presentation/abhashkumar},
publisher = {{USENIX} Association},
month = feb,
}

Presentation Video