Parallel Symbolic Execution for Smart Contracts with Load Balancing

As an effective technology for detecting vulnerabilities, symbolic execution has been applied to detect vulnerabilities in smart contracts. However, it faces challenges such as low detection efficiency. Existing parallel symbolic execution techniques for vulnerability detection of smart contracts lack load balancing mechanism, resulting in unnecessary overhead. To address this issue, we propose a load-balanced parallel symbolic execution approach to accelerate the vulnerability detection of smart contracts. In the approach, the main process first explores and assigns an initial path to each worker process. The worker processes then explore different paths in parallel and utilize a work stealing algorithm to balance the workload among them. By allowing multiple worker processes to explore various paths on different CPU cores and ensuring the load balance, we enhance the efficiency of symbolic execution. We implement a parallel symbolic execution tool called PMyth based on Mythril and evaluate our approach by experimenting on two third-party datasets. The experimental results show that PMyth can provide up to 4.36x acceleration compared to Mythril.