Automated Vulnerability Analysis in Ethereum Smart Contracts Using Symbolic Execution and SMT Solvers

Abstract

Ethereum smart contracts have emerged as a core component of decentralized applications, enabling
trustless computation and automated value transfer. However, the immutability and public accessibility of smart
contracts make them highly susceptible to security vulnerabilities that can cause severe financial losses. This study
presents an automated vulnerability detection framework that integrates symbolic execution with Satisfiability
Modulo Theories (SMT) solvers for identifying critical weaknesses within Ethereum smart contracts. By leveraging
state-space exploration, path constraint evaluation, and automated assertion checking, the framework effectively
detects reentrancy, integer overflows, timestamp dependencies, and unchecked return value bugs. The proposed
system incorporates two industry-standard open-source analyzers—Mythril and Oyente—to enhance detection
precision and provide comprehensive comparative insights. A benchmark dataset of frequently interacted smart
contracts sourced from Etherscan is used to evaluate tool performance. Experimental results demonstrate improved
detection rates, reduced false positives, and enhanced scalability in exploring complex execution paths. This
automated approach significantly contributes to the security auditing process by minimizing manual effort and
offering a reproducible technique for identifying contract-level vulnerabilities. The findings highlight the importance
of integrating symbolic execution–driven analysis into the development lifecycle to improve the overall reliability
and robustness of decentralized applications.