{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T16:20:01Z","timestamp":1791994801315,"version":"4.4.0"},"reference-count":37,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2025,4,24]],"date-time":"2025-04-24T00:00:00Z","timestamp":1745452800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>The rapid expansion of the Internet of Things (IoT) has made software security and reliability a critical concern. With multi-language programs running on edge computing, embedded systems, and sensors, each connected device represents a potential attack vector, threatening data integrity and privacy. Symbolic execution is a key technique for automated vulnerability detection. However, unknown function interfaces, such as sensor interactions, limit traditional concrete or concolic execution due to uncertain function returns and missing symbolic expressions. Compared with system simulation, the traditional method is to construct an interface abstraction layer for the symbolic execution engine to reduce the cost of simulation. Nevertheless, the disadvantage of this solution is that the manual modeling of these functions is very inefficient and requires professional developers to spend hundreds of hours. In order to improve efficiency, we propose an LLM-based automated approach for modeling unknown functions. By fine-tuning a 20-billion-parameter language model, it automatically generates function models based on annotations and function names. Our method improves symbolic execution efficiency, reducing reliance on manual modeling, which is a limitation of existing frameworks like KLEE. Experimental results primarily focus on comparing the usability, accuracy, and efficiency of LLM-generated models with human-written ones. Our approach was integrated into one verification platform project and applied to the verification of smart contracts with distributed edge computing characteristics. The application of this method directly reduces the manual modeling effort from a month to just a few minutes. This provides a foundational validation of our method\u2019s feasibility, particularly in reducing modeling time while maintaining quality. This work is the first to integrate LLMs into formal verification, offering a scalable and automated verification solution for sensor-driven software, blockchain smart contracts, and WebAssembly systems, expanding the scope of secure IoT development.<\/jats:p>","DOI":"10.3390\/s25092683","type":"journal-article","created":{"date-parts":[[2025,4,24]],"date-time":"2025-04-24T06:18:02Z","timestamp":1745475482000},"page":"2683","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["LLM-Based Unknown Function Automated Modeling in Sensor-Driven Systems for Multi-Language Software Security Verification"],"prefix":"10.3390","volume":"25","author":[{"given":"Liangjun","family":"Deng","sequence":"first","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu 610054, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3736-7135","authenticated-orcid":false,"given":"Qi","family":"Zhong","sequence":"additional","affiliation":[{"name":"Faculty of Data Science, City University of Macau, Macau, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8297-3492","authenticated-orcid":false,"given":"Jingcheng","family":"Song","sequence":"additional","affiliation":[{"name":"School of Information Science and Engineering, Linyi University, Linyi 276000, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hang","family":"Lei","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu 610054, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wenjuan","family":"Li","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Information Technology, The Education University of Hong Kong, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2025,4,24]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"2170","DOI":"10.1109\/TETC.2020.2974183","article-title":"Lightweight privacy-preserving raw data publishing scheme","volume":"9","author":"Chen","year":"2020","journal-title":"IEEE Trans. Emerg. Top. Comput."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"104053","DOI":"10.1016\/j.jnca.2024.104053","article-title":"RLL-SWE: A robust linked list steganography without embedding for intelligence networks in smart environments","volume":"234","author":"Zhao","year":"2025","journal-title":"J. Netw. Comput. Appl."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Zardari, S., Alam, S., Al Salem, H.A., Al Reshan, M.S., Shaikh, A., Malik, A.F.K., Masood ur Rehman, M., and Mouratidis, H. (2022). A comprehensive bibliometric assessment on software testing (2016\u20132021). Electronics, 11.","DOI":"10.3390\/electronics11131984"},{"key":"ref_4","first-page":"100593","article-title":"Industrial blockchain threshold signatures in federated learning for unified space-air-ground-sea model training","volume":"39","author":"Chen","year":"2024","journal-title":"J. Ind. Inf. Integr."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3679013","article-title":"When federated learning meets privacy-preserving computation","volume":"56","author":"Chen","year":"2024","journal-title":"ACM Comput. Surv."},{"key":"ref_6","unstructured":"Alon, U., Brody, S., Levy, O., and Yahav, E. (2018). code2seq: Generating sequences from structured representations of code. arXiv."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"4752","DOI":"10.1109\/TDSC.2022.3233519","article-title":"A Temporal Chrominance Trigger for Clean-Label Backdoor Attack Against Anti-Spoof Rebroadcast Detection","volume":"20","author":"Guo","year":"2023","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"970","DOI":"10.1109\/TIFS.2023.3329426","article-title":"Universal Detection of Backdoor Attacks via Density-Based Clustering and Centroids Analysis","volume":"19","author":"Guo","year":"2024","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Wang, K., Yan, M., Zhang, H., and Hu, H. (2022, January 16\u201317). Unified abstract syntax tree representation learning for cross-language program classification. Proceedings of the 30th IEEE\/ACM International Conference on Program Comprehension, Virtual.","DOI":"10.1145\/3524610.3527915"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Jodogne, S. (2022, January 9\u201311). Rendering Medical Images using WebAssembly. Proceedings of the BIOIMAGING, Online.","DOI":"10.5220\/0010833300003123"},{"key":"ref_11","unstructured":"Chen, J., Han, W., Yin, M., Zeng, H., Song, C., Lee, B., Yin, H., and Shin, I. (2022, January 10\u201312). SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis. Proceedings of the 31st USENIX Security Symposium (USENIX Security 22), Boston, MA, USA."},{"key":"ref_12","unstructured":"Yun, I., Lee, S., Xu, M., Jang, Y., and Kim, T. (2018, January 15\u201317). QSYM: A practical concolic execution engine tailored for hybrid fuzzing. Proceedings of the 27th USENIX Security Symposium (USENIX Security 18), Baltimore, MD, USA."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Klees, G., Ruef, A., Cooper, B., Wei, S., and Hicks, M. (2018, January 15\u201319). Evaluating fuzz testing. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, Toronto, ON, Canada.","DOI":"10.1145\/3243734.3243804"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/j.jss.2007.03.004","article-title":"Examining the significance of high-level programming features in source code author classification","volume":"81","author":"Frantzeskou","year":"2008","journal-title":"J. Syst. Softw."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"867","DOI":"10.1007\/s10009-020-00570-3","article-title":"KLEE symbolic execution engine in 2019","volume":"23","author":"Cadar","year":"2021","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"2155","DOI":"10.32604\/csse.2023.027680","article-title":"Formal Verification Platform as a Service: WebAssembly Vulnerability Detection Application","volume":"45","author":"Deng","year":"2023","journal-title":"Comput. Syst. Sci. Eng."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Jain, S.M., and Jain, S.M. (2022). WebAssembly introduction. WebAssembly for Cloud: A Basic Guide for Wasm-Based Cloud Apps, Springer.","DOI":"10.1007\/978-1-4842-7496-5"},{"key":"ref_18","unstructured":"(2024, April 10). WebAssembly Core Specification. World Wide Web Consortium (W3C). Available online: https:\/\/www.w3.org\/2021\/11\/wasm-stage\/."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Yao, Y., Cen, X., Liu, Y., Yuan, J., and Ye, Y. (2023, January 24\u201327). Blockchain-based Electronic Medical Record Security Sharing Scheme. Proceedings of the 2023 45th Annual International Conference of the IEEE Engineering in Medicine & Biology Society (EMBC), Piscataway, NJ, USA.","DOI":"10.1109\/EMBC40787.2023.10340218"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"3530","DOI":"10.1109\/TII.2021.3114621","article-title":"A Blockchain-Based Auditable Access Control System for Private Data in Service-Centric IoT Environments","volume":"18","author":"Han","year":"2022","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Haas, A., Rossberg, A., Schuff, D.L., Titzer, B.L., Holman, M., Gohman, D., Wagner, L., Zakai, A., and Bastien, J. (2017, January 18\u201323). Bringing the web up to speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, Spain.","DOI":"10.1145\/3062341.3062363"},{"key":"ref_22","unstructured":"Lehmann, D., Kinder, J., and Pradel, M. (2020, January 12\u201314). Everything old is new again: Binary security of WebAssembly. Proceedings of the 29th USENIX Security Symposium (USENIX Security 20), Boston, MA, USA."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Hilbig, A., Lehmann, D., and Pradel, M. (2021, January 12\u201313). An empirical study of real-world webassembly binaries: Security, languages, use cases. Proceedings of the Web Conference 2021, Virtual.","DOI":"10.1145\/3442381.3450138"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Lehmann, D., and Pradel, M. (2019, January 13\u201317). Wasabi: A framework for dynamically analyzing webassembly. Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, Providence, RI, USA.","DOI":"10.1145\/3297858.3304068"},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Sti\u00e9venart, Q., and De Roover, C. (October, January 28). Compositional information flow analysis for WebAssembly programs. Proceedings of the 2020 IEEE 20th International Working Conference on Source Code Analysis and Manipulation (SCAM), Adelaide, Australia.","DOI":"10.1109\/SCAM51674.2020.00007"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Watt, C., Rao, X., Pichon-Pharabod, J., Bodin, M., and Gardner, P. (2021, January 20\u201326). Two mechanisations of webassembly 1.0. Proceedings of the Formal Methods: 24th International Symposium, FM 2021, Virtual Event. Proceedings 24.","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Li, L.T., and Zhang, M. (2022, January 7\u201311). Poster: EOSDFA: Data Flow Analysis of EOSIO Smart Contracts. Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, Los Angeles, CA, USA.","DOI":"10.1145\/3548606.3563545"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"1133","DOI":"10.1109\/TNSE.2020.2968505","article-title":"Contractward: Automated vulnerability detection models for ethereum smart contracts","volume":"8","author":"Wang","year":"2020","journal-title":"IEEE Trans. Netw. Sci. Eng."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Zhao, G., and Huang, J. (2018, January 4\u20139). Deepsim: Deep learning code functional similarity. Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Lake Buena Vista, FL, USA.","DOI":"10.1145\/3236024.3236068"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Sobania, D., Briesch, M., and Rothlauf, F. (2022, January 9\u201313). Choose your programming copilot: A comparison of the program synthesis performance of github copilot and genetic programming. Proceedings of the Genetic and Evolutionary Computation Conference, Boston, MA, USA.","DOI":"10.1145\/3512290.3528700"},{"key":"ref_31","first-page":"129","article-title":"Using ChatGPT to produce code for a typical college-level assignment","volume":"44","author":"Wollowski","year":"2023","journal-title":"AI Mag."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"1092","DOI":"10.1126\/science.abq1158","article-title":"Competition-level code generation with alphacode","volume":"378","author":"Li","year":"2022","journal-title":"Science"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Feng, Y., Vanam, S., Cherukupally, M., Zheng, W., Qiu, M., and Chen, H. (2023, January 26\u201330). Investigating code generation performance of ChatGPT with crowdsourcing social data. Proceedings of the 2023 IEEE 47th Annual Computers, Software, and Applications Conference (COMPSAC), Torino, Italy.","DOI":"10.1109\/COMPSAC57700.2023.00117"},{"key":"ref_34","unstructured":"Gao, L., Biderman, S., Black, S., Golding, L., Hoppe, T., Foster, C., Phang, J., He, H., Thite, A., and Nabeshima, N. (2020). The pile: An 800 GB dataset of diverse text for language modeling. arXiv."},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Rasley, J., Rajbhandari, S., Ruwase, O., and He, Y. (2020, January 6\u201310). Deepspeed: System optimizations enable training deep learning models with over 100 billion parameters. Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, Virtual Event.","DOI":"10.1145\/3394486.3406703"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Black, S., Biderman, S., Hallahan, E., Anthony, Q., Gao, L., Golding, L., He, H., Leahy, C., McDonell, K., and Phang, J. (2022). Gpt-neox-20b: An open-source autoregressive language model. arXiv.","DOI":"10.18653\/v1\/2022.bigscience-1.9"},{"key":"ref_37","first-page":"50","article-title":"A survey of symbolic execution techniques","volume":"51","author":"Baldoni","year":"2018","journal-title":"ACM Comput. Surv. CSUR"}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/25\/9\/2683\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:20:32Z","timestamp":1760030432000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/25\/9\/2683"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,24]]},"references-count":37,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2025,5]]}},"alternative-id":["s25092683"],"URL":"https:\/\/doi.org\/10.3390\/s25092683","relation":{},"ISSN":["1424-8220"],"issn-type":[{"value":"1424-8220","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,24]]}}}