Reinforcement Learning Guided Symbolic Execution for Ethereum Smart Contracts

Abstract

Symbolic execution is one of the most popular technologies for detecting vulnerabilities in smart contracts, however, the path explosion problem and the timeout problem in solving path constraints hinder the detection efficiency. In order to find possible vulnerabilities in smart contracts faster, we propose a reinforcement learning guided heuristic search strategy for symbolic execution of smart contracts. In the strategy, we employ Q-Iearning as the reinforcement learning algorithm, and use Q-table to provide some suggestions for the path selection of symbolic execution. In addition, to further improve the detection efficiency, an incentive path pruning strategy is also adopted to delete paths which are not relevant to finding vulnerabilities. Moreover, for the timeout problem in solving path constraints, we predict the solution time to determine whether or not to solve a constraint. We have implemented our strategies in a tool called MythrilQL, and evaluated it on benchmarks consisting of four publicly available smart contract datasets and 5 large-scale contracts with more than 800 LOC (line of code). The experimental results show that MythrilQL is more efficiency than the most related tools Mythril and MPro, especially in detecting smart contracts in large scale.