Parallel symbolic execution for smart contracts with load balancing
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Fri 6 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
14:00 - 15:30 | |||
14:00 30mTalk | Sound Floating-Point Neural Network Verification with MILP Technical Track Shifu Yang College of Computer, National University of Defense Technology, Changsha, China, Liqian Chen National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Minghao Li College of Computer, National University of Defense Technology, Changsha, China, Yuan Zhou University of Oxford, Ji Wang National University of Defense Technology | ||
14:30 30mTalk | Parallel symbolic execution for smart contracts with load balancing Technical Track | ||
15:00 20mTalk | Designing distributed systems using SAT solvers ERA - Early Research Achievements Puneet Bhateja DA-IICT |