A Formally Verified NAT Stack

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.


Publié dans:
8-14
Présenté à:
KBNets '18, Budapest, Hungary, August 20, 2018
Année
Aug 20 2018
Mots-clefs:
Autres identifiants:
Laboratoires:




 Notice créée le 2019-03-08, modifiée le 2019-03-16

Final:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)