Pirelli, SolalZaostrovnykh, ArseniyCandea, George2019-03-082019-03-082019-03-082018-08-2010.1145/3229538.3229540https://infoscience.epfl.ch/handle/20.500.14299/155291Prior 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.Network FunctionsSoftware VerificationKernel Bypasstext::conference output::conference proceedings::conference paper