{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:58Z","timestamp":1750221298845,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T00:00:00Z","timestamp":1548633600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGCOMM Comput. Commun. Rev."],"published-print":{"date-parts":[[2019,1,28]]},"abstract":"<jats:p>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].<\/jats:p>","DOI":"10.1145\/3310165.3310176","type":"journal-article","created":{"date-parts":[[2019,1,29]],"date-time":"2019-01-29T13:16:22Z","timestamp":1548767782000},"page":"77-83","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A formally verified NAT stack"],"prefix":"10.1145","volume":"48","author":[{"given":"Solal","family":"Pirelli","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arseniy","family":"Zaostrovnykh","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George","family":"Candea","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,28]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"35","volume":"201","author":"Ball T.","journal-title":"TX"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"volume-title":"RWset: Attacking Path Explosion in Constraint-Based Test Generation. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08)","year":"2008","author":"Boonstoppel P.","key":"e_1_2_1_3_1"},{"volume-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI '08)","year":"2008","author":"Cadar C.","key":"e_1_2_1_4_1"},{"volume-title":"Data Plane Development Kit","year":"2018","author":"DPDK","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","unstructured":"DPDK bug 18: mmap with MAP_ANONYMOUS should have fd == -1: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=18. Accessed: 2018-04-01.  DPDK bug 18: mmap with MAP_ANONYMOUS should have fd == -1: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=18. Accessed: 2018-04-01."},{"key":"e_1_2_1_7_1","unstructured":"DPDK bug 19: Crash on initialization if first RTE_MAX_LCORE cores are disabled: https:\/\/dpdk.org\/tracker\/show_ bug. cgi ?id= 19. Accessed: 2018-04-01.  DPDK bug 19: Crash on initialization if first RTE_MAX_LCORE cores are disabled: https:\/\/dpdk.org\/tracker\/show_ bug. cgi ?id= 19. Accessed: 2018-04-01."},{"key":"e_1_2_1_8_1","unstructured":"DPDK bug 20: Undefined behavior caused by NUMA function in eal_memory: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=20. Accessed: 2018-04-01.  DPDK bug 20: Undefined behavior caused by NUMA function in eal_memory: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=20. Accessed: 2018-04-01."},{"key":"e_1_2_1_9_1","unstructured":"DPDK bug 21: Ixgbe driver changes FCTRL without first disabling RXCTRL.RXEN: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=21. Accessed: 2018-04-01.  DPDK bug 21: Ixgbe driver changes FCTRL without first disabling RXCTRL.RXEN: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=21. Accessed: 2018-04-01."},{"key":"e_1_2_1_10_1","unstructured":"DPDK bug 22: Ixgbe driver sets RDRXCTL with the wrong RSCACKC and FCOE_WRFIX values: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=22. Accessed: 2018-04-01.  DPDK bug 22: Ixgbe driver sets RDRXCTL with the wrong RSCACKC and FCOE_WRFIX values: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=22. Accessed: 2018-04-01."},{"key":"e_1_2_1_11_1","unstructured":"DPDK bug 23: Ixgbe driver writes to reserved bit in the EIMC register: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=23. Accessed: 2018-04-01.  DPDK bug 23: Ixgbe driver writes to reserved bit in the EIMC register: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=23. Accessed: 2018-04-01."},{"key":"e_1_2_1_12_1","unstructured":"DPDK bug 24: Ixgbe driver sets unknown bit of the 82599's SW_FW_SYNC register: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=24. Accessed: 2018-04-01.  DPDK bug 24: Ixgbe driver sets unknown bit of the 82599's SW_FW_SYNC register: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=24. Accessed: 2018-04-01."},{"key":"e_1_2_1_13_1","unstructured":"DPDK bug 25: Ixgbe driver sets TDH register after TXDCTL.ENABLE is set: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=25. Accessed: 2018-04-01.  DPDK bug 25: Ixgbe driver sets TDH register after TXDCTL.ENABLE is set: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=25. Accessed: 2018-04-01."},{"key":"e_1_2_1_14_1","unstructured":"DPDK bug 26: Ixgbe driver does not ensure FWSM firmware mode is valid before using it: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=26. Accessed: 2018-04-01.  DPDK bug 26: Ixgbe driver does not ensure FWSM firmware mode is valid before using it: https:\/\/dpdk.org\/tracker\/show_bug.cgi?id=26. Accessed: 2018-04-01."},{"key":"e_1_2_1_15_1","unstructured":"Intel\u00ae 82599 10 GbE Controller Datasheet: 2016. https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/datasheets\/82599-10-gbe-controller-datasheet.pdf. Accessed: 2018-02-12.  Intel\u00ae 82599 10 GbE Controller Datasheet: 2016. https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/datasheets\/82599-10-gbe-controller-datasheet.pdf. Accessed: 2018-02-12."},{"key":"e_1_2_1_16_1","unstructured":"Intel\u00ae Ethernet Controller I350 Datasheet: 2017. https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/datasheets\/ethernet-controller-i350-datasheet.pdf. Accessed: 2018-02-12.  Intel\u00ae Ethernet Controller I350 Datasheet: 2017. https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/datasheets\/ethernet-controller-i350-datasheet.pdf. Accessed: 2018-02-12."},{"volume-title":"Fast Verifier for C and Java. Third International Conference on NASA Formal Methods","year":"2011","author":"Jacobs B.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"volume-title":"Testing Closed-Source Binary Device Drivers with DDT. 2010 USENIX Annual Technical Conference","year":"2010","author":"Kuznetsov V.","key":"e_1_2_1_19_1"},{"volume-title":"LLVM and Clang: Next Generation Compiler Technology LLVM: Low Level Virtual Machine. The BSD Conference","year":"2008","author":"Lattner C.","key":"e_1_2_1_20_1"},{"volume-title":"Integrated Static Analysis for Linux Device Driver Verification. Integrated Formal Methods","year":"2007","author":"Post H.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","unstructured":"Release Notes - Data Plane Development Kit: 2018. https:\/\/dpdk.org\/doc\/guides\/rel_notes\/. Accessed: 2018-02-12.  Release Notes - Data Plane Development Kit: 2018. https:\/\/dpdk.org\/doc\/guides\/rel_notes\/. Accessed: 2018-02-12."},{"volume-title":"10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12)","year":"2012","author":"Renzelmann M.J.","key":"e_1_2_1_23_1"},{"volume-title":"Traditional IP Network Address Translator (Traditional NAT)","year":"2001","key":"e_1_2_1_24_1"},{"volume-title":"21st USENIX Security Symposium (USENIX Security '12)","year":"2012","author":"Rizzo L.","key":"e_1_2_1_25_1"},{"volume-title":"Snort: Lightweight Intrusion Detection for Networks. 13th Systems Administration Conference (LISA '99)","year":"1999","author":"Roesch M.","key":"e_1_2_1_26_1"},{"volume-title":"A Software NIC to Augment Hardware","year":"2015","author":"Soft NIC","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","unstructured":"VigNAT home repository - GitHub: https:\/\/github.com\/vignat\/vignat.  VigNAT home repository - GitHub: https:\/\/github.com\/vignat\/vignat."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"}],"container-title":["ACM SIGCOMM Computer Communication Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310165.3310176","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310165.3310176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:15Z","timestamp":1750212795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310165.3310176"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,28]]},"references-count":29,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,1,28]]}},"alternative-id":["10.1145\/3310165.3310176"],"URL":"https:\/\/doi.org\/10.1145\/3310165.3310176","relation":{},"ISSN":["0146-4833"],"issn-type":[{"type":"print","value":"0146-4833"}],"subject":[],"published":{"date-parts":[[2019,1,28]]},"assertion":[{"value":"2019-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}