Predicting network futures with plankton

Santhosh Prabhu, Ali Kheradmand, Brighten Godfrey, Matthew Caesar

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


Recent years have seen significant advancement in the field of formal network verification. Tools have been proposed for offline data plane verification, real-time data plane verification and configuration verification under arbitrary, but static sets of failures. However, due to the fundamental limitation of not treating the network as an evolving system, current verification platforms have significant constraints in terms of scope. In real-world networks, correctness policies may be violated only through a particular combination of environment events and protocol actions, possibly in a non-deterministic sequence. Moreover, correctness specifications themselves may often correlate multiple data plane states, particularly when dynamic data plane elements are present. Tools in existence today are not capable of reasoning about all the possible network events, and all the subsequent execution paths that are enabled by those events. We propose Plankton, a verification platform for identifying undesirable evolutions of networks. By combining symbolic modeling of data plane and control plane with explicit state exploration, Plankton performs a goal-directed search on a finite-state transition system that captures the behavior of the network as well as the various events that can influence it. In this way, Plankton can automatically find policy violations that can occur due to a sequence of network events, starting from the current state. Initial experiments have successfully predicted scenarios like BGP Wedgies.

Original languageEnglish (US)
Title of host publicationAPNET 2017 - Proceedings of the 2017 Asia-Pacific Workshop on Networking
PublisherAssociation for Computing Machinery
Number of pages7
ISBN (Print)9781450352444
StatePublished - Aug 3 2017
Event1st Asia-Pacific Workshop on Networking, APNET 2017 - Hong Kong, China
Duration: Aug 3 2017Aug 4 2017

Publication series

NameACM International Conference Proceeding Series


Other1st Asia-Pacific Workshop on Networking, APNET 2017
CityHong Kong


  • Correctness
  • Network Troubleshooting

ASJC Scopus subject areas

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications


Dive into the research topics of 'Predicting network futures with plankton'. Together they form a unique fingerprint.

Cite this