{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:24:44Z","timestamp":1773192284642,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"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":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523708","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"31-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Hardening attack surfaces with formally proven binary format parsers"],"prefix":"10.1145","author":[{"given":"Nikhil","family":"Swamy","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Irina","family":"Spiridonova","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Haobin","family":"Ni","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Dmitry","family":"Malloy","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]},{"given":"Juan","family":"Vazquez","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]},{"given":"Michael","family":"Tang","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]},{"given":"Omar","family":"Cardona","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]},{"given":"Arti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Nail: A Practical Tool for Parsing and Generating Data Formats. login Usenix Mag., 40, 1","author":"Bangert Julian","year":"2015","unstructured":"Julian Bangert and Nickolai Zeldovich . 2015 . Nail: A Practical Tool for Parsing and Generating Data Formats. login Usenix Mag., 40, 1 (2015), https:\/\/www.usenix.org\/publications\/login\/feb15\/bangert Julian Bangert and Nickolai Zeldovich. 2015. Nail: A Practical Tool for Parsing and Generating Data Formats. login Usenix Mag., 40, 1 (2015), https:\/\/www.usenix.org\/publications\/login\/feb15\/bangert"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373836"},{"key":"e_1_3_2_1_3_1","volume-title":"Curing the Vulnerable Parser: Design Patterns for Secure Input Handling. login Usenix Mag., 42, 1","author":"Bratus Sergey","year":"2017","unstructured":"Sergey Bratus , Lars Hermerschmidt , Sven M. Hallberg , Michael E. Locasto , Falcon Momot , Meredith L. Patterson , and Anna Shubina . 2017. Curing the Vulnerable Parser: Design Patterns for Secure Input Handling. login Usenix Mag., 42, 1 ( 2017 ), https:\/\/www.usenix.org\/publications\/login\/spring2017\/bratus Sergey Bratus, Lars Hermerschmidt, Sven M. Hallberg, Michael E. Locasto, Falcon Momot, Meredith L. Patterson, and Anna Shubina. 2017. Curing the Vulnerable Parser: Design Patterns for Secure Input Handling. login Usenix Mag., 42, 1 (2017), https:\/\/www.usenix.org\/publications\/login\/spring2017\/bratus"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473599"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938556"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581483"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964011"},{"key":"e_1_3_2_1_9_1","first-page":"45","article-title":"Partial evaluation of computation process-an approach to a compiler-compiler. Systems, Computers","volume":"2","author":"Futamura Yoshihiko","year":"1971","unstructured":"Yoshihiko Futamura . 1971 . Partial evaluation of computation process-an approach to a compiler-compiler. Systems, Computers , Controls , 2 , 5 (1971), 45 \u2013 50 . https:\/\/ci.nii.ac.jp\/naid\/10000032872\/en\/ Yoshihiko Futamura. 1971. Partial evaluation of computation process-an approach to a compiler-compiler. Systems, Computers, Controls, 2, 5 (1971), 45\u201350. https:\/\/ci.nii.ac.jp\/naid\/10000032872\/en\/","journal-title":"Controls"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.24"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454053"},{"key":"e_1_3_2_1_13_1","volume-title":"tcp.h. https:\/\/elixir.bootlin.com\/linux\/v5.15.1\/source\/include\/linux\/tcp.h#L81","unstructured":"Linux. 2021. tcp.h. https:\/\/elixir.bootlin.com\/linux\/v5.15.1\/source\/include\/linux\/tcp.h#L81 Linux. 2021. tcp.h. https:\/\/elixir.bootlin.com\/linux\/v5.15.1\/source\/include\/linux\/tcp.h#L81"},{"key":"e_1_3_2_1_14_1","unstructured":"Linux. 2021. tcp_input.c. https:\/\/elixir.bootlin.com\/linux\/v5.15.1\/source\/net\/ipv4\/tcp_input.c#L4001  Linux. 2021. tcp_input.c. https:\/\/elixir.bootlin.com\/linux\/v5.15.1\/source\/net\/ipv4\/tcp_input.c#L4001"},{"key":"e_1_3_2_1_15_1","volume-title":"Quickstart: Create Intel SGX VM in the Azure portal. https:\/\/docs.microsoft.com\/en-us\/azure\/confidential-computing\/quick-create-portal","author":"Microsoft Corp.","year":"2021","unstructured":"Microsoft Corp. 2021 . Quickstart: Create Intel SGX VM in the Azure portal. https:\/\/docs.microsoft.com\/en-us\/azure\/confidential-computing\/quick-create-portal Microsoft Corp. 2021. Quickstart: Create Intel SGX VM in the Azure portal. https:\/\/docs.microsoft.com\/en-us\/azure\/confidential-computing\/quick-create-portal"},{"key":"e_1_3_2_1_16_1","unstructured":"Mitre Corp. 2020. Common Weakness Enumeration. https:\/\/cwe.mitre.org\/top25\/archive\/2020\/2020_cwe_top25.html  Mitre Corp. 2020. Common Weakness Enumeration. https:\/\/cwe.mitre.org\/top25\/archive\/2020\/2020_cwe_top25.html"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW50608.2020.00064"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Jon Postel. 1981. Transmission Control Protocol. https:\/\/datatracker.ietf.org\/doc\/html\/rfc793  Jon Postel. 1981. Transmission Control Protocol. https:\/\/datatracker.ietf.org\/doc\/html\/rfc793","DOI":"10.17487\/rfc0793"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 28th USENIX Conference on Security Symposium (USENIX Security 2019","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Nikhil Swamy , Tej Chajed , Nadim Kobeissi , and Jonathan Protzenko . 2019 . EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats . In Proceedings of the 28th USENIX Conference on Security Symposium (USENIX Security 2019 ). USENIX Association, USA. 1465\u20131482. isbn:978 1939133069 Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In Proceedings of the 28th USENIX Conference on Security Symposium (USENIX Security 2019). USENIX Association, USA. 1465\u20131482. isbn:9781939133069"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"E. Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. IETF RFC 8446. https:\/\/tools.ietf.org\/html\/rfc8446  E. Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. IETF RFC 8446. https:\/\/tools.ietf.org\/html\/rfc8446","DOI":"10.17487\/RFC8446"},{"key":"e_1_3_2_1_22_1","unstructured":"Mark Russinovich. 2021. Azure and AMD announce landmark in confidential computing evolution. https:\/\/azure.microsoft.com\/en-us\/blog\/azure-and-amd-enable-lift-and-shift-confidential-computing\/  Mark Russinovich. 2021. Azure and AMD announce landmark in confidential computing evolution. https:\/\/azure.microsoft.com\/en-us\/blog\/azure-and-amd-enable-lift-and-shift-confidential-computing\/"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031813"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_25_1","unstructured":"The Coq development team. 1989. The Coq proof assistant. http:\/\/coq.inria.fr  The Coq development team. 1989. The Coq proof assistant. http:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_26_1","volume-title":"26th USENIX Security Symposium (USENIX Security 17)","author":"Wang Pengfei","year":"2017","unstructured":"Pengfei Wang , Jens Krinke , Kai Lu , Gen Li , and Steve Dodier-Lazaro . 2017 . How Double-Fetch Situations turn into Double-Fetch Vulnerabilities: A Study of Double Fetches in the Linux Kernel . In 26th USENIX Security Symposium (USENIX Security 17) . USENIX Association, Vancouver, BC. 1\u201316. isbn:978-1-93 1971-40-9 https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/wang-pengfei Pengfei Wang, Jens Krinke, Kai Lu, Gen Li, and Steve Dodier-Lazaro. 2017. How Double-Fetch Situations turn into Double-Fetch Vulnerabilities: A Study of Double Fetches in the Linux Kernel. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC. 1\u201316. isbn:978-1-931971-40-9 https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/wang-pengfei"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294105"},{"key":"e_1_3_2_1_28_1","unstructured":"Young-X. 2019. Git commit. https:\/\/github.com\/torvalds\/linux\/commit\/9609dad263f8bea347f41fddca29353dbf8a7d37  Young-X. 2019. Git commit. https:\/\/github.com\/torvalds\/linux\/commit\/9609dad263f8bea347f41fddca29353dbf8a7d37"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523708","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523708","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523708"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":28,"alternative-id":["10.1145\/3519939.3523708","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523708","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}