A Formally Verified NAT Stack

Solal Pirelli, Arseniy Zaostrovnykh, George Candea
Abstract

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.

Download the full article

10 comments

  1. Pingback: fireman wood flag
  2. Pingback: Dresses For Women
  3. Pingback: 2019 bikini
  4. Pingback: prints promo
  5. Pingback: mommy blog
  6. Pingback: forum

Leave a Reply