Successful executions of smart contracts require sufficient pre-allocated transaction fees, i.e., gas, on Ethereum. A gas vulnerability is a feasible execution of smart contracts that has its gas consumption depending on external inputs, e.g., used to check loop conditions or to calculate gas formulas. Such gas vulnerabilities may be exploited to raise massive gas consumption that leads the execution to unexpected exceptions. In this work, we propose an instruction-level symbolic stack simulation approach for systematic gas vulnerability detection and attack synthesis. The analysis process consists of 1) a sound control flow graph construction with blocks that are associated with their gas formulas and stack states, 2) symbolic execution path enumeration along with path and gas constraints generation, where loops are symbolically encoded with an auxiliary index for the number of iterations, and 3) gas vulnerability detection and its attack synthesis. To synthesize an attack to exploit the vulnerability, we use the sat model returned by an SMT solver to generate the inputs to trigger the execution that exceeds the gas limit. We report our analysis results against various contracts on Etherscan and In-house development cases, revealing previously unknown vulnerabilities in these contracts.
Peng, Min Hao; Yu, Fang; and Jiang, Jie Hong Roland, "Symbolic Gas Vulnerability Detection and Attack Synthesis" (2020). PACIS 2020 Proceedings. 107.
When commenting on articles, please be friendly, welcoming, respectful and abide by the AIS eLibrary Discussion Thread Code of Conduct posted here.