Software Dataplane Verification

Software dataplanes are emerging as an alternative to traditional hardware switches and routers, promising programmability and short time to market. These advantages are set against the risk of disrupting the network with bugs, unpredictable performance, or security vulnerabilities. We explore the feasibility of verifying software dataplanes to ensure smooth network operation. For general programs, verifiability and performance are competing goals; we argue that software dataplanes are different---we can write them in a way that enables verification \emph{and} preserves performance. We present a verification tool that takes as input a software dataplane, written in a way that meets a given set of conditions, and (dis)proves that the dataplane satisfies crash-freedom, bounded-execution, and filtering properties. We evaluate our tool on stateless and simple stateful Click pipelines; we perform complete and sound verification of these pipelines within tens of minutes, whereas a state-of-the-art general-purpose tool fails to complete the same task within several hours.

Published in:
Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)
Presented at:
USENIX Symposium on Networked Systems Design and Implementation (NSDI), Seattle, WA, USA, April 2-4, 2014

Note: The status of this file is:

 Record created 2014-04-07, last modified 2019-12-05

Publisher's version:
Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)