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

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

Leave a Reply