{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:11:17Z","timestamp":1773277877132,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,7]],"date-time":"2017-08-07T00:00:00Z","timestamp":1502064000000},"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":[[2017,8,7]]},"DOI":"10.1145\/3098822.3098833","type":"proceedings-article","created":{"date-parts":[[2017,8,4]],"date-time":"2017-08-04T13:48:54Z","timestamp":1501854534000},"page":"141-154","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["A Formally Verified NAT"],"prefix":"10.1145","author":[{"given":"Arseniy","family":"Zaostrovnykh","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Solal","family":"Pirelli","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luis","family":"Pedrosa","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katerina","family":"Argyraki","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":[[2017,8,7]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Formal Methods for Components and Objects","author":"Barnett M.","year":"2005","unstructured":"Barnett , M. , Chang , B.-Y. E. , DeLine , R. , Jacobs , B. , and Leino , K. R. M . Boogie: A Modular Reusable Verifier for Object-Oriented Programs . In Formal Methods for Components and Objects ( 2005 ). Barnett, M., Chang, B.-Y. E., DeLine, R., Jacobs, B., and Leino, K. R. M. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects (2005)."},{"key":"e_1_3_2_2_2_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symp.","author":"Beringer L.","year":"2015","unstructured":"Beringer , L. , Petcher , A. , Katherine , Q. Y. , and Appel , A. W . Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symp. ( 2015 ). Beringer, L., Petcher, A., Katherine, Q. Y., and Appel, A. W. Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symp. (2015)."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1090191.1080123"},{"key":"e_1_3_2_2_4_1","volume-title":"Automatic Proof and Disproof in Isabelle\/HOL. Frontiers of Combining Systems","author":"Blanchette J.","year":"2011","unstructured":"Blanchette , J. , Bulwahn , L. , and Nipkow , T . Automatic Proof and Disproof in Isabelle\/HOL. Frontiers of Combining Systems ( 2011 ). Blanchette, J., Bulwahn, L., and Nipkow, T. Automatic Proof and Disproof in Isabelle\/HOL. Frontiers of Combining Systems (2011)."},{"key":"e_1_3_2_2_5_1","volume-title":"Seminar on Network Protocols in Operating Systems","author":"Boye M.","year":"2013","unstructured":"Boye , M. Netfilter Connection Tracking and NAT Implementation . In Seminar on Network Protocols in Operating Systems ( 2013 ). Boye, M. Netfilter Connection Tracking and NAT Implementation. In Seminar on Network Protocols in Operating Systems (2013)."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_2_7_1","volume-title":"RFC Editor","author":"Bradner S.","year":"1999","unstructured":"Bradner , S. , and McQaid , J. Benchmarking Methodology for Network Interconnect Devices. RFC 2544 , RFC Editor , 1999 . Bradner, S., and McQaid, J. Benchmarking Methodology for Network Interconnect Devices. RFC 2544, RFC Editor, 1999."},{"key":"e_1_3_2_2_8_1","unstructured":"Brocade Vyatta Network OS. http:\/\/www.brocade.com\/en\/products-services\/software-networking\/network-functions-virtualization\/vyatta-network-os.html. Accessed: 2017-01-24.  Brocade Vyatta Network OS. http:\/\/www.brocade.com\/en\/products-services\/software-networking\/network-functions-virtualization\/vyatta-network-os.html. Accessed: 2017-01-24."},{"key":"e_1_3_2_2_9_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Symp. on Operating Sys. Design and Implem.","author":"Cadar C.","year":"2008","unstructured":"Cadar , C. , Dunbar , D. , Engler , D. R. , KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Symp. on Operating Sys. Design and Implem. ( 2008 ). Cadar, C., Dunbar, D., Engler, D. R., et al. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Symp. on Operating Sys. Design and Implem. (2008)."},{"key":"e_1_3_2_2_10_1","volume-title":"Symp. on Networked Systems Design and Implem.","author":"Canini M.","year":"2012","unstructured":"Canini , M. , Venzano , D. , Pere\u0161\u00edni , P. , Kosti\u0107 , D. , and Rexford , J . A NICE Way to Test OpenFlow Applications . In Symp. on Networked Systems Design and Implem. ( 2012 ). Canini, M., Venzano, D., Pere\u0161\u00edni, P., Kosti\u0107, D., and Rexford, J. A NICE Way to Test OpenFlow Applications. In Symp. on Networked Systems Design and Implem. (2012)."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993526"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"e_1_3_2_2_15_1","volume-title":"CVE-ID CVE-2013-1138.","year":"2013","unstructured":"CVE-2013-1138. Available from CVE Details , CVE-ID CVE-2013-1138. , 2013 . CVE-2013-1138. Available from CVE Details, CVE-ID CVE-2013-1138., 2013."},{"key":"e_1_3_2_2_16_1","volume-title":"CVE-ID CVE-2014-3817.","year":"2014","unstructured":"CVE-2014-3817. Available from CVE Details , CVE-ID CVE-2014-3817. , 2014 . CVE-2014-3817. Available from CVE Details, CVE-ID CVE-2014-3817., 2014."},{"key":"e_1_3_2_2_17_1","volume-title":"CVE-ID CVE-2015-6271.","year":"2015","unstructured":"CVE-2015-6271. Available from CVE Details , CVE-ID CVE-2015-6271. , 2015 . CVE-2015-6271. Available from CVE Details, CVE-ID CVE-2015-6271., 2015."},{"key":"e_1_3_2_2_18_1","volume-title":"CVE-ID CVE-2014-9715.","year":"2014","unstructured":"CVE-2014-9715. Available from CVE Details , CVE-ID CVE-2014-9715. , 2014 . CVE-2014-9715. Available from CVE Details, CVE-ID CVE-2014-9715., 2014."},{"key":"e_1_3_2_2_19_1","volume-title":"Software Dataplane Verification. In Symp. on Networked Systems Design and Implem.","author":"Dobrescu M.","year":"2014","unstructured":"Dobrescu , M. , and Argyraki , K . Software Dataplane Verification. In Symp. on Networked Systems Design and Implem. ( 2014 ). Dobrescu, M., and Argyraki, K. Software Dataplane Verification. In Symp. on Networked Systems Design and Implem. (2014)."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629578"},{"key":"e_1_3_2_2_21_1","unstructured":"Data Plane Development Kit. http:\/\/dpdk.org. Accessed: 2017-06-16.  Data Plane Development Kit. http:\/\/dpdk.org. Accessed: 2017-06-16."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815675.2815692"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_2_2_24_1","volume-title":"BUZZ: Testing Context-Dependent Policies in Stateful Networks. In Symp. on Networked Systems Design and Implem.","author":"Fayaz S. K.","year":"2016","unstructured":"Fayaz , S. K. , Yu , T. , Tobioka , Y. , Chaki , S. , and Sekar , V . BUZZ: Testing Context-Dependent Policies in Stateful Networks. In Symp. on Networked Systems Design and Implem. ( 2016 ). Fayaz, S. K., Yu, T., Tobioka, Y., Chaki, S., and Sekar, V. BUZZ: Testing Context-Dependent Policies in Stateful Networks. In Symp. on Networked Systems Design and Implem. (2016)."},{"key":"e_1_3_2_2_25_1","volume-title":"Symp. on Networked Systems Design and Implem.","author":"Fogel A.","year":"2015","unstructured":"Fogel , A. , Fung , S. , Pedrosa , L. , Walraed-Sullivan , M. , Govindan , R. , Mahajan , R. , and Millstein , T . A General Approach to Network Configuration Analysis . In Symp. on Networked Systems Design and Implem. ( 2015 ). Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., and Millstein, T. A General Approach to Network Configuration Analysis. In Symp. on Networked Systems Design and Implem. (2015)."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.231144"},{"key":"e_1_3_2_2_29_1","volume-title":"Netfilter Project","author":"Kadlecsik J.","year":"2004","unstructured":"Kadlecsik , J. , and P\u00e1sztor , G . Netfilter Performance Testing. Tech. rep ., Netfilter Project , Berlin, Germany , 2004 . Kadlecsik, J., and P\u00e1sztor, G. Netfilter Performance Testing. Tech. rep., Netfilter Project, Berlin, Germany, 2004."},{"key":"e_1_3_2_2_30_1","volume-title":"Real Time Network Policy Checking Using Header Space Analysis. In Symp. on Networked Systems Design and Implem.","author":"Kazemian P.","year":"2013","unstructured":"Kazemian , P. , Chan , M. , Zeng , H. , Varghese , G. , McKeown , N. , and Whyte , S . Real Time Network Policy Checking Using Header Space Analysis. In Symp. on Networked Systems Design and Implem. ( 2013 ). Kazemian, P., Chan, M., Zeng, H., Varghese, G., McKeown, N., and Whyte, S. Real Time Network Policy Checking Using Header Space Analysis. In Symp. on Networked Systems Design and Implem. (2013)."},{"key":"e_1_3_2_2_31_1","volume-title":"N. Header Space Analysis: Static Checking For Networks. In Symp. on Networked Systems Design and Implem.","author":"Kazemian P.","year":"2012","unstructured":"Kazemian , P. , Varghese , G. , and McKeown , N. Header Space Analysis: Static Checking For Networks. In Symp. on Networked Systems Design and Implem. ( 2012 ). Kazemian, P., Varghese, G., and McKeown, N. Header Space Analysis: Static Checking For Networks. In Symp. on Networked Systems Design and Implem. (2012)."},{"key":"e_1_3_2_2_32_1","volume-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time. In Symp. on Networked Systems Design and Implem.","author":"Khurshid A.","year":"2013","unstructured":"Khurshid , A. , Zou , X. , Zhou , W. , Caesar , M. , and Godfrey , P. B . VeriFlow: Verifying Network-Wide Invariants in Real Time. In Symp. on Networked Systems Design and Implem. ( 2013 ). Khurshid, A., Zou, X., Zhou, W., Caesar, M., and Godfrey, P. B. VeriFlow: Verifying Network-Wide Invariants in Real Time. In Symp. on Networked Systems Design and Implem. (2013)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_34_1","volume-title":"Symp. on Operating Systems Principles","author":"Klein G.","year":"2009","unstructured":"Klein , G. , Elphinstone , K. , Heiser , G. , Andronick , J. , Cock , D. , Derrin , P. , Elkaduwe , D. , Engelhardt , K. , Kolanski , R. , Norrish , M. , : Formal Verification of an OS Kernel . In Symp. on Operating Systems Principles ( 2009 ). Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al. seL4: Formal Verification of an OS Kernel. In Symp. on Operating Systems Principles (2009)."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/354871.354874"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413207"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/508791.508972"},{"key":"e_1_3_2_2_38_1","volume-title":"Checking Beliefs in Dynamic Networks. In Symp. on Networked Systems Design and Implem.","author":"Lopes N. P.","year":"2015","unstructured":"Lopes , N. P. , Bj\u00f8rner , N. , Godefroid , P. , Jayaraman , K. , and Varghese , G . Checking Beliefs in Dynamic Networks. In Symp. on Networked Systems Design and Implem. ( 2015 ). Lopes, N. P., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., and Varghese, G. Checking Beliefs in Dynamic Networks. In Symp. on Networked Systems Design and Implem. (2015)."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_2_40_1","volume-title":"CVE-ID MS13-064.","year":"2013","unstructured":"MS13-064. Available from CVE Details , CVE-ID MS13-064. , 2013 . MS13-064. Available from CVE Details, CVE-ID MS13-064., 2013."},{"key":"e_1_3_2_2_41_1","volume-title":"Model Checking Large Network Protocol Implementations. In Symp. on Networked Systems Design and Implem.","volume":"4","author":"Musuvathi M.","year":"2004","unstructured":"Musuvathi , M. , Engler , D. R. , Model Checking Large Network Protocol Implementations. In Symp. on Networked Systems Design and Implem. ( 2004 ), vol. 4 . Musuvathi, M., Engler, D. R., et al. Model Checking Large Network Protocol Implementations. In Symp. on Networked Systems Design and Implem. (2004), vol. 4."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542504"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806651.1806657"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_2_46_1","volume-title":"Verifying Reachability in Networks with Mutable Datapaths. In Symp. on Networked Systems Design and Implem.","author":"Panda A.","year":"2017","unstructured":"Panda , A. , Lahav , O. , Argyraki , K. , Sagiv , M. , and Shenker , S . Verifying Reachability in Networks with Mutable Datapaths. In Symp. on Networked Systems Design and Implem. ( 2017 ). Panda, A., Lahav, O., Argyraki, K., Sagiv, M., and Shenker, S. Verifying Reachability in Networks with Mutable Datapaths. In Symp. on Networked Systems Design and Implem. (2017)."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1041685.1029901"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Postel J. Discard Protocol. RFC 863 RFC Editor 1983.  Postel J. Discard Protocol. RFC 863 RFC Editor 1983.","DOI":"10.17487\/rfc0863"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098583.3098590"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233835"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_2_52_1","volume-title":"Symp. on Networked Systems Design and Implem.","author":"Ryzhyk L.","year":"2017","unstructured":"Ryzhyk , L. , Bj\u00f8rner , N. , Canini , M. , Jeannin , J.-B. , Schlesinger , C. , Terry , D. B. , and Varghese , G . Correct by Construction Networks Using Stepwise Refinement . In Symp. on Networked Systems Design and Implem. ( 2017 ). Ryzhyk, L., Bj\u00f8rner, N., Canini, M., Jeannin, J.-B., Schlesinger, C., Terry, D. B., and Varghese, G. Correct by Construction Networks Using Stepwise Refinement. In Symp. on Networked Systems Design and Implem. (2017)."},{"key":"e_1_3_2_2_53_1","volume-title":"RFC Editor","author":"Srisuresh P.","year":"2001","unstructured":"Srisuresh , P. , and Egevang , K . Traditional IP Network Address Translator (Traditional NAT). RFC 3022 , RFC Editor , 2001 . Srisuresh, P., and Egevang, K. Traditional IP Network Address Translator (Traditional NAT). RFC 3022, RFC Editor, 2001."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676985"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_2_56_1","first-page":"1","volume":"36","author":"Tange O. GNU","year":"2011","unstructured":"Tange , O. GNU Parallel - The Command-Line Power Tool.; login : The USENIX Magazine 36 , 1 ( 2011 ). Tange, O. GNU Parallel - The Command-Line Power Tool.; login: The USENIX Magazine 36, 1 (2011).","journal-title":"The USENIX Magazine"},{"key":"e_1_3_2_2_57_1","unstructured":"Clang 5 documentation - UndefinedBehaviorSanitizer - Available checks. https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html#available-checks. Accessed: 2017-01-24.  Clang 5 documentation - UndefinedBehaviorSanitizer - Available checks. https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html#available-checks. Accessed: 2017-01-24."},{"key":"e_1_3_2_2_58_1","volume-title":"https:\/\/vignat.github.io","author":"Vig NAT","year":"2017","unstructured":"Vig NAT Project Repository . https:\/\/vignat.github.io , 2017 . VigNAT Project Repository. https:\/\/vignat.github.io, 2017."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_3_2_2_60_1","volume-title":"Feb.","author":"Zaostrovnykh A.","year":"2016","unstructured":"Zaostrovnykh , A. , Argyraki , K. , and Candea , G . Nework software verification survey. https:\/\/vignat.github.io\/survey , Feb. 2016 . Zaostrovnykh, A., Argyraki, K., and Candea, G. Nework software verification survey. https:\/\/vignat.github.io\/survey, Feb. 2016."}],"event":{"name":"SIGCOMM '17: ACM SIGCOMM 2017 Conference","location":"Los Angeles CA USA","acronym":"SIGCOMM '17","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the Conference of the ACM Special Interest Group on Data Communication"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3098822.3098833","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3098822.3098833","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:07:21Z","timestamp":1750273641000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3098822.3098833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,7]]},"references-count":59,"alternative-id":["10.1145\/3098822.3098833","10.1145\/3098822"],"URL":"https:\/\/doi.org\/10.1145\/3098822.3098833","relation":{},"subject":[],"published":{"date-parts":[[2017,8,7]]},"assertion":[{"value":"2017-08-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}