{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:53Z","timestamp":1775873513623,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T00:00:00Z","timestamp":1733702400000},"content-version":"vor","delay-in-days":7,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["N66001-21-C-4028 \/ W912CG-23-C-0024"],"award-info":[{"award-number":["N66001-21-C-4028 \/ W912CG-23-C-0024"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690244","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"2786-2798","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6625-1123","authenticated-orcid":false,"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Open University & Virginia Tech, Heerlen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3442-1543","authenticated-orcid":false,"given":"Nico","family":"Naus","sequence":"additional","affiliation":[{"name":"Open University, Heerlen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8663-739X","authenticated-orcid":false,"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008."},{"key":"e_1_3_2_1_2_1","first-page":"250","volume-title":"Rastislav Bodik","author":"Balakrishnan Gogul","year":"2005","unstructured":"Gogul Balakrishnan, Radu Gruian, Thomas Reps, and Tim Teitelbaum. Codesurfer\/x86'a platform for analyzing x86 executables. In Rastislav Bodik, editor, Compiler Construction, pages 250--254, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1454115.1454128"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966913.1966919"},{"key":"e_1_3_2_1_5_1","first-page":"353","volume-title":"Proceedings of the 22th USENIX Security Symposium","author":"Brumley David","year":"2013","unstructured":"David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring. In Samuel T. King, editor, Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14--16, 2013, pages 353--368. USENIX Association, 2013."},{"key":"e_1_3_2_1_6_1","first-page":"385","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Carlini Nicholas","year":"2014","unstructured":"Nicholas Carlini and David Wagner. ROP is still dangerous: Breaking modern defenses. In 23rd USENIX Security Symposium (USENIX Security 14), pages 385--399, 2014."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250706"},{"key":"e_1_3_2_1_8_1","first-page":"153","volume-title":"Installing and using NASM. Guide to Assembly Language Programming in Linux","author":"Dandamudi Sivarama P","year":"2005","unstructured":"Sivarama P Dandamudi. Installing and using NASM. Guide to Assembly Language Programming in Linux, pages 153--166, 2005."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.005"},{"key":"e_1_3_2_1_11_1","volume-title":"ReCon 2014 Conference","author":"Dinaburg Artem","year":"2014","unstructured":"Artem Dinaburg and Andrew Ruef. McSema: Static translation of x86 instructions to LLVM. In ReCon 2014 Conference, Montreal, Canada, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385972"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2011.49"},{"key":"e_1_3_2_1_14_1","unstructured":"Shilpi Goel. Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. PhD thesis The University of Texas at Austin 2016."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/23.3.223"},{"key":"e_1_3_2_1_16_1","first-page":"613","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Huang Yongzhe","year":"2022","unstructured":"Yongzhe Huang, Vikram Narayanan, David Detweiler, Kaiming Huang, Gang Tan, Trent Jaeger, and Anton Burtsev. KSplit: Automating device driver isolation. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 613--631, Carlsbad, CA, July 2022. USENIX Association."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2983996"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497776.3517776"},{"key":"e_1_3_2_1_20_1","volume-title":"July 2018","author":"Kroustek Jakub","year":"2017","unstructured":"Jakub Kroustek, Peter Matula, and P Zemek. RetDec: An open-source machine-code decompiler. In July 2018, 2017."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9360-2"},{"key":"e_1_3_2_1_23_1","volume-title":"System V Application Binary Interface AMD64 Architecture Processor Supplement","author":"Matz Michael","year":"2012","unstructured":"Michael Matz, Jan Hubicka, Andreas Jaeger, and Mark Mitchell. System V Application Binary Interface AMD64 Architecture Processor Supplement, 2012."},{"key":"e_1_3_2_1_24_1","first-page":"208","volume-title":"European Symposium on Programming","author":"Mycroft Alan","year":"1999","unstructured":"Alan Mycroft. Type-based decompilation (or program reconstruction via type reconstruction). In European Symposium on Programming, pages 208--223. Springer, 1999."},{"key":"e_1_3_2_1_25_1","first-page":"78","volume-title":"2012 Formal Methods in Computer-Aided Design (FMCAD)","author":"Myreen Magnus O.","year":"2012","unstructured":"Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. Decompilation into logic -- improved. In 2012 Formal Methods in Computer-Aided Design (FMCAD), pages 78--81. IEEE, 2012."},{"key":"e_1_3_2_1_26_1","first-page":"699","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Narayan Shravan","year":"2020","unstructured":"Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. Retrofitting fine grain isolation in the firefox renderer. In 29th USENIX Security Symposium (USENIX Security 20), pages 699--716. USENIX Association, August 2020."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_28_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283. Springer Science & Business Media, 2002."},{"key":"e_1_3_2_1_29_1","first-page":"4","article-title":"Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon, Portugal, March 28--April 4, 1998 Proceedings 4, pages 151--166. Springer, 1998.","journal-title":"Portugal, March 28--"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22038-9_23"},{"key":"e_1_3_2_1_31_1","volume-title":"Return-oriented programming: Systems, languages, and applications. ACM Transactions on Information and System Security (TISSEC), 15(1):1--34","author":"Roemer Ryan","year":"2012","unstructured":"Ryan Roemer, Erik Buchanan, Hovav Shacham, and Stefan Savage. Return-oriented programming: Systems, languages, and applications. ACM Transactions on Information and System Security (TISSEC), 15(1):1--34, 2012."},{"key":"e_1_3_2_1_32_1","volume-title":"Scalpel: Exploring the limits of tag-enforced compartmentalization. J. Emerg. Technol. Comput. Syst., 18(1), sep","author":"Roessler Nick","year":"2021","unstructured":"Nick Roessler and Andr\u00e9 DeHon. Scalpel: Exploring the limits of tag-enforced compartmentalization. J. Emerg. Technol. Comput. Syst., 18(1), sep 2021."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337167.3337175"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 18th International Conference on Software Engineering and Formal Methods, SEFM 2020","author":"Verbeek Freek","year":"2020","unstructured":"Freek Verbeek, Pierre Olivier, and Binoy Ravindran. Sound C code decompilation for a subset of x86--64 binaries. In Proceedings of the 18th International Conference on Software Engineering and Formal Methods, SEFM 2020, September 2020."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 24th Annual Symposium on Network and Distributed System Security, NDSS'17","author":"Wang Ruoyu","year":"2017","unstructured":"Ruoyu Wang, Yan Shoshitaishvili, Antonio Bianchi, Aravind Machiry, John Grosen, Paul Grosen, Christopher Kruegel, and Giovanni Vigna. Ramblr: Making reassembly great again. In Proceedings of the 24th Annual Symposium on Network and Distributed System Security, NDSS'17, 2017."},{"key":"e_1_3_2_1_38_1","first-page":"627","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Wang Shuai","year":"2015","unstructured":"Shuai Wang, Pei Wang, and Dinghao Wu. Reassembleable disassembling. In 24th USENIX Security Symposium (USENIX Security 15), pages 627--642, 2015."},{"key":"e_1_3_2_1_39_1","first-page":"13","volume-title":"PLMMS","author":"Wenzel Makarius","year":"2009","unstructured":"Makarius Wenzel. Parallel proof checking in isabelle\/isar. PLMMS, pages 13--29, 2009."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","location":"Salt Lake City UT USA","acronym":"CCS '24","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690244","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690244","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690244","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:06:06Z","timestamp":1755842766000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690244"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":40,"alternative-id":["10.1145\/3658644.3690244","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690244","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}