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.

Publié dans:
Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)
Présenté à:
USENIX Symposium on Networked Systems Design and Implementation (NSDI), Seattle, WA, USA, April 2-4, 2014

 Notice créée le 2014-04-07, modifiée le 2019-03-16

Publisher's version:
Télécharger le document

Évaluer ce document:

Rate this document:
(Pas encore évalué)