{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T16:54:16Z","timestamp":1769532856180,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T00:00:00Z","timestamp":1533600000000},"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":[],"published-print":{"date-parts":[[2018,8,7]]},"DOI":"10.1145\/3229538.3229540","type":"proceedings-article","created":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T19:07:07Z","timestamp":1533150427000},"page":"8-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A Formally Verified NAT Stack"],"prefix":"10.1145","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":[[2018,8,7]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"35","volume":"201","author":"Ball T.","unstructured":"Ball , T. , Bounimova , E. , Kumar , R. and Levin , V. 2010. SLAM2: Static driver verification with under 4% false alarms. Formal Methods in Computer Aided Design (FMCAD '10) (Austin , TX , 201 0), 35 -- 42 . Ball, T., Bounimova, E., Kumar, R. and Levin, V. 2010. SLAM2: Static driver verification with under 4% false alarms. Formal Methods in Computer Aided Design (FMCAD '10) (Austin, TX, 2010), 35--42.","journal-title":"TX"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_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","unstructured":"Boonstoppel , P. , Cadar , C. and Engler , D . 2008 . RWset: Attacking Path Explosion in Constraint-Based Test Generation. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08) (Berlin, Heidelberg , 2008 ), 351--366. Boonstoppel, P., Cadar, C. and Engler, D. 2008. RWset: Attacking Path Explosion in Constraint-Based Test Generation. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08) (Berlin, Heidelberg, 2008), 351--366."},{"key":"e_1_3_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","unstructured":"Cadar , C. , Dunbar , D. and Engler , D.R . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI '08) (Berkeley, CA, USA, 2008 ), 209--224. Cadar, C., Dunbar, D. and Engler, D.R. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI '08) (Berkeley, CA, USA, 2008), 209--224."},{"key":"e_1_3_2_1_5_1","volume-title":"Data Plane Development Kit","author":"DPDK","year":"2018","unstructured":"DPDK : Data Plane Development Kit : 2018 . http:\/\/dpdk.org\/. Accessed : 2018-02-12. DPDK: Data Plane Development Kit: 2018. http:\/\/dpdk.org\/. Accessed: 2018-02-12."},{"key":"e_1_3_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_3_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_3_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_3_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_3_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_3_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_3_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_3_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_3_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_3_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_3_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_3_2_1_17_1","volume-title":"Fast Verifier for C and Java. Third International Conference on NASA Formal Methods","author":"Jacobs B.","year":"2011","unstructured":"Jacobs , B. , Smans , J. , Philippaerts , P. , Vogels , F. , Penninckx , W. and Piessens , F . 2011. VeriFast: A Powerful, Sound, Predictable , Fast Verifier for C and Java. Third International Conference on NASA Formal Methods ( Berlin, Heidelberg , 2011 ), 41--55. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W. and Piessens, F. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. Third International Conference on NASA Formal Methods (Berlin, Heidelberg, 2011), 41--55."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_19_1","volume-title":"Testing Closed-Source Binary Device Drivers with DDT. 2010 USENIX Annual Technical Conference","author":"Kuznetsov V.","year":"2010","unstructured":"Kuznetsov , V. , Chipounov , V. and Candea , G . 2010 . Testing Closed-Source Binary Device Drivers with DDT. 2010 USENIX Annual Technical Conference ( Berkeley, CA, USA , 2010 ), 12. Kuznetsov, V., Chipounov, V. and Candea, G. 2010. Testing Closed-Source Binary Device Drivers with DDT. 2010 USENIX Annual Technical Conference (Berkeley, CA, USA, 2010), 12."},{"key":"e_1_3_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","unstructured":"Lattner , C. 2008 . LLVM and Clang: Next Generation Compiler Technology LLVM: Low Level Virtual Machine. The BSD Conference (2008). Lattner, C. 2008. LLVM and Clang: Next Generation Compiler Technology LLVM: Low Level Virtual Machine. The BSD Conference (2008)."},{"key":"e_1_3_2_1_21_1","volume-title":"Integrated Static Analysis for Linux Device Driver Verification. Integrated Formal Methods","author":"Post H.","year":"2007","unstructured":"Post , H. and K\u00fcchlin , W . 2007 . Integrated Static Analysis for Linux Device Driver Verification. Integrated Formal Methods ( Berlin, Heidelberg , 2007 ), 518--537. Post, H. and K\u00fcchlin, W. 2007. Integrated Static Analysis for Linux Device Driver Verification. Integrated Formal Methods (Berlin, Heidelberg, 2007), 518--537."},{"key":"e_1_3_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_3_2_1_23_1","volume-title":"10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12)","author":"Renzelmann M.J.","year":"2012","unstructured":"Renzelmann , M.J. , Kadav , A. and Swift , M.M . 2012. SymDrive: Testing Drivers without Devices . 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12) (Hollywood, CA, 2012 ), 279--292. Renzelmann, M.J., Kadav, A. and Swift, M.M. 2012. SymDrive: Testing Drivers without Devices. 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI '12) (Hollywood, CA, 2012), 279--292."},{"key":"e_1_3_2_1_24_1","volume-title":"Traditional IP Network Address Translator (Traditional NAT)","year":"2001","unstructured":"RFC 3022 : Traditional IP Network Address Translator (Traditional NAT) : 2001 . https:\/\/www.ietf.org\/rfc\/rfc3022.txt. Accessed : 2018-02-12. RFC 3022: Traditional IP Network Address Translator (Traditional NAT): 2001. https:\/\/www.ietf.org\/rfc\/rfc3022.txt. Accessed: 2018-02-12."},{"key":"e_1_3_2_1_25_1","volume-title":"21st USENIX Security Symposium (USENIX Security '12)","author":"Rizzo L.","year":"2012","unstructured":"Rizzo , L. 2012 . NetMap: A novel framework for fast packet I\/ O . 21st USENIX Security Symposium (USENIX Security '12) (2012), 101--112. Rizzo, L. 2012. NetMap: A novel framework for fast packet I\/ O. 21st USENIX Security Symposium (USENIX Security '12) (2012), 101--112."},{"key":"e_1_3_2_1_26_1","volume-title":"Snort: Lightweight Intrusion Detection for Networks. 13th Systems Administration Conference (LISA '99)","author":"Roesch M.","year":"1999","unstructured":"Roesch , M. 1999 . Snort: Lightweight Intrusion Detection for Networks. 13th Systems Administration Conference (LISA '99) (1999), 229--238. Roesch, M. 1999. Snort: Lightweight Intrusion Detection for Networks. 13th Systems Administration Conference (LISA '99) (1999), 229--238."},{"key":"e_1_3_2_1_27_1","volume-title":"A Software NIC to Augment Hardware","author":"Soft NIC","year":"2015","unstructured":"Soft NIC : A Software NIC to Augment Hardware : 2015 . http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2015\/EECS-2015-155.html. SoftNIC: A Software NIC to Augment Hardware: 2015. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2015\/EECS-2015-155.html."},{"key":"e_1_3_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_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"}],"event":{"name":"SIGCOMM '18: ACM SIGCOMM 2018 Conference","location":"Budapest Hungary","acronym":"SIGCOMM '18","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 2018 Afternoon Workshop on Kernel Bypassing Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229538.3229540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3229538.3229540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:43Z","timestamp":1750210783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229538.3229540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,7]]},"references-count":29,"alternative-id":["10.1145\/3229538.3229540","10.1145\/3229538"],"URL":"https:\/\/doi.org\/10.1145\/3229538.3229540","relation":{},"subject":[],"published":{"date-parts":[[2018,8,7]]},"assertion":[{"value":"2018-08-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}