Pirelli, SolalZaostrovnykh, ArseniyCandea, George2019-06-182019-06-182019-06-182018-10-0110.1145/3310165.3310176https://infoscience.epfl.ch/handle/20.500.14299/156908WOS:000457161300010Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. 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 [28].Computer Science, Information SystemsComputer Sciencenetwork functionssoftware verificationkernel bypasstext::journal::journal article::research article