{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:04:22Z","timestamp":1750309462092,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T00:00:00Z","timestamp":1740268800000},"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":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>Concolic execution follows the execution paths of concrete inputs, capable of generating new inputs for unexplored code by solving negated path constraints. However, implicit flows can hinder concolic execution, reducing the code coverage. Implicit flows occur when inputs influence control flow, and the control flow variation affects the values of some variables. During concolic execution, the preceding path selections limit the potential values of these variables. This limitation may result in unsolvable constraints, subsequently restricting the generation of new inputs for unexplored paths. Our insight is that following the same preceding paths is unnecessary, and we can adapt preceding paths to make the latest constraints solvable. We divide states into general states and implicit-flow-solving states (IFSSs). We utilize the general states to perform concolic execution. When solving constraints influenced by implicit flows, we switch to the IFSSs. We use the IFSSs to explore the relevant code region and adapt paths. To mitigate path explosion and construct the relation between inputs and the variables, we merge the IFSSs. State merging does not burden the general states, and we limit the code regions for the IFSSs to minimize the introduced overhead. Finally, we replace the variable symbols in the target constraints with new expressions and attempt to solve the new constraints. We implement our approach in Backsolver and build a test suite to evaluate it. Backsolver successfully identifies all the implicit flows in the test suite and resolves most of them. When evaluated on six real-world binaries, Backsolver resolves the highest number of branches related to implicit flows in total. Besides, Backsolver has the highest code coverage in PlutoSVG and finds a 0-day vulnerability. We reported the vulnerability and obtained a CVE ID.<\/jats:p>","DOI":"10.1145\/3712194","type":"journal-article","created":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T14:48:33Z","timestamp":1737038913000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Backsolver: Adapting Preceding Execution Paths to Solve Constraints for Concolic Execution"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-0267-5629","authenticated-orcid":false,"given":"Yicheng","family":"Zeng","sequence":"first","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China and School of Cyber Security, University of the Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3284-7351","authenticated-orcid":false,"given":"Zhanwei","family":"Song","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China and School of Cyber Security, University of the Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4215-9971","authenticated-orcid":false,"given":"Guo","family":"Lv","sequence":"additional","affiliation":[{"name":"Jiangsu Provincial Public Security Department, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3263-8222","authenticated-orcid":false,"given":"Yu","family":"Zhou","sequence":"additional","affiliation":[{"name":"Jiangsu Provincial Public Security Department, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3720-7403","authenticated-orcid":false,"given":"Hongsong","family":"Zhu","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China and School of Cyber Security, University of the Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2745-7521","authenticated-orcid":false,"given":"Limin","family":"Sun","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China and School of Cyber Security, University of the Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,2,23]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"File. 2018. file. Retrieved from https:\/\/github.com\/file\/file\/tree\/6367a7c9b476767a692f76e78e3b355dc9386e48"},{"key":"e_1_3_1_3_2","unstructured":"Pnggroup. 2018. libpng. Retrieved from https:\/\/github.com\/pnggroup\/libpng"},{"key":"e_1_3_1_4_2","unstructured":"Matthias. 2019. Exif JPEG header manipulation tool. Retrieved from https:\/\/www.sentex.ca\/mwandel\/jhead\/"},{"key":"e_1_3_1_5_2","unstructured":"Badnack. 2020. Angr taint engine. Retrieved from https:\/\/github.com\/badnack\/angr_taint_engine"},{"key":"e_1_3_1_6_2","unstructured":"Sammycage. 2020. PlutoVG. Retrieved from https:\/\/github.com\/sammycage\/plutovg\/tree\/91ebcfc3cca193ac9267eaf1fdff342a6583738b"},{"key":"e_1_3_1_7_2","unstructured":"Sammycage. 2021. PlutoSVG. Retrieved from https:\/\/github.com\/sammycage\/plutosvg\/tree\/336c02997277a1888e6ccbbbe674551a0582e5c4"},{"key":"e_1_3_1_8_2","unstructured":"Angr. 2024. Angr error. Retrieved from https:\/\/docs.angr.io\/en\/latest\/faq.html#what-does-unsupportediroperror-floating-point-support-disabled-mean"},{"key":"e_1_3_1_9_2","unstructured":"Sunwithmoon. 2024. Backsolver. Retrieved from https:\/\/github.com\/sunwithmoon\/Backsolver"},{"key":"e_1_3_1_10_2","unstructured":"Sunwithmoon. 2024. Implicit test suite. Retrieved from https:\/\/github.com\/sunwithmoon\/implicit_check"},{"key":"e_1_3_1_11_2","unstructured":"Akheron. 2024. jansson. Retrieved from https:\/\/github.com\/akheron\/jansson"},{"key":"e_1_3_1_12_2","unstructured":"GNU Binary Utilities. 2024. readelf. Retrieved from https:\/\/www.gnu.org\/software\/binutils"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","first-page":"787","DOI":"10.1109\/ICSE.2015.250","volume-title":"Proceedings of the 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering","volume":"2","author":"Bichhawat Abhishek","year":"2015","unstructured":"Abhishek Bichhawat. 2015. Post-dominator analysis for precisely handling implicit flows. In Proceedings of the 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering, Vol. 2, IEEE, 787\u2013789."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102368"},{"key":"e_1_3_1_16_2","first-page":"199","volume-title":"Proceedings of the 2013 USENIX Annual Technical Conference (USENIX ATC \u201913)","author":"Bugrara Suhabe","year":"2013","unstructured":"Suhabe Bugrara and Dawson Engler. 2013. Redundant state detection for dynamic symbolic execution. In Proceedings of the 2013 USENIX Annual Technical Conference (USENIX ATC \u201913), 199\u2013211."},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"e_1_3_1_18_2","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R. Engler. 2008. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, Vol. 8, 209\u2013224."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363225"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/2810103.2813643","volume-title":"Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security","author":"Chen Qi Alfred","year":"2015","unstructured":"Qi Alfred Chen, Zhiyun Qian, Yunhan Jack Jia, Yuru Shao, and Zhuoqing Morley Mao. 2015. Static detection of packet injection vulnerabilities: A case for identifying attacker-controlled implicit information leaks. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 388\u2013400."},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"1580","DOI":"10.1109\/SP40000.2020.00002","volume-title":"Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920)","author":"Chen Yaohui","year":"2020","unstructured":"Yaohui Chen, Peng Li, Jun Xu, Shengjian Guo, Rundong Zhou, Yulong Zhang, Tao Wei, and Long Lu. 2020. Savior: Towards bug-driven hybrid testing. In Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920). IEEE, 1580\u20131596."},{"key":"e_1_3_1_24_2","volume-title":"Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep)","author":"Chipounov Vitaly","year":"2009","unstructured":"Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, and George Candea. 2009. Selective symbolic execution. In Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep)."},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273464"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","first-page":"1613","DOI":"10.1109\/SP40000.2020.00063","volume-title":"Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920)","author":"Huang Heqing","year":"2020","unstructured":"Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang. 2020. Pangolin: Incremental hybrid fuzzing with polyhedral path abstraction. In Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920). IEEE, 1613\u20131627."},{"key":"e_1_3_1_28_2","first-page":"1913","volume-title":"Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919)","author":"Jung Jinho","year":"2019","unstructured":"Jinho Jung, Hong Hu, David Solodukhin, Daniel Pagan, Kyu Hyung Lee, and Taesoo Kim. 2019. Fuzzification:{anti-fuzzing} techniques. In Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919), 1913\u20131930."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2811411.2811485"},{"key":"e_1_3_1_30_2","volume-title":"Proceedings of the Network and Distributed System Security Symposium","author":"Kang Min Gyung","year":"2011","unstructured":"Min Gyung Kang, Stephen McCamant, Pongsin Poosankam, and Dawn Song. 2011. Dta \\(++\\) : Dynamic taint analysis with targeted control-flow propagation. In Proceedings of the Network and Distributed System Security Symposium."},{"key":"e_1_3_1_31_2","first-page":"438","volume-title":"Proceedings of the 44th IEEE\/ACM International Conference on Software Engineering (ICSE \u201922)","volume":"22","author":"Kukucka James","year":"2022","unstructured":"James Kukucka, Lu\u00eds Pina, Paul Ammann, and Jonathan Bell. 2022. CONFETTI: Amplifying concolic guidance for fuzzers. In Proceedings of the 44th IEEE\/ACM International Conference on Software Engineering (ICSE \u201922), Vol. 22, 438\u2013450."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254088"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357071"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.41"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491438"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3471621.3471852"},{"key":"e_1_3_1_37_2","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/978-3-642-24372-1_34","volume-title":"Proceedings of the International Symposium on Automated Technology for Verification and Analysis","author":"Obdr\u017e\u00e1lek Jan","year":"2011","unstructured":"Jan Obdr\u017e\u00e1lek and Marek Trt\u00edk. 2011. Efficient loop navigation for symbolic execution. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Springer, 453\u2013462."},{"key":"e_1_3_1_38_2","unstructured":"Brian S. Pak. 2012. Hybrid fuzz testing: Discovering software bugs via fuzzing and symbolic execution. School of Computer Science Carnegie Mellon University."},{"key":"e_1_3_1_39_2","first-page":"181","volume-title":"Proceedings of the 29th USENIX Security Symposium (USENIX Security \u201920)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with {SymCC}: Don\u2019t interpret, compile!. In Proceedings of the 29th USENIX Security Symposium (USENIX Security \u201920), 181\u2013198."},{"key":"e_1_3_1_40_2","first-page":"49","volume-title":"Proceedings of the 24th USENIX Security Symposium (USENIX Security \u201915)","author":"Ramos David A.","year":"2015","unstructured":"David A. Ramos and Dawson Engler. 2015. {Under-Constrained} symbolic execution: Correctness checking for real code. In Proceedings of the 24th USENIX Security Symposium (USENIX Security \u201915), 49\u201364."},{"key":"e_1_3_1_41_2","first-page":"781","volume-title":"Proceedings of the 26th USENIX Security Symposium (USENIX Security \u201917)","author":"Redini Nilo","year":"2017","unstructured":"Nilo Redini, Aravind Machiry, Dipanjan Das, Yanick Fratantonio, Antonio Bianchi, Eric Gustafson, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2017. {BootStomp}: On the security of bootloaders in mobile devices. In Proceedings of the 26th USENIX Security Symposium (USENIX Security \u201917), 781\u2013798."},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","first-page":"1544","DOI":"10.1109\/SP40000.2020.00036","volume-title":"Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920)","author":"Redini Nilo","year":"2020","unstructured":"Nilo Redini, Aravind Machiry, Ruoyu Wang, Chad Spensky, Andrea Continella, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2020. Karonte: Detecting insecure multi-binary interactions in embedded firmware. In Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP \u201920). IEEE, 1544\u20131561."},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321746"},{"key":"e_1_3_1_45_2","first-page":"1","volume-title":"Proceedings of the 2016 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD \u201916)","author":"Shin Jangseop","year":"2016","unstructured":"Jangseop Shin, Hongce Zhang, Jinyong Lee, Ingoo Heo, Yu-Yuan Chen, Ruby Lee, and Yunheung Paek. 2016. A hardware-based technique for efficient implicit information flow tracking. In Proceedings of the 2016 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD \u201916). IEEE, 1\u20137."},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1109\/SP.2016.17","volume-title":"Proceedings of the 2016 IEEE Symposium on Security and Privacy (SP \u201916)","author":"Shoshitaishvili Yan","year":"2016","unstructured":"Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, et al. 2016. Sok:(state of) the art of war: Offensive techniques in binary analysis. In Proceedings of the 2016 IEEE Symposium on Security and Privacy (SP \u201916). IEEE, 138\u2013157."},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23368"},{"key":"e_1_3_1_48_2","first-page":"413","volume-title":"Proceedings of the 31st USENIX Security Symposium (USENIX Security \u201922)","author":"Vadayath Jayakrishna","year":"2022","unstructured":"Jayakrishna Vadayath, Moritz Eckert, Kyle Zeng, Nicolaas Weideman, Gokulkrishna Praveen Menon, Yanick Fratantonio, Davide Balzarotti, Adam Doup\u00e9, Tiffany Bao, Ruoyu Wang, et al. 2022. Arbiter: Bridging the static and dynamic divide in vulnerability discovery on binary programs. In Proceedings of the 31st USENIX Security Symposium (USENIX Security \u201922), 413\u2013430."},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180177"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813663"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3604608"},{"key":"e_1_3_1_52_2","first-page":"745","volume-title":"Proceedings of the 27th USENIX Security Symposium (USENIX Security \u201918)","author":"Yun Insu","year":"2018","unstructured":"Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2018. {QSYM}: A practical concolic execution engine tailored for hybrid fuzzing. In Proceedings of the 27th USENIX Security Symposium (USENIX Security \u201918), 745\u2013761."},{"key":"e_1_3_1_53_2","unstructured":"Michal Zalewski. 2010. American fuzzy lop. Retrieved from http:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_3_1_54_2","first-page":"290","volume-title":"Proceedings of the 2022 IEEE International Performance, Computing, and Communications Conference (IPCCC \u201922)","author":"Zeng Yicheng","year":"2022","unstructured":"Yicheng Zeng, Jiaqian Peng, Zhihui Zhao, Zhanwei Song, Hongsong Zhu, and Limin Sun. 2022. SIFOL: Solving implicit flows in loops for concolic execution. In Proceedings of the 2022 IEEE International Performance, Computing, and Communications Conference (IPCCC \u201922). IEEE, 290\u2013297."},{"key":"e_1_3_1_55_2","volume-title":"Proceedings of the 26th Network and Distributed System Security Symposium","author":"Zhao Lei","year":"2019","unstructured":"Lei Zhao, Yue Duan, Heng Yin, and Jifeng Xuan. 2019. Send hardest problems my way: Probabilistic path prioritization for hybrid fuzzing. In Proceedings of the 26th Network and Distributed System Security Symposium."},{"key":"e_1_3_1_56_2","first-page":"4365","volume-title":"Proceedings of the 31st USENIX Security Symposium (USENIX Security \u201922)","author":"Zhou Shunfan","year":"2022","unstructured":"Shunfan Zhou, Zhemin Yang, Dan Qiao, Peng Liu, Min Yang, Zhe Wang, and Chenggang Wu. 2022. Ferry: {State-aware} symbolic execution for exploring {State-dependent} program paths. In Proceedings of the 31st USENIX Security Symposium (USENIX Security \u201922), 4365\u20134382."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3712194","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3712194","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:10:28Z","timestamp":1750295428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3712194"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,23]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3712194"],"URL":"https:\/\/doi.org\/10.1145\/3712194","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2025,2,23]]},"assertion":[{"value":"2024-05-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}