A Formally Verified NAT Stack

Solal Pirelli, Arseniy Zaostrovnykh, George Candea

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


  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
  7. Pingback: tor onion websites
  8. Pingback: dark web directory
  9. Pingback: Barcatoto
  10. Pingback: istanbul escort
  11. Pingback: bestwaytolearn
  12. Pingback: tree service
  13. Pingback: metal prints

Leave a Reply