000198189 001__ 198189
000198189 005__ 20190316235907.0
000198189 037__ $$aCONF
000198189 245__ $$aSoftware Dataplane Verification
000198189 269__ $$a2014
000198189 260__ $$c2014
000198189 336__ $$aConference Papers
000198189 520__ $$aSoftware 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.
000198189 6531_ $$aSoftware routers
000198189 6531_ $$aMiddleboxes
000198189 6531_ $$aNetwork verification
000198189 700__ $$0243543$$g184891$$aDobrescu, Mihai
000198189 700__ $$aArgyraki, Katerina$$g176638$$0243542
000198189 7112_ $$dApril 2-4, 2014$$cSeattle, WA, USA$$aUSENIX Symposium on Networked Systems Design and Implementation (NSDI)
000198189 773__ $$tProceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)
000198189 8564_ $$uhttps://infoscience.epfl.ch/record/198189/files/dataplaneVerificationNsdi14_1.pdf$$zPublisher's version$$s294462$$yPublisher's version
000198189 909C0 $$xU12550$$0252412$$pNAL
000198189 909CO $$qGLOBAL_SET$$pconf$$ooai:infoscience.tind.io:198189$$pIC
000198189 917Z8 $$x176638
000198189 917Z8 $$x176638
000198189 917Z8 $$x176638
000198189 937__ $$aEPFL-CONF-198189
000198189 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000198189 980__ $$aCONF