Loading...
research article
A Formally Verified NAT Stack
October 1, 2018
Prior 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].
Use this identifier to reference this record
Type
research article
Web of Science ID
WOS:000457161300010
Authors
Publication date
2018-10-01
Publisher
Published in
Volume
48
Issue
5
Start page
77
End page
83
Note
ACM SIGCOMM Workshop on Kernel-Bypassing Networks (KBNets), Budapest, HUNGARY, Aug 20-24, 2018
Peer reviewed
REVIEWED
EPFL units
Available on Infoscience
June 18, 2019