Plankton: Scalable network configuration verification through model checking

Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, P. Brighten Godfrey, Matthew Caesar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Network configuration verification enables operators to ensure that the network will behave as intended, prior to deployment of their configurations. Although techniques ranging from graph algorithms to SMT solvers have been proposed, scalable configuration verification with sufficient protocol support continues to be a challenge. In this paper, we show that by combining equivalence partitioning with explicit-state model checking, network configuration verification can be scaled significantly better than the state of the art, while still supporting a rich set of protocol features. We propose Plankton, which uses symbolic partitioning to manage large header spaces and efficient model checking to exhaustively explore protocol behavior. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art.

Original languageEnglish (US)
Title of host publicationProceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020
PublisherUSENIX Association
Pages953-967
Number of pages15
ISBN (Electronic)9781939133137
StatePublished - 2020
Event17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020 - Santa Clara, United States
Duration: Feb 25 2020Feb 27 2020

Publication series

NameProceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020

Conference

Conference17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020
CountryUnited States
CitySanta Clara
Period2/25/202/27/20

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Control and Systems Engineering

Fingerprint Dive into the research topics of 'Plankton: Scalable network configuration verification through model checking'. Together they form a unique fingerprint.

Cite this