{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:49:52Z","timestamp":1769734192475,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1512611 and CCF-1521584,"],"award-info":[{"award-number":["CCF-1512611 and CCF-1521584,"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0007"],"award-info":[{"award-number":["FA8750-16-C-0007"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>\n            It is a neat result from functional programming that libraries of\n            <jats:italic>parser combinators<\/jats:italic>\n            can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy \u2013 one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format specifications, covering all popular network packet formats and generating both decoders and encoders automatically. The catch is that we use the Coq proof assistant to derive both kinds of artifacts using tactics, automatically, in a way that guarantees that they form inverses of each other. We used our approach to reimplement packet processing for a full Internet protocol stack, inserting our replacement into the OCaml-based MirageOS unikernel, resulting in minimal performance degradation.\n          <\/jats:p>","DOI":"10.1145\/3341686","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Narcissus: correct-by-construction derivation of decoders and encoders from binary formats"],"prefix":"10.1145","volume":"3","author":[{"given":"Benjamin","family":"Delaware","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Sorawit","family":"Suriyakarn","sequence":"additional","affiliation":[{"name":"Band Protocol, Thailand"}]},{"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Qianchuan","family":"Ye","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2013a. CVE-2012-5965: Stack-based buffer overflow in the unique_service_name function in ssdp\/ssdp_server.c in the SSDP parser in the portable SDK for UPnP Devices 1.3.1 allows remote attackers to execute arbitrary code via a long DeviceType field in a UDP packet. (Jan. 2013). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2012- 5965  2013a. CVE-2012-5965: Stack-based buffer overflow in the unique_service_name function in ssdp\/ssdp_server.c in the SSDP parser in the portable SDK for UPnP Devices 1.3.1 allows remote attackers to execute arbitrary code via a long DeviceType field in a UDP packet. (Jan. 2013). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2012- 5965"},{"key":"e_1_2_2_2_1","unstructured":"2013b. CVE-2013-1203: Cisco ASA CX Context-Aware Security Software allows remote attackers to cause a denial of service (device reload) via crafted TCP packets that appear to have been forwarded by a Cisco Adaptive Security Appliances device. (May 2013). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2013- 1203  2013b. CVE-2013-1203: Cisco ASA CX Context-Aware Security Software allows remote attackers to cause a denial of service (device reload) via crafted TCP packets that appear to have been forwarded by a Cisco Adaptive Security Appliances device. (May 2013). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2013- 1203"},{"key":"e_1_2_2_3_1","unstructured":"2015. CVE-2015-0618: Cisco IOS XR 5.0.1 and 5.2.1 on Network Convergence System 6000 devices and 5.1.3 and 5.1.4 on Carrier Routing System X devices allows remote attackers to cause a denial of service via malformed IPv6 packets with extension headers. (Feb. 2015). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2015- 0618  2015. CVE-2015-0618: Cisco IOS XR 5.0.1 and 5.2.1 on Network Convergence System 6000 devices and 5.1.3 and 5.1.4 on Carrier Routing System X devices allows remote attackers to cause a denial of service via malformed IPv6 packets with extension headers. (Feb. 2015). https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2015- 0618"},{"key":"e_1_2_2_4_1","unstructured":"2016. CVE-2016-5080: Integer overflow in the rtxMemHeapAlloc function in asn1rt_a.lib in Objective Systems ASN1C for C\/C++ before 7.0.2 allows context-dependent attackers to execute arbitrary code or cause a denial of service on a system running an application compiled by ASN1C via crafted ASN.1 data. (July 2016). https:\/\/cve.mitre.org\/cgibin\/cvename.cgi?name=CVE- 2016- 5080  2016. CVE-2016-5080: Integer overflow in the rtxMemHeapAlloc function in asn1rt_a.lib in Objective Systems ASN1C for C\/C++ before 7.0.2 allows context-dependent attackers to execute arbitrary code or cause a denial of service on a system running an application compiled by ASN1C via crafted ASN.1 data. (July 2016). https:\/\/cve.mitre.org\/cgibin\/cvename.cgi?name=CVE- 2016- 5080"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088357"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009867"},{"key":"e_1_2_2_7_1","unstructured":"Apache Software Foundation. 2016. Apache Avro 1.8.0 Documentation. (2016). http:\/\/avro.apache.org\/docs\/current\/ {Accessed May 04 2016}.  Apache Software Foundation. 2016. Apache Avro 1.8.0 Documentation. (2016). http:\/\/avro.apache.org\/docs\/current\/ {Accessed May 04 2016}."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645435.652647"},{"key":"e_1_2_2_9_1","volume-title":"Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914","author":"Bangert Julian","year":"2014","unstructured":"Julian Bangert and Nickolai Zeldovich . 2014 . Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914 , Broomfield, CO, USA , October 6-8, 2014. 615\u2013628. https:\/\/www.usenix.org\/conference\/osdi14\/technical- sessions\/presentation\/bangert Julian Bangert and Nickolai Zeldovich. 2014. Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914, Broomfield, CO, USA, October 6-8, 2014. 615\u2013628. https:\/\/www.usenix.org\/conference\/osdi14\/technical- sessions\/presentation\/bangert"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_12"},{"key":"e_1_2_2_11_1","volume-title":"Certified Context-Free Parsing: A formalisation of Valiant\u2019s Algorithm in Agda. Logical Methods in Computer Science","author":"Bernardy Jean-Philippe","year":"2016","unstructured":"Jean-Philippe Bernardy and Patrik Jansson . 2016. Certified Context-Free Parsing: A formalisation of Valiant\u2019s Algorithm in Agda. Logical Methods in Computer Science Volume 12 , Issue 2 ( June 2016 ). Jean-Philippe Bernardy and Patrik Jansson. 2016. Certified Context-Free Parsing: A formalisation of Valiant\u2019s Algorithm in Agda. Logical Methods in Computer Science Volume 12, Issue 2 (June 2016)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502409.2502410"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_16_1","volume-title":"A constructive approach to the problem of program correctness. (Aug","author":"Dijkstra Edsger W.","year":"1967","unstructured":"Edsger W. Dijkstra . 1967. A constructive approach to the problem of program correctness. (Aug . 1967 ). http:\/\/www.cs. utexas.edu\/users\/EWD\/ewd02xx\/EWD209.PDF Circulated privately. Edsger W. Dijkstra. 1967. A constructive approach to the problem of program correctness. (Aug. 1967). http:\/\/www.cs. utexas.edu\/users\/EWD\/ewd02xx\/EWD209.PDF Circulated privately."},{"key":"e_1_2_2_17_1","volume-title":"Constructing Semantic Models of Programs with the Software Analysis Workbench","author":"Dockins Robert","unstructured":"Robert Dockins , Adam Foltzer , Joe Hendrix , Brian Huffman , Dylan McNamee , and Aaron Tomb . 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench . In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing , Cham , 56\u201372. Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing, Cham, 56\u201372."},{"key":"e_1_2_2_18_1","unstructured":"Olivier Dubuisson. 2001. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann.   Olivier Dubuisson. 2001. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065046"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111039"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411257"},{"key":"e_1_2_2_23_1","volume-title":"James","author":"Hardin Christopher S.","year":"2013","unstructured":"Christopher S. Hardin and Roshan P . James . 2013 . Core_bench: micro-benchmarking for OCaml . (2013). https:\/\/github. com\/janestreet\/core_bench Christopher S. Hardin and Roshan P. James. 2013. Core_bench: micro-benchmarking for OCaml. (2013). https:\/\/github. com\/janestreet\/core_bench"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983993"},{"key":"e_1_2_2_26_1","volume-title":"Yacc: Yet Another Compiler-Compiler. Technical Report.","author":"Johnson Stephen C.","year":"1979","unstructured":"Stephen C. Johnson . 1979 . Yacc: Yet Another Compiler-Compiler. Technical Report. Stephen C. Johnson. 1979. Yacc: Yet Another Compiler-Compiler. Technical Report."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005209"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158129"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2847538.2847544"},{"key":"e_1_2_2_32_1","volume-title":"TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2","author":"Koprowski Adam","year":"2011","unstructured":"Adam Koprowski and Henri Binsztok . 2011 . TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2 (2011). Adam Koprowski and Henri Binsztok. 2011. TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2 (2011)."},{"key":"e_1_2_2_33_1","volume-title":"Parsec: Direct style monadic parser combinators for the real world.","author":"Leijen Daan","year":"2001","unstructured":"Daan Leijen and Erik Meijer . 2001 . Parsec: Direct style monadic parser combinators for the real world. (2001). Daan Leijen and Erik Meijer. 2001. Parsec: Direct style monadic parser combinators for the real world. (2001)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234198"},{"key":"e_1_2_2_36_1","volume-title":"FliPpr: A System for Deriving Parsers from Pretty-Printers. New Generation Computing 36, 3 (01","author":"Matsuda Kazutaka","year":"2018","unstructured":"Kazutaka Matsuda and Meng Wang . 2018. FliPpr: A System for Deriving Parsers from Pretty-Printers. New Generation Computing 36, 3 (01 Jul 2018 ), 173\u2013202. Kazutaka Matsuda and Meng Wang. 2018. FliPpr: A System for Deriving Parsers from Pretty-Printers. New Generation Computing 36, 3 (01 Jul 2018), 173\u2013202."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/347059.347563"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158089"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1035"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_2_2_41_1","volume-title":"Mathematics of Program Construction","author":"Mu Shin-Cheng","unstructured":"Shin-Cheng Mu , Zhenjiang Hu , and Masato Takeichi . 2004. An Injective Language for Reversible Computation . In Mathematics of Program Construction , Dexter Kozen (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 289\u2013313. Shin-Cheng Mu, Zhenjiang Hu, and Masato Takeichi. 2004. An Injective Language for Reversible Computation. In Mathematics of Program Construction, Dexter Kozen (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 289\u2013313."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1177080.1177119"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250705"},{"key":"e_1_2_2_44_1","volume-title":"Smith","author":"Pavlovic Dusko","year":"2010","unstructured":"Dusko Pavlovic , Peter Pepper , and Douglas R . Smith . 2010 . Formal Derivation of Concurrent Garbage Collectors. In Mathematics of Program Construction. Springer Berlin Heidelberg , 353\u2013376. Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. 2010. Formal Derivation of Concurrent Garbage Collectors. In Mathematics of Program Construction. Springer Berlin Heidelberg, 353\u2013376."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863525"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_10"},{"key":"e_1_2_2_48_1","volume-title":"https:\/\/courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf","author":"Simmons Keith","year":"2016","unstructured":"Keith Simmons . 2016. Cheerios. ( 2016 ). https:\/\/courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf . Keith Simmons. 2016. Cheerios. (2016). https:\/\/courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf."},{"key":"e_1_2_2_49_1","volume-title":"Westfold","author":"Smith Douglas R.","year":"2008","unstructured":"Douglas R. Smith and Stephen J . Westfold . 2008 . Synthesis of Propositional Satisfiability Solvers . (2008). Douglas R. Smith and Stephen J. Westfold. 2008. Synthesis of Propositional Satisfiability Solvers. (2008)."},{"key":"e_1_2_2_50_1","volume-title":"Srinivas and Richard J\u00fcllig","author":"Yellamraju","year":"1995","unstructured":"Yellamraju V. Srinivas and Richard J\u00fcllig . 1995 . Specware : Formal support for composing software. In Mathematics of Program Construction, Bernhard M\u00f6ller (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg, 399\u2013422. Yellamraju V. Srinivas and Richard J\u00fcllig. 1995. Specware: Formal support for composing software. In Mathematics of Program Construction, Bernhard M\u00f6ller (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 399\u2013422."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1832"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9429-1"},{"key":"e_1_2_2_54_1","volume-title":"The Coq Proof Assistant, version 8.7.2. (Feb","author":"Development Team The Coq","year":"2018","unstructured":"The Coq Development Team . 2018. The Coq Proof Assistant, version 8.7.2. (Feb . 2018 ). The Coq Development Team. 2018. The Coq Proof Assistant, version 8.7.2. (Feb. 2018)."},{"key":"e_1_2_2_55_1","volume-title":"Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System","author":"Tullsen Mark","unstructured":"Mark Tullsen , Lee Pike , Nathan Collins , and Aaron Tomb . 2018. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , Cham , 413\u2013429. Mark Tullsen, Lee Pike, Nathan Collins, and Aaron Tomb. 2018. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 413\u2013429."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122979"},{"key":"e_1_2_2_57_1","unstructured":"Kenton Varda. 2008. Protocol Buffers. https:\/\/developers.google.com\/protocol-buffers\/. (2008).  Kenton Varda. 2008. Protocol Buffers. https:\/\/developers.google.com\/protocol-buffers\/. (2008)."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863548"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294105"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341686","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341686","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341686","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:29Z","timestamp":1750200089000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341686"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":59,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341686"],"URL":"https:\/\/doi.org\/10.1145\/3341686","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}