{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T12:29:23Z","timestamp":1784636963480,"version":"3.55.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["RS-2021-NR060080,RS-2022-NR070102"],"award-info":[{"award-number":["RS-2021-NR060080,RS-2022-NR070102"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Institute for Information and Communications Technology Planning and Evaluation","award":["RS-2024-00337703"],"award-info":[{"award-number":["RS-2024-00337703"]}]},{"DOI":"10.13039\/100004358","name":"Samsung Electronics Co., Ltd","doi-asserted-by":"crossref","award":["G01210570"],"award-info":[{"award-number":["G01210570"]}],"id":[{"id":"10.13039\/100004358","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n            Binary lifting is a key component in binary analysis tools.        In order to guarantee the correctness of binary lifting,        researchers have proposed various formally verified lifters.        However, such formally verified lifters have too strict requirements on binary,        which do not sufficiently reflect real-world lifters. In addition, real-world lifters use heuristic-based assumptions to lift binary code, which makes it difficult to guarantee the correctness of the lifted code using formal methods.        In this paper, we propose a new interpretation of the correctness of real-world binary lifting.        We formalize the process of binary lifting with heuristic-based assumptions used in real-world lifters by dividing it into a series of transformations, where each transformation represents a lift with new abstraction features.        We define the correctness of each transformation as\n            <jats:italic toggle=\"yes\">filtered-simulation<\/jats:italic>\n            , which is a variant of bi-simulation, between programs before and after transformation.        We present three essential transformations in binary lifting and formalize them: (1) control flow graph reconstruction, (2) abstract stack reconstruction, and (3) function input\/output identification.        We implement our approach for x86-64 Linux binaries, named FIBLE, and demonstrate that it can correctly lift Coreutils and CGC datasets compiled with GCC.\n          <\/jats:p>","DOI":"10.1145\/3720524","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"898-926","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6792-5161","authenticated-orcid":false,"given":"Jihee","family":"Park","sequence":"first","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8931-2833","authenticated-orcid":false,"given":"Insu","family":"Yun","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0019-9772","authenticated-orcid":false,"given":"Sukyoung","family":"Ryu","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2011. musl libc. https:\/\/musl.libc.org\/"},{"key":"e_1_2_1_2_1","unstructured":"National Security Agency. 2024. Ghidra. https:\/\/www.nsa.gov\/resources\/everyone\/ghidra"},{"key":"e_1_2_1_3_1","unstructured":"National Security Agency. 2024. Ghidra P-Code description. https:\/\/github.com\/NationalSecurityAgency\/ghidra\/blob\/master\/GhidraDocs\/languages\/html\/pcodedescription.html"},{"key":"e_1_2_1_4_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley. isbn:0321486811"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2013.20"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465351.2465380"},{"key":"e_1_2_1_7_1","unstructured":"Avast Software. 2017. RetDec: A Retargetable Machine-Code Decompiler. https:\/\/retdec.com\/"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_6"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the FREENIX Track: 2005 USENIX Annual Technical Conference","author":"Bellard Fabrice","year":"2005","unstructured":"Fabrice Bellard. 2005. QEMU, a Fast and Portable Dynamic Translator. In Proceedings of the FREENIX Track: 2005 USENIX Annual Technical Conference, April 10-15, 2005, Anaheim, CA, USA. USENIX, 41\u201346. http:\/\/www.usenix.org\/events\/usenix05\/tech\/freenix\/bellard.html"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN48987.2021.00064"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2005.20"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/WPC.1999.777758"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385964"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474369.3486865"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968455.2968514"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3033019.3033028"},{"key":"e_1_2_1_22_1","unstructured":"A. Dinaburg A. Kumar P. Goodman A. Gario and G. Reece. 2024. McSema. https:\/\/github.com\/lifting-bits\/mcsema"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80395-5"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00194-7"},{"key":"e_1_2_1_26_1","unstructured":"GNU. 2024. Extensions to the C Language Family - x86 Function Attributes. https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/x86-Function-Attributes.html"},{"key":"e_1_2_1_27_1","unstructured":"GrammaTech. 2022. CGC Challenge Binaries. https:\/\/github.com\/GrammaTech\/cgc-cbs"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2017.70"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.14722\/bar.2019.23051"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_19"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503299"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029444.99264.c0"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-009-9155-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Lixin Li and Chao Wang. 2013. Dynamic Analysis and Debugging of Binary Code for Security Applications. In Runtime Verification Axel Legay and Saddek Bensalem (Eds.). Springer Berlin Heidelberg 403\u2013423. isbn:978-3-642-40787-1","DOI":"10.1007\/978-3-642-40787-1_31"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106295"},{"key":"e_1_2_1_37_1","unstructured":"Lifting Bits. 2024. Remill. https:\/\/github.com\/lifting-bits\/remill"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833799"},{"key":"e_1_2_1_39_1","volume-title":"VulHawk: Cross-architecture Vulnerability Detection with Entropy-based Binary Code Search. In 30th Annual Network and Distributed System Security Symposium, NDSS 2023","author":"Luo Zhenhao","year":"2023","unstructured":"Zhenhao Luo, Pengfei Wang, Baosheng Wang, Yong Tang, Wei Xie, Xu Zhou, Danjun Liu, and Kai Lu. 2023. VulHawk: Cross-architecture Vulnerability Detection with Entropy-based Binary Code Search. In 30th Annual Network and Distributed System Security Symposium, NDSS 2023, San Diego, California, USA, February 27 - March 3, 2023. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/vulhawk-cross-architecture-vulnerability-detection-with-entropy-based-binary-code-search\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10990-006-8609-1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_2_1_42_1","volume-title":"FMCAD 2012","author":"Myreen Magnus O.","year":"2012","unstructured":"Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. 2012. Decompilation into logic - Improved. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012, Gianpiero Cabodi and Satnam Singh (Eds.). IEEE, 78\u201381. https:\/\/ieeexplore.ieee.org\/document\/6462558\/"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-25803-9_7"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2019.8661201"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Jihee Park Insu Yun and Sukyoung Ryu. 2024. Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation (Artifact). https:\/\/doi.org\/10.5281\/zenodo.14903169 10.5281\/zenodo.14903169","DOI":"10.5281\/zenodo.14903169"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Jihee Park Insu Yun and Sukyoung Ryu. 2024. Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation (Extended Report). https:\/\/doi.org\/10.5281\/zenodo.14922366 10.5281\/zenodo.14922366","DOI":"10.5281\/zenodo.14922366"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW59333.2023.00026"},{"key":"e_1_2_1_48_1","unstructured":"Radare2 Team. 2017. radare2. https:\/\/github.com\/radareorg\/radare2"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2907"},{"key":"e_1_2_1_50_1","unstructured":"Hex-Rays SA. 2024. About IDA. https:\/\/www.hex-rays.com\/products\/ida\/"},{"key":"e_1_2_1_51_1","volume-title":"IDA: What\u2019s new in 7.1. https:\/\/hex-rays.com\/products\/ida\/news\/7_1\/","author":"Hex-Rays","year":"2024","unstructured":"Hex-Rays SA. 2024. IDA: What\u2019s new in 7.1. https:\/\/hex-rays.com\/products\/ida\/news\/7_1\/"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1315245.1315313"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_2_1_54_1","volume-title":"FFXE: Dynamic Control Flow Graph Recovery for Embedded Firmware Binaries. In 33rd USENIX Security Symposium (USENIX Security 24)","author":"Tsang Ryan","year":"2024","unstructured":"Ryan Tsang, Asmita, Doreen Joseph, Soheil Salehi, Prasant Mohapatra, and Houman Homayoun. 2024. FFXE: Dynamic Control Flow Graph Recovery for Embedded Firmware Binaries. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, 5573\u20135590. isbn:978-1-939133-44-1 https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/tsang"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359986.3361215"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_6"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3564625.3568001"},{"key":"e_1_2_1_59_1","volume-title":"Playing Without Paying: Detecting Vulnerable Payment Verification in Native Binaries of Unity Mobile Games. In 31st USENIX Security Symposium (USENIX Security 22)","author":"Zuo Chaoshun","year":"2022","unstructured":"Chaoshun Zuo and Zhiqiang Lin. 2022. Playing Without Paying: Detecting Vulnerable Payment Verification in Native Binaries of Unity Mobile Games. In 31st USENIX Security Symposium (USENIX Security 22). USENIX Association, 3093\u20133110. isbn:978-1-939133-31-1 https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/zuo"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720524","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720524","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:09:18Z","timestamp":1760029758000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720524"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":59,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720524"],"URL":"https:\/\/doi.org\/10.1145\/3720524","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}