Related Experiment Video
Updated: May 17, 2025

03:14
Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness
Published on: December 6, 2024
466
LLM-Based Unknown Function Automated Modeling in Sensor-Driven Systems for Multi-Language Software Security
Liangjun Deng1, Qi Zhong2, Jingcheng Song3
1School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu 610054, China.
Sensors (Basel, Switzerland)
|May 14, 2025
Summary
This study introduces an automated method using large language models (LLMs) to model unknown functions for symbolic execution, significantly reducing manual effort in software security verification for the Internet of Things (IoT). The approach enhances efficiency and accuracy in detecting vulnerabilities in complex systems.
Area of Science:
- Computer Science
- Software Engineering
- Artificial Intelligence
Background:
- The proliferation of Internet of Things (IoT) devices introduces significant software security and reliability challenges due to complex, multi-language programs and potential attack vectors.
- Symbolic execution is crucial for automated vulnerability detection but is hindered by unknown function interfaces, common in sensor interactions, which require extensive manual modeling.
- Existing methods for handling unknown interfaces in symbolic execution are inefficient, demanding hundreds of hours from professional developers for manual modeling.
Purpose of the Study:
- To propose and evaluate an automated approach for modeling unknown functions using large language models (LLMs) to enhance symbolic execution for software security.
- To reduce the significant manual effort and time currently required for interface modeling in formal verification processes.
- To improve the efficiency, accuracy, and scalability of vulnerability detection in IoT and related systems.
Main Methods:
- Fine-tuning a 20-billion-parameter language model to automatically generate function models based on annotations and function names.
- Integrating the LLM-based function modeling approach into a symbolic execution engine.
- Comparing the performance (usability, accuracy, efficiency) of LLM-generated models against human-written models.
Main Results:
- The LLM-based approach significantly reduces manual modeling effort from months to minutes.
- Experimental results demonstrate comparable usability and accuracy between LLM-generated and human-written models.
- The method was successfully applied to verify smart contracts in distributed edge computing environments, validating its practical feasibility.
Conclusions:
- LLMs offer a scalable and automated solution for modeling unknown functions, overcoming a key limitation in symbolic execution for software verification.
- This work represents the first integration of LLMs into formal verification, paving the way for more efficient and accessible security analysis of sensor-driven software, smart contracts, and WebAssembly systems.
- The proposed method enhances the scope and applicability of secure IoT development by automating a previously labor-intensive process.

