Peng M.HYu FJIE-HONG JIANG2021-09-022021-09-022020https://www.scopus.com/inward/record.uri?eid=2-s2.0-85089125534&partnerID=40&md5=aec2d775cfabb2acff5dc1a5a4e487d9https://scholars.lib.ntu.edu.tw/handle/123456789/580983Successful 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. ? Proceedings of the 24th Pacific Asia Conference on Information Systems: Information Systems (IS) for the Future, PACIS 2020. All rights reserved.Data flow analysis; Flow graphs; Information systems; Information use; Analysis process; Control flow graphs; In-house development; Instruction-level; Number of iterations; Simulation approach; Symbolic execution; Vulnerability detection; Gasesconference paper2-s2.0-85089125534