Graduation Semester and Year
Summer 2025
Language
English
Document Type
Dissertation
Degree Name
Doctor of Philosophy in Computer Science
Department
Computer Science and Engineering
First Advisor
Jeff Lei
Second Advisor
Hao Che
Third Advisor
Christoph Csallner
Fourth Advisor
Allison Sullivan
Abstract
Smart contracts are self-executing programs that transform a blockchain from a distributed digital ledger into a programmable platform enabling a wide range of complex applications. They are susceptible to vulnerabilities and immutable once deployed, which can lead to significant and often irreversible financial losses. Thorough security testing and analysis is hence critical prior to the deployment of smart contracts.
Symbolic execution is one powerful program analysis technique widely applied for security testing and analysis. One major challenge in applying symbolic execution to smart contracts is the function sequence explosion problem. The problem refers to the phenomenon that the number of executed function sequences grows exponentially as the length of sequences increases. We propose to address this problem by considering a subset of sequences driven by code coverage, as high code coverage is generally correlated with improved vulnerability detection. The strategy is designed to balance the execution time with the covered code, aiming for practical applicability.
This dissertation proposes two program analysis-based approaches and one artificial intelligence (AI)-based approach to address the sequence explosion problem from different perspectives. The first program analysis-based approach heuristically considers a subset of sequences selected via function dependency analysis. The second extends on the first one by prioritizing states using state significance analysis at the function-path level. (Note that a state denotes the symbolic state reached at the end of a fully executed path within a function, known as world state or inter-transaction state.) The AI-based approach relies on a large language model (LLM) assisted with the function dependency analysis approach to directly generate a set of sequences.
We have implemented these approaches on the symbolic execution framework that is developed in industry and widely used in academia. We implement a guided symbolic execution tool that enables the two program analysis-based approaches and name the tool SmartExecutor. We also implement an LLM-enhanced symbolic execution tool that is based on the AI-based approach. The experimental evaluation indicates that SmartExecutor can detect more vulnerabilities while achieving competitive code coverage compared with the state-of-the-art tools. The LLM-enhanced tool strikes a balance by detecting a competitive number of vulnerabilities in much less time while achieving slightly higher code coverage, making it an efficient option when execution time is a constraint.
This dissertation can be used to enhance the security analysis of smart contracts and hence the security of blockchain.
Keywords
Symbolic Execution, Ethereum Smart Contracts, LLM, Testing and Security Analysis, Blockchian, AI2SE, Sequence Generation
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Recommended Citation
Wei, Qiping, "Enhancing Symbolic Execution for Solidity Smart Contracts" (2025). Computer Science and Engineering Dissertations. 415.
https://mavmatrix.uta.edu/cse_dissertations/415