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.
Use this identifier to reference this record
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