000264620 001__ 264620
000264620 005__ 20190316233227.0
000264620 0247_ $$2doi$$a10.1145/3229538.3229540
000264620 02470 $$2DOI$$a10.1145/3229538.3229540
000264620 037__ $$aCONF
000264620 245__ $$aA Formally Verified NAT Stack
000264620 260__ $$c2018-08-20
000264620 269__ $$a2018-08-20
000264620 300__ $$a7
000264620 336__ $$aConference Papers
000264620 520__ $$aPrior work proved a stateful NAT network function to be semantically correct, crash-free, and memory safe. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardware to be correct. We extend the toolchain to verify the kernel-bypass framework and a NIC driver in the context of the NAT. We uncover bugs in both the framework and the driver. Our code is publicly available.
000264620 542__ $$fCC BY
000264620 6531_ $$aNetwork Functions
000264620 6531_ $$aSoftware Verification
000264620 6531_ $$aKernel Bypass 
000264620 700__ $$aPirelli, Solal
000264620 700__ $$aZaostrovnykh, Arseniy
000264620 700__ $$aCandea, George
000264620 7112_ $$aKBNets '18$$cBudapest, Hungary$$dAugust 20, 2018
000264620 773__ $$q8-14
000264620 8560_ $$fsolal.pirelli@epfl.ch
000264620 8564_ $$uhttps://infoscience.epfl.ch/record/264620/files/KBNets%20-%20CameraReady.pdf$$zFinal$$s573499
000264620 909C0 $$zGrolimund, Raphael$$xU11275$$pDSLAB$$mgeorge.candea@epfl.ch$$0252225
000264620 909CO $$qGLOBAL_SET$$pconf$$pIC$$ooai:infoscience.epfl.ch:264620
000264620 960__ $$asolal.pirelli@epfl.ch
000264620 961__ $$aalain.borel@epfl.ch
000264620 973__ $$aEPFL$$rREVIEWED
000264620 980__ $$aCONF
000264620 981__ $$aoverwrite