Visible to the public Predicting Network Futures with PlanktonConflict Detection Enabled

TitlePredicting Network Futures with Plankton
Publication TypeConference Paper
Year of Publication2017
AuthorsSanthosh Prabhu, University of Illinois at Urbana-Champaign, Ali Kheradmand, University of Illinois at Urbana-Champaign, Brighten Godfrey, University of Illinois at Urbana-Champaign, Matthew Caesar, University of Illinois at Urbana-Champaign
Conference Name1st Asia-Pacific Workshop on Networking (APNet)
Conference LocationHong Kong, China
Keywordscorrectness, Network Troubleshooting
Abstract

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.

URLhttp://publish.illinois.edu/science-of-security-lablet/files/2014/05/Predicting-Network-Futures-with...
Citation Keynode-37477

Other available formats:

Predicting Network Futures with Plankton
AttachmentTaxonomyKindSize
Predicting Network Futures with PlanktonPDF document369.46 KBDownloadPreview