Loading...
conference paper
A Formally Verified NAT Stack
Pirelli, Solal
•
Zaostrovnykh, Arseniy
•
Candea, George
August 20, 2018
KBNets'18: Proceedings of the 2018 Afternoon Workshop on Kernel Bypassing Networks
Prior 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.
Loading...
Name
KBNets - CameraReady.pdf
Type
Publisher's version
Access type
openaccess
License Condition
CC BY
Size
560.06 KB
Format
Adobe PDF
Checksum (MD5)
18fe6268cd3e374ba7e5d9e3529234d2