{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T05:18:17Z","timestamp":1672636697284},"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":"http:\/\/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":"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":"http:\/\/dx.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"}]},{"given":"Arseniy","family":"Zaostrovnykh","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"George","family":"Candea","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]}],"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"},{"key":"e_1_2_1_3_1","volume-title":"RWset: Attacking Path Explosion in Constraint-Based Test Generation. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08)","author":"Boonstoppel P.","year":"2008"},{"key":"e_1_2_1_4_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)","author":"Cadar C.","year":"2008"},{"key":"e_1_2_1_5_1","volume-title":"Data Plane Development Kit","author":"DPDK","year":"2018"},{"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."},{"key":"e_1_2_1_17_1","volume-title":"Fast Verifier for C and Java. Third International Conference on NASA Formal Methods","author":"Jacobs B.","year":"2011"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_19_1","volume-title":"Testing Closed-Source Binary Device Drivers with DDT. 2010 USENIX Annual Technical Conference","author":"Kuznetsov V.","year":"2010"},{"key":"e_1_2_1_20_1","volume-title":"LLVM and Clang: Next Generation Compiler Technology LLVM: Low Level Virtual Machine. The BSD Conference","author":"Lattner C.","year":"2008"},{"key":"e_1_2_1_21_1","volume-title":"Integrated Static Analysis for Linux Device Driver Verification. Integrated Formal Methods","author":"Post H.","year":"2007"},{"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."},{"key":"e_1_2_1_23_1","volume-title":"10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12)","author":"Renzelmann M.J.","year":"2012"},{"key":"e_1_2_1_24_1","volume-title":"Traditional IP Network Address Translator (Traditional NAT)","year":"2001"},{"key":"e_1_2_1_25_1","volume-title":"21st USENIX Security Symposium (USENIX Security '12)","author":"Rizzo L.","year":"2012"},{"key":"e_1_2_1_26_1","volume-title":"Snort: Lightweight Intrusion Detection for Networks. 13th Systems Administration Conference (LISA '99)","author":"Roesch M.","year":"1999"},{"key":"e_1_2_1_27_1","volume-title":"A Software NIC to Augment Hardware","author":"Soft NIC","year":"2015"},{"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\/pdf\/10.1145\/3310165.3310176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T10:19:07Z","timestamp":1672568347000},"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":[{"value":"0146-4833","type":"print"}],"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"}}]}}